research-article

Free access

A temporal language for SystemC

Authors:

Moshe Y. Vardi,

Eli SingermanAuthors Info & Claims

FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design

Article No.: 22, Pages 1 - 9

Published: 17 November 2008 Publication History

Abstract

We describe a general approach for defining new temporal specification languages, and adopting existing languages, for SystemC. We define the concept of "underlying trace" describing the execution of a SystemC model, and then define a set of important primitive assertions about the states in the trace. Our framework not only provides additional expressive power for making atomic assertions, but also provides very fine control over the temporal resolution of the language. Using the primitives defined here as clock expression allows sampling at different levels, from transaction-level to the level of individual statements. The advantage of our approach is that it defines important SystemC properties that have been overlooked previously, and also provides a uniform mechanism for specifying the sampling rate of temporal languages.

References

[1]

IEEE Std 1666 - 2005 IEEE Standard SystemC Language Reference Manual, 2006.

[2]

Standard for property specification language (PSL). IEC 62531:2007 (E), pages 1--156, 2007.

[3]

R. Armoni, L. Fix, A. Flaisher, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, E. Singerman, A. Tiemeyer, M. Y. Vardi, and Y. Zbar. The ForSpec temporal logic: A new temporal property-specification logic. In Proc. 8th ICTACAS, volume 2280 of LNCS, pages 296--211, Grenoble, France, April 2002. Springer-Verlag.

Digital Library

[4]

T. Ball and S. Rajamani. SLIC: A specification language for interface checking. Technical report, Microsoft Research, January 2002.

[5]

D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar. The BLAST query language for software verification. In SAS, pages 2--18, 2004.

[6]

A. Bunker, G. Gopalakrishnan, and S. A. McKee. Formal Hardware Specification Languages for Protocol Compliance Verification. ACM Transactions on Design Autom. of Elec. Sys., 9(1):1--32, January 2004.

Digital Library

[7]

L. Burdy, Y. Cheon, D. Cok, M. D. Ernst, J. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of JML tools and applications. Software Tools for Technology Transfer, 7(3):212--232, June 2005.

Digital Library

[8]

L. Charest and E. M. Aboulhamid. A VHDL/SystemC comparison in handling design reuse. In Proceedings of 2002 International Workshop on System-on-Chip for Real-Time Applications, pages 79--85, Banff, Canada, July 2002.

[9]

James C. Corbett, Matthew B. Dwyer, John Hatcliff, and Robby. Expressing checkable properties of dynamic systems: the Bandera Specification Language. STTT, 4(1):34--56, 2002.

[10]

A. Dahan, D. Geist, L. Gluhovsky, D. Pidan, G. Shapir, Y. Wolfsthal, L. Benalycherif, R. Kamdem, and Y. Lahbib. Combining system level modeling with assertion based verification. In ISQED, pages 310--315, 2005.

Digital Library

[11]

R. Drechsler and D. Große. Reachability analysis for formal verification of SystemC. In DSD, pages 337--340, 2002.

Digital Library

[12]

W. Ecker, V. Esen, T. Steininger, M. Velten, and M. Hull. Specification language for transaction level assertions. HLDVT, pages 77--84, 2006.

[13]

W Ecker, V Esen, T Steininger, M Velten, and J Smit. Implementation of a SystemC assertion library, 2005.

[14]

C. Eisner and D. Fisman. A Practical Introduction to PSL (Series on Integrated Circuits and Systems). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006.

Digital Library

[15]

D. Große and R. Drechsler. Formal verification of ltl formulas for SystemC designs. In ISCAS (5), pages 245--248, 2003.

[16]

T. Grotker, S. Liao, G. Martin, and S. Swan. System Design with SystemC. Kluwer Academic Publishers, Norwell, MA, USA, 2002.

Digital Library

[17]

A. Habibi, A. Gawanmeh, and S. Tahar. Assertion based verification of PSL for SystemC designs. In International Symposium on System-on-Chip, pages 177--180, 2004.

[18]

A. Habibi and S. Tahar. On the extension of SystemC by SystemVerilog assertions. Electrical and Computer Engineering, 2004. Canadian Conference on, 4: 1869--1872 Vol. 4, 2--5 May 2004.

[19]

T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with BLAST. In Tenth International Workshop on Model Checking of Software (SPIN), volume LNCS 2648, 2003.

Digital Library

[20]

D. Karlsson, P. Eles, and Z. Peng. Formal verification of SystemC designs using a Petri-net based representation. In DATE '06: Proceedings of the conference on Design, automation and test in Europe, pages 1228--1233, 3001 Leuven, Belgium, Belgium, 2006. European Design and Automation Association.

Digital Library

[21]

A. Kasuya and T. Tesfaye. Verification methodologies in a tlm-to-rtl design flow. In DAC, pages 199--204, 2007.

Digital Library

[22]

D. Kroening and N. Sharygina. Formal verification of SystemC by automatic hardware/software partitioning. In MEMOCODE, pages 101--110, 2005.

Digital Library

[23]

M. Moy, F. Maraninchi, and L. Maillet-Contoz. LusSy: A toolbox for the analysis of systems-on-a-chip at the transactional level. In International Conference on Application of Concurrency to System Design, June 2005.

Digital Library

[24]

M. Moy, F. Maraninchi, and L. Maillet-Contoz. LusSy: an open tool for the analysis of systems-on-a-chip at the transaction level. Design Automation for Embedded Systems, 2006.

Digital Library

[25]

Matthieu Moy. Techniques and Tools for the Verification of Systems-on-a-Chip at the Transaction Level. PhD thesis, INPG, Grenoble, France, December 2005.

[26]

James L. Peterson. Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1981.

Digital Library

[27]

L. Pierre and L. Ferro. A tractable and fast method for monitoring SystemC TLM specifications. IEEE Transactions on Computers, 2008.

Digital Library

[28]

A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foundation of Computer Science, pages 46--57, 1977.

Digital Library

[29]

C. Traulsen, J. Cornet, M. Moy, and F. Maraninchi. A SystemC/TLM semantics in Promela and its possible applications. In 14th Workshop on Model Checking Software SPIN, July 2007.

Digital Library

[30]

M. Y. Vardi. Formal techniques for SystemC verification. In DAC '07: Proceedings of the 44th annual conference on Design automation, pages 188--192, New York, NY, USA, 2007. ACM.

Digital Library

[31]

S. Vijayaraghavan and M. Ramanathan. A Practical Guide for SystemVerilog Assertions. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2005.

[32]

G. Winskel. The formal semantics of programming languages: an introduction. MIT Press, Cambridge, MA, USA, 1993.

Digital Library

Cited By

Zhang HLu Y(2016)SMT-based Bounded Model Checking for Cooperative Software with a Deterministic Scheduler6th International Workshop on Structured Object-Oriented Formal Language and Method - Volume 1018910.1007/978-3-319-57708-1_11(181-200)Online publication date: 15-Nov-2016
https://dl.acm.org/doi/10.1007/978-3-319-57708-1_11
(2014)Assertion-based flow monitoring of SystemC modelsProceedings of the Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2014.6961853(145-154)Online publication date: 1-Oct-2014
https://dl.acm.org/doi/10.1109/MEMCOD.2014.6961853
Chou CChu CHuang CHenkel J(2013)Conquering the scheduling alternative explosion problem of SystemC symbolic simulationProceedings of the International Conference on Computer-Aided Design10.5555/2561828.2561961(685-690)Online publication date: 18-Nov-2013
https://dl.acm.org/doi/10.5555/2561828.2561961
Show More Cited By

Recommendations

A testbench specification language for SystemC verification
CODES+ISSS '12: Proceedings of the eighth IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis

Testing of embedded systems, operating in the real environment, is generally performed by using an industrial test bench that stimulates the system through sensors and human-machine interfaces. The test bench provides the engineers with a set of tools ...
Checkers for SystemC designs
MEMOCODE '04: Proceedings of the Second ACM/IEEE International Conference on Formal Methods and Models for Co-Design

Today's complex systems are modeled on a high level of abstraction. In this context, C/C++-based description languages, like SystemC, become very important. The modeling features of SystemC enable adequate levels of abstraction, hardware/software ...
Monitoring temporal SystemC properties
MEMOCODE '10: Proceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign

Monitoring temporal SystemC properties is crucial for the validation of functional and transaction-level models, yet the current SystemC standard provides no support for temporal specifications. In this work we describe a temporal monitoring framework ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design

November 2008

236 pages

ISBN:9781424427352

Editors:
Alessandro Cimatti
FBK-irst
,
Robert B. Jones
Intel Corporation

Sponsors

CEDA: Council on Electronic Design Automation

Publisher

IEEE Press

Publication History

Published: 17 November 2008

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
79
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)1

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Zhang HLu Y(2016)SMT-based Bounded Model Checking for Cooperative Software with a Deterministic Scheduler6th International Workshop on Structured Object-Oriented Formal Language and Method - Volume 1018910.1007/978-3-319-57708-1_11(181-200)Online publication date: 15-Nov-2016
https://dl.acm.org/doi/10.1007/978-3-319-57708-1_11
(2014)Assertion-based flow monitoring of SystemC modelsProceedings of the Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2014.6961853(145-154)Online publication date: 1-Oct-2014
https://dl.acm.org/doi/10.1109/MEMCOD.2014.6961853
Chou CChu CHuang CHenkel J(2013)Conquering the scheduling alternative explosion problem of SystemC symbolic simulationProceedings of the International Conference on Computer-Aided Design10.5555/2561828.2561961(685-690)Online publication date: 18-Nov-2013
https://dl.acm.org/doi/10.5555/2561828.2561961
Le HGroße DHerdt VDrechsler R(2013)Verifying SystemC using an intermediate verification language and symbolic simulationProceedings of the 50th Annual Design Automation Conference10.1145/2463209.2488877(1-6)Online publication date: 29-May-2013
https://dl.acm.org/doi/10.1145/2463209.2488877
Tabakov DVardi MBorchert CHaupt MLohmann DLorenz D(2012)Automatic aspectization of systemCProceedings of the 2012 workshop on Modularity in Systems Software10.1145/2162024.2162029(9-14)Online publication date: 27-Mar-2012
https://dl.acm.org/doi/10.1145/2162024.2162029
Campana DCimatti ANarasamdya IRoveri M(2011)An analytic evaluation of SystemC encodings in PromelaProceedings of the 18th international SPIN conference on Model checking software10.5555/2032692.2032703(90-107)Online publication date: 14-Jul-2011
https://dl.acm.org/doi/10.5555/2032692.2032703
Cimatti AGriggio AMicheli ANarasamdya IRoveri M(2011)KRATOSProceedings of the 23rd international conference on Computer aided verification10.5555/2032305.2032329(310-316)Online publication date: 14-Jul-2011
https://dl.acm.org/doi/10.5555/2032305.2032329
Cimatti ANarasamdya IRoveri M(2011)Boosting lazy abstraction for systemc with partial order reductionProceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software10.5555/1987389.1987430(341-356)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.5555/1987389.1987430
Sen A(2011)Concurrency-oriented verification and coverage of system-level designsACM Transactions on Design Automation of Electronic Systems10.1145/2003695.200369716:4(1-25)Online publication date: 27-Oct-2011
https://dl.acm.org/doi/10.1145/2003695.2003697
Liu LSheridan DAthavale VVasudevan S(2011)Automatic generation of assertions from system level design using data miningProceedings of the Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2011.5970526(191-200)Online publication date: 1-Jul-2011
https://dl.acm.org/doi/10.1109/MEMCOD.2011.5970526
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents