Habibi, Ali and Tahar, Sofiène (2005) On the Transformation of SystemC to AsmL Using Abstract Interpretation. Electronic Notes in Theoretical Computer Science, 131 . pp. 39-49. ISSN 15710661
Preview |
Text (application/pdf)
136kBENTCS-2005.pdf - Accepted Version |
Official URL: http://dx.doi.org/10.1016/j.entcs.2005.01.021
Abstract
SystemC is among a group of system level design languages proposed to raise the abstraction level for embedded system design and verification. A straight and sound verification by model checking or theorem proving of SystemC designs is, however, infeasible given the object-oriented nature of this library and the complexity of its simulation environment. We illustrated, in a previous work, the feasibility and success of performing model checking and assertions monitors generation of SystemC using a variant of Abstract State Machines (ASM) languages (AsmL). In this paper, we establish the soundness of our approach by proving the correctness of the transformation from SystemC to AsmL.
| 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: | Electronic Notes in Theoretical Computer Science |
| Date: | 2005 |
| Digital Object Identifier (DOI): | 10.1016/j.entcs.2005.01.021 |
| Keywords: | abstract interpretation; formal verification; systemc |
| ID Code: | 977381 |
| Deposited By: | Danielle Dennie |
| Deposited On: | 14 Jun 2013 15:43 |
| Last Modified: | 18 Jan 2018 17:44 |
References:
[1]Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
[2]
Patrick Cousot , Radhia Cousot, Systematic design of program transformation frameworks by abstract interpretation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.178-190, January 16-18, 2002, Portland, Oregon [doi>10.1145/503272.503290]
[3]
Yuri Gurevich, Evolving algebras 1993: Lipari guide, Specification and validation methods, Oxford University Press, Inc., New York, NY, 1995
[4]
Ali Habibi , Sofiene Tahar, Design for Verification of SystemC Transaction Level Models, Proceedings of the conference on Design, Automation and Test in Europe, p.560-565, March 07-11, 2005 [doi>10.1109/DATE.2005.112]
[5]
A. Habibi and S. Tahar. AsmL fixpoint semantics. Technical report, Department of ECE, Concordia University, December 2004
[6]
A. Habibi and S. Tahar. SystemC fixpoint semantics. Technical report, Department of ECE, Concordia University, December 2004
[7]
F. Logozzo. Analyse Statique Modulaire de Langages à Objets. PhD thesis, Ecole Polytechnique, Paris, France, June 2004
[8]
Microsoft Corp. AsmL for Microsoft .NET framework, 2004
[9]
Müller, W., Ruf, J. and Rosenstiel, W., SystemC Methodologies and Applications. 2003. Kluwe Academic Pub.
[10]
Peter D. Mosses, Denotational semantics, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
[11]
http://www.systemc.org
[12]
K. Oumalou, A. Habibi, and S. Tahar. Design for verification of a PCI bus in SystemC. In Symposium on System-on-Chip, Finland, November 2004
[13]
Ashraf Salem, Formal Semantics of Synchronous SystemC, Proceedings of the conference on Design, Automation and Test in Europe, p.10376, March 03-07, 2003
Repository Staff Only: item control page
Download Statistics
Download Statistics