Revolutionary system specification languages now allow integration of processors, memory, OS, sensors, and networking into a single System-on-Chip (SoC). We propose an SoC verification framework for Transaction Level Modeling (TLM) based on the SystemC system level language and using static analysis to simplify designs, improving model checking and assertion-based verification. For model checking, a reduced model is first translated to AsmL (Abstract State Machines Language) and checked against properties written in PSL (Property Specification Language). Using Microsoft Research’s Asmlt tool, AsmL code can be compiled to C# or linked to the .NET framework. PSL properties are defined directly in AsmL. When model checking fails due to state explosion, we switch to assertion-based verification: PSL assertions are compiled into C# modules and integrated into the SystemC design, and verified by simulation. The transformation from AsmL to SystemC has been formally proven using trace semantics. Our framework has yielded promising results on SystemC TLMs of commercial designs like the PCI bus, look-aside interface (LA-1), and AGP bus, and was compared with tools such as IBM RuleBase and Cadence FormalCheck.
Publications
Thesis
[1] Amjad Gawanmeh, "On the Formal Verification of Group Key security Protocols , PhD Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2008.
[2] Amer Samarah, Automated Coverage Directed Test Generation Using a Cell-Based Genetic Algorithm, MASc Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2006.
[3] Haja Moinudeen, Design for Verification of a PCI-X Bus Model , MASc Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, February 2006.
[4] Ali Habibi, A Framework for System Level Verification, The SystemC Case , PhD Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, November 2005.
[5] Amjad Gawanmeh, Interfacing Abstract State Machines with Miltiway Decision Graphs, MASc Thesis, Concordia University, Department of Electrical and Computer Engineering, April 2003.
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
[1] A. Habibi and S. Tahar: SystemC fixpoint semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [15 pages]
[2] A. Habibi and S. Tahar: A Survey: AsmL fixpoint semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [18 pages].
[3] 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].
[4] 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]
[5] 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].
[6] 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]
Applications
- Look-Aside Interface (LA1-B).
- PCI Bus.
- PCI-X Bus.
- AGP Bus.
- Packet Switch (from SystemC library).
- Master/Slave Model (from SystemC library).