Habibi, Ali and Tahar, Sofiène (2006) Design and verification of SystemC transaction-level models. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 14 (1). pp. 57-68. ISSN 1063-8210
Preview |
Text (application/pdf)
290kBTVLSI-2006.pdf - Accepted Version |
Official URL: http://dx.doi.org/10.1109/TVLSI.2005.863187
Abstract
Transaction-level modeling allows exploring several SoC design architectures, leading to better performance and easier verification of the final product. In this paper, 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 Property Specification language) in Unifed Modeling Language (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 a finite state machine of the design, including the properties. Checking the correctness of the properties is performed on the fly while generating the state machine. 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. For existing SystemC designs, we propose to translate the code back to AsmL in order to apply the same verification approach. 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.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering |
|---|---|
| Item Type: | Article |
| Refereed: | Yes |
| Authors: | Habibi, Ali and Tahar, Sofiène |
| Journal or Publication: | IEEE Transactions on Very Large Scale Integration (VLSI) Systems |
| Date: | 2006 |
| Digital Object Identifier (DOI): | 10.1109/TVLSI.2005.863187 |
| Keywords: | SystemC system-level design system-level verification transaction-level modeling |
| ID Code: | 977376 |
| Deposited By: | Danielle Dennie |
| Deposited On: | 14 Jun 2013 15:19 |
| Last Modified: | 18 Jan 2018 17:44 |
References:
Accellera Property Specification Language Reference Manual, 2004 [online] Available:<item>http://www.accellera.org</item>
P. Cousot and R. Cousot, "Systematic design of program analysis frameworks", Proc. Symp. Principles Programming Languages, pp.269 -282 1979
P. Cousot and R. Cousot, "Abstract interpretation frameworks", J. Logic Computat., vol. 2, no. 4, pp.511 -547 1992
P. Cousot and R. Cousot, "Systematic design of program transformation frameworks by abstract interpretation", Proc. Symp. Principles Programming Languages, pp.178 -190 2002
R. Damasevicius and V. Stuikys, "Application of UML for hardware design based on design process model", Proc. Asia South Pacific Design Automat. Conf., pp.244 -249 2004
P. Godefroid and S. Khurshid, "Exploring very large state spaces using genetic algorithms", Proc. Tools Algorithms Construction Anal. Syst., 2002
M. Gordon, "Validating the PSL/Sugar semantics using automated reasoning", Proc. Formal Aspects Comput., pp.306 -421 2003
M. Gordon and T. Melham, Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic, 1993 :Cambridge Univ. Press
PCI Special Interest Group, 2004 [online] Available:
<item> http://www.pcisig.com/</item>
Y. Gurevich, "Evolving algebras 1993: Lipari guide", Specification and Validation Methods, pp.9 -36 1995 :Oxford Univ. Press
A. Habibi, A. I. Ahmed, O. A. Mohamed, and S. Tahar, "On the design and verification of the look-aside interface", Proc. Design Automat. Test Europe, vol. 3, pp.290 -295 2005
A. Habibi, A. Gawanmeh, and S. Tahar, "Assertion based verification of PSL for SystemC designs", Proc. IEEE Int. Symp. System-on-Chip, pp.177 -180 2004
A. Habibi and S. Tahar, "Design for verification of SystemC transaction level models", Proc. Design Automat. Test Europe, vol. 1, pp.560 -565 2005
A. Habibi and S. Tahar, "Toward an efficient assertion based verification of SystemC designs", Proc. 9th Int. High Level Design Validation Test Workshop, pp.19 -22 2004
A. Habibi and S. Tahar, SystemC Fixpoint Semantics, 2004 :Dept. Elect. Comput. Eng., Concordia Univ. [online] Available:
<item>www.ece.concordia.ca/~habibi/techrp/TR0401/ </item>
A. Habibi and S. Tahar, AsmL Fixpoint Semantics, 2004 :Dept. Elect. Comput. Eng., Concordia Univ. [online] Available:
<item>www.ece.concordia.ca/!habibi/techrp/TR0402/ </item>
A. Habibi and S. Tahar, Abstract Interpretation of SystemC Designs, 2004 :Dept. Elect. Comput. Eng., Concordia Univ.
A. Habibi and S. Tahar, "On the transformation of SystemC to AsmL using abstract interpretation", Electronic Notes Theoret. Computer Sci., vol. 131, pp.39 -49 2005
A. Habibi, S. Tahar, and L. Halleb, "Formal verification of a bus structure modeled in SystemC", Proc. 2nd Annu. IEEE Northeast Workshop Circuits Syst., pp.61 -64 2004
J. Holland, Adaptation in Natural and Artificial Systems, 1975 :Univ. Michigan Press
RuleBase Formal Verification Tool (Version 1.5). User',s Guide, 2003
F. Logozzo, Anhalyze statique modulaire de langages a objets, 2004 :Math. Comput. Scie. Dept., Ecole Polytechnique
AsmL for Microsoft .NET Framework, [online] Available:
<item>research.microsoft.com</item>
W. Mü,ller, J. Ruf, and W. Rosenstiel, SystemC Methodologies and Applications, 2003 :Kluwer
Denotational Semantics, Volume B of Handbook of Theoretical Computer Science, pp.575 -631 1990 :Elsevier Science B.V.
Look-Aside (LA-1) Interface, Implementation Agreement, Revision 1.1, 2004
Open SystemC Initiative, 2004 [online] Available:
<item>http://www.systemc.org </item>
K. Oumalou, A. Habibi, and S. Tahar, "Design for verification of a PCI bus in SystemC", Proc. Symp. System-on-Chip, pp.201 -204 2004
H. Rudin, "Protocol development success stories: Part I", Proc. 12th Int. Symp. Protocol Spec., Testing Verificat., vol. C-8, pp.149 -160 1992
A. Salem, "Formal semantics of synchronous SystemC", Proc. Design, Automat. Test Europe Conf., pp.376 -381 2003
C. Schulz-Key, M. Winterholer, T. Schweizer, T. Kuhn, and W. Rosenstiel, "Object-oriented modeling and synthesis of SystemC specifications", Proc. Conf. Asia South Pacific Design Automation, pp.238 -243 2004
F. Vederine, Analyzes totales de programmes par interpretation abstraite, 2000 :Math. Comput. Sci. Dept., Ecole Polytechnique
Repository Staff Only: item control page
Download Statistics
Download Statistics