SystemC TLM Verification

Journal Papers

1. A. Habibi and S. Tahar: On the Transformation of SystemC to AsmL using Abstract Interpretation. Electronic Notes in Theoretical Computer Science, 131:39-49, May 2005.


2. A. Habibi and S. Tahar: Design and Verification of SystemC Transaction Level Model.Very Large Scale Integration (VLSI) Systems, IEEE Transactions on , vol.14, no.1, pp.57,68, Jan. 2006


3. A.Gawanmeh, S. Tahar, H. Moinudeen, and A. Habibi: A Design for Verification Approach using an Embedding of PSL in AsmL. Journal of Circuits, Systems, and Computers, Vol. 16, No. 6, World Scientific Publishing, 2008, pp. 859.881.

Conference Papers

1. A. Habibi, H. Moinudeen and S. Tahar: Towards a Faster Simulation of SystemC Designs ; Proc. IEEE Computer Society Annual Symposium on VLSI (ISVLSI'06), Karlsruhe, Germany, March 2006.


2. A. Habibi, S.Tahar, A. Samara, D. Li, O. Ait-Mohamed: Efficient Assertion Based Verification using TLM ; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006.


3. A. Habibi, H. Moinudeen and S. Tahar: Generating Finite State Machines from SystemC; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006


4. A. Habibi and S. Tahar: On the Formal Verification of a SystemC Packet Switch Model; Proc. IEEE International Conference on Electronics, Circuits and Systems (ICECS'05), Gammarth, Tunisia, December 2005.


5. A. Habibi and S. Tahar: An Approach for the Verification of SystemC Designs using AsmL; In: D.A. Peled. and Y.-K. Tsay (Eds.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3707, Springer Verlag, pp. 69-83. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, October 2005]


6. H. Moinudeen, A. Habibi, and S. Tahar: An Executable Specification of the PCI-X Bus Standard in AsmL. In Proc. of the Canadian Conference on Electrical & Computer Engineering, Saskatoon, Saskatchewan, Canada, May 2005.


7. A. Habibi and S. Tahar: Design for Verification of SystemC Transaction Level Models. In Proc. of the Design Automation and Test in Europe, pages 560-565, Munich, Germany, March 2005.


8. A. Habibi, A. I. Ahmed, O. Ait-Mohamed, and S. Tahar: On the Design and Verification of the Look-Aside Interface . In Proc. of the Design Automation and Test in Europe, pages 290-296, Munich, Germany, March 2005


9. A. Habibi and S. Tahar: AsmL Semantics in Fixpoint . In Proc. of the International Conference on Abstract State Machines, pages 233-245, Paris, France, March 2005


10. A. Gawanmeh, A. Habibi, and S. Tahar: Embedding and Verification of PSL using ASM . In Proc. of the International Conference on Abstract State Machines, pages 201-215, Paris, France, March 2005


11. K. Oumalou, A. Habibi, and S. Tahar: Design for Verification of a PCI Bus in SystemC . In Proc. of the Symposium on System-on-Chip, Tampere, Finland, November 2004


12. A. Habibi, A. Gawanmeh, and S. Tahar: Assertion Based Verification of PSL for SystemC Designs . In Proc. of the Symposium on System-on-Chip, Tampere, Finland, November 2004.


13. A. Habibi and S. Tahar: Towards an Efficient Assertion Based Verification of SystemC Designs . In Proc. of the High Level Design Validation and Test Workshop, pages 19-22, Sonoma Valley, California, USA, November 2004.


14. A. Gawanmeh, A. Habibi, and S. Tahar: Enabling SystemC Verification using Abstract State Machines . In Proc. of the Forum on Specification & Design Languages, pages 19-22, Lille, France, September 2004.


15. A. Habibi, S. Tahar, and L. Halleb: Formal Verification of a Bus Structure Modeled in SystemC. In Proc. of the Northeast Workshop on Circuits and Systems, pages 61-64, Montreal, Quebec, Canada, June 2004


16. A. Habibi and S. Tahar: On the Extension of SystemC by SystemVerilog Assertions . In Proc. of the Canadian Conference on Electrical & Computer Engineering, volume 4, pages 1869-1872, Niagara Falls, Ontario, Canada, May 2004.


17. A. Habibi and S. Tahar: A Survey on System-On-a-Chip Design Languages . In Proc. of the International Workshop on System-on-Chip, volume 4, pages 212-215, Calgary, Alberta, Canada, June-July 2003.


18. A. Habibi and S. Tahar: Formal Verification of the ADSP-2100 Processor using the HOL Theorem Prover. IEEE Proceedings on Computers and Digital Techniques,vol.2, p 614-19, 2002,.


 

Technical Reports




SystemC Semantics in Fixpoint

A. Habibi and S. Tahar


SystemC is among a group of system level design languages proposed to raise the abstraction level for embedded system design and verification. Defining the formal semantics of SystemC is an important and mandatory step towards enabling the formal verification of SystemC. In this technical report, we present a sound and complete semantics of the main parts of SystemC in fixpoint. Such a semantics are a precise and non ambiguous definitions of the SystemC library. They are very useful to guarantee a unique implementation of the library and interpretation of its behaviour. Besides, they can used in conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages.

A. Habibi and S. Tahar: SystemC fixpoint semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [15 pages]

Send comments and suggestions to: habibi@ece.concordia.ca


 



AsmL Semantics in Fixpoint

A. Habibi and S. Tahar


AsmL is a novel executable specification language based on the theory of Abstract State Machines (ASMs). It represents one of the most powerful practical engines to write and execute ASMs. In this report, we present a proven complete small-step trace-based operational semantics of the main parts of AsmL. Such a semantics provides precise and non ambiguous definitions of AsmL. It is very useful to guarantee a unique implementation of the language and interpretation of its behavior. Furthermore, they can be used in conducting formal proofs for sound abstractions or even to construct syntactical transformers to other languages.

A. Habibi and S. Tahar: A Survey: AsmL fixpoint semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [18 pages].

Send comments and suggestions to: habibi@ece.concordia.ca


 



Design and Verification of SystemC Transaction Level Models

A. Habibi and S. Tahar


Transaction level modeling allows exploring several SoC design architectures leading to better performance and easier verification of the final product. In this report, we present an approach to design and verify SystemC models at the transaction level. We integrate the verification as part of the design-flow where we first model both the design and the properties (written in PSL) in UML; then, we translate them into an intermediate format modeled with AsmL (language based on Abstract State Machines (ASM)). The AsmL model is used to generate an FSM of the design including the properties. Finally, we translate the verified design to SystemC and map the properties to a set of assertions (as monitors in C#) that can be reused to validate the design at lower levels by simulation. At the SystemC level, we also present a genetic algorithm to enhance the assertions coverage. We will ensure the soundness of our approach by proving the correctness of the SystemC to AsmL and AsmL to SystemC transformations. We illustrate our approach on two case studies including the PCI bus standard and a Master/ Slave generic architecture from the SystemC library.

A. Habibi and S. Tahar: Design and Verification of SystemC Transaction Level Models; Technical Report, Concordia University, Department of Electrical and Computer Engineering. December 2004. [32 pages].

Send comments and suggestions to: habibi@ece.concordia.ca


 



Enabling SystemC Verification using Abstract State Machines

A. Gawanmeh, A. Habibi, and S. Tahar


SystemC is a system level language recently proposed to raise the abstraction level for embedded systems design and verification. We propose a verification methodology for SystemC designs based on a combination of static code analysis and SystemC semantics described with abstract state machines (ASM). We abstract the source SystemC design into hypergraphs to keep an abstract (simplified) view of the design including only processes status, activation conditions and order of execution. This latter is then modeled with ASMs and compiled with the AsmL tool in order to generate a finite state machine that can be used for formal verification by external tools linked to ASM, such as model checkers or theorem provers. We can also generate a .NET representation of the abstracted SystemC model to guide test vectors generation and perform coverage analysis within the .NET framework. Our approach solves a number of problems classical verification techniques do face when used with SystemC through the efficient handling of the object--oriented aspect of SystemC and the complexity of its simulation environment.

A. Gawanmeh, A. Habibi, and S. Tahar: Enabling SystemC Verification using Abstract State Machines; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2004. [15 pages]

Send comments and suggestions to: amjad@ece.concordia.ca


 

An Executable Operational Semantics for SystemC using Abstract State Machines

A. Gawanmeh, A. Habibi, and S. Tahar


In this work, we use the Abstract State Machines (ASM) modeling language, AsmL, to define the semantics of the SystemC system level language. AsmL provides an efficient way for formally specifying computing systems. The SystemC semantics we defined includes SystemC FIFO channels, MUTEX channels, message queuing, request-grant protocol and SystemC FIFO hierarchical channels with handshake protocol. We also specified the semantics of design rules for SystemC channels including static and dynamic design rules checking. We then defined the operation of SystemC simulator in AsmL, where SystemC designs can be described in AsmL within our model, and run on the simulator we define. The simulator we defined provide the SystemC operational semantics by means of ASM transition rules that can be executed using supporting tools for AsmL, such as Microsoft Word, Microsoft .NET Visual Studio, and AsmL Tester. This allows the specification of SystemC designs in ASM and their execution, however, it lefts the level at which we describe the design from the implementation level (in SystemC) to a more abstract level (in ASM), where we define the behavior of our system as a set of events and processes. We then describe this abstraction, and what features of the design can be modeled in order to be run on the simulator. We believe that this work reduces the learning time and effort for understanding SystemC by providing an abstract executable simulator.

A. Gawanmeh, A. Habibi, and S. Tahar: An Executable Operational Semantics for SystemC using Abstract State Machines; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2004. [24 pages].

Send comments and suggestions to: amjad@ece.concordia.ca


 

A Survey: System-on-a-Chip Design and Verification

A. Habibi and S. Tahar


In this technical report, we survey the state-of-the-art of the design and verification techniques and methodologies the System on-a-Chip (SoC). The advancement in the hardware area made it possible the integration of a complete yet complex system on a single chip. Over 10 million gates, integrated together and running a real time optimized software red crossed classical design techniques. Traditional Register Transfer level (RTL) will serve as an assembler language for the new design languages or so called system level languages. A challenge facing the SoC designers is to decide which system level language we have to use and how the verification task will be accomplished. This report presents the main proposals in defining a system level language and discusses the eventual verification techniques that can be used.

A. Habibi and S. Tahar: A Survey: System-on-a-Chip Design and Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, January 2003. [32 pages]

Send comments and suggestions to: habibi@ece.concordia.ca


 



Thesis


Ali Habibi: A Framework for System Level Verification: The SystemC Case. Ph.D. Thesis, Electrical Engineering. Concordia University, Department of Electrical and Computer Engineering, November 2005.