Gawanmeh, Amjad, Tahar, Sofiène, Moinudeen, Haja and Habibi, Ali (2007) A Design for verification approach using an embedding of PSL in AsmL. Journal of Circuits, Systems and Computers, 16 (06). pp. 859-881. ISSN 0218-1266
Preview |
Text (application/pdf)
259kBJCSC2008.pdf - Accepted Version |
Official URL: http://dx.doi.org/10.1142/S0218126607004052
Abstract
In this paper, we propose to integrate an embedding of Property Specification Language (PSL) in Abstract State Machines Language (AsmL) with a top–down design for verification approach in order to enable the model checking of large systems at the early stages of the design process. We provide a complete embedding of PSL in the ASM language AsmL, which allows us to integrate PSL properties as a part of the design. For verification, we propose a technique based on the AsmL tool that translates the code containing both the design and the properties into a finite state machine (FSM) representation. We use the generated FSM to run model checking on an external tool, here SMV. Our approach takes advantage of the AsmL language capabilities to model designs at the system level as well as from the power of the AsmL tool in generating both C# code and FSMs from AsmL models. We applied our approach on the PCI-X bus standard, which AsmL model was constructed from the informal standard specifications and a subsequent UML model. Experimental results on the PCI-X bus case study showed a superiority of our approach to conventional verification.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering |
|---|---|
| Item Type: | Article |
| Refereed: | Yes |
| Authors: | Gawanmeh, Amjad and Tahar, Sofiène and Moinudeen, Haja and Habibi, Ali |
| Journal or Publication: | Journal of Circuits, Systems and Computers |
| Date: | 2007 |
| Digital Object Identifier (DOI): | 10.1142/S0218126607004052 |
| Keywords: | PSL; abstract state machines; AsmL; model checking; PCI-X bus |
| ID Code: | 977372 |
| Deposited By: | Danielle Dennie |
| Deposited On: | 14 Jun 2013 14:49 |
| Last Modified: | 18 Jan 2018 17:44 |
References:
E. Börger and R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis (Springer-Verlag, 2003).K. Claessen and J. Martensson, Formal Methods in Computer-Aided Design, LNCS 3312 (Springer-Verlag, 2004) pp. 337–351.
K. H. Chang, A PCI-X verification environment using C and Verilog, VLSI Design/CAD Symp. (2003).
M. Chong, A PCI express to PCI-X bridge optimized for performance and area, Master's thesis, Department of Electrical Engineering and Computer Science, Massachussets Institute of Technology (2004).
M. Dwyer, Tool-supported program abstraction for finite-state verification, Int. Conf. Software Engineering (2001) pp. 177–187.
A. Gawanmeh, A. Habibi and S. Tahar, Languages for Formal Specification and Verification, Forum on Specification and Design Languages (2004).
A. Gawanmeh, A. Habibi and S. Tahar, Embedding and verification of PSL using ASM, IEEE Int. Workshop on System-on-Chip (2006) pp. 125–130.
A. Gawanmeh, S. Tahar and K. Winter, J. Syst. Architecture 54, 15 (2008), DOI: 10.1016/j.sysarc.2007.03.007
W. Grieskamp, Software Eng. Notes 27, 112 (2002), DOI: 10.1145/566171.566190
D. Grobe and R. Drechsler, Checkers for SystemC designs, 2nd ACM and IEEE Int. Conf. Formal Methods and Models for Codesign (2004) pp. 171–178.
M. Gordon, J. Hurd and K. Slind, Correct Hardware Design and Verification Methods, LNCS 2860 (Springer-Verlag, 2003) pp. 200–215.
M. Gordon and T. Melham, Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic (Cambridge University Press, Cambridge, UK, 1993).
M. Gordon, Formal Aspects Comput. 15, 406 (2003), DOI: 10.1007/s00165-003-0014-5
Y. Gurevich, Specification and Validation Methods (Oxford University Press, 1995).
Y. Gurevich, B. Rossman and W. Schulte, Semantic essence of AsmL, Technical Report, Microsoft Research, MSR-TR-2004-27, March 2004.
A. Habibi, A framework for system level verification: The SystemC case, PhD thesis, Concordia University, Montreal, Canada (2005).
A. Habibi and S. Tahar, Electron. Notes Theor. Comput. Sci. 131, 39 (2005), DOI: 10.1016/j.entcs.2005.01.021
J. Huggins, Abstract state machines website, http://www.eecs.umich.edu/gasm (2008).
M. L. McMillan, Symbolic Model Checking (Kluwer Academic Publishers, 1993).
H. Moinudeen, A. Habibi and S. Tahar, Design for verification of the PCI-X bus, IEEE Int. Conf. Formal Methods in Computer-Aided Design (IEEE Computer Society Press, 2006) pp. 187–188.
K. Oumalou, A. Habibi and S. Tahar, Design for verification of a PCI bus in SystemC, Symp. System-on-Chip (IEEE Computer Society Press, 2004) pp. 201–204.
PCI Special Interest Group, www.pcisig.com (2005).
Accellera Property Specification Language Reference Manual, Version 1.01, http://www.accellera.org (2008).
K. Shimizu, D. Dill and A. Hu, Formal Methods in Computer-Aided Design, LNCS 1954 (Springer-Verlag, 2000) pp. 335–353.
SystemVerilog, http://www.systemverilog.org (2008).
C. Wallace, Specification and Validation Methods (Oxford University Press, 1995) pp. 131–164.
R. Wang and Z. Wen, A verification environment for PCI-X BFMs in VERA, Technical report, Synopsys Inc. (2002).
K. Winter, Model checking abstract state machines, PhD thesis, Technical University of Berlin, Germany (2001).
C. C. Yu, System level assertion-based verification environment for PCI/PCI-X and PCI-express, VLSI Design/CAD Symp. (2004).
Repository Staff Only: item control page
Download Statistics
Download Statistics