This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
A Tractable and Fast Method for Monitoring SystemC TLM Specifications
October 2008 (vol. 57 no. 10)
pp. 1346-1356
Laurence Pierre, TIMA, Grenoble
Luca Ferro, TIMA, grenoble
The TLM modeling level of the SystemC language emphasizes the transactions in a complex system, considered at a very high level of abstraction. This level of specification considerably improves simulation performance and is therefore increasingly being adopted. We address assertion-based verification (ABV) of TLM SystemC models. We propose a framework for supervising during simulation the verification of temporal properties expressed in PSL. Very few modifications are needed in the original SystemC code. The TLM specification can be timed or not. The properties can involve several channels, of different types.

[1] R. Dubey, “Elements of Verification,” SOC Central: white paper, Mar. 2005.
[2] M. Glasser, “Applying Transaction-Level Models for Design and Testbenches,” SOC Central, June 2006.
[3] IEEE Std 1666-2005, IEEE Standard System C Language Reference Manual, IEEE, 2005.
[4] T. Grötker, S. Liao, G. Martin, and S. Swan, System Design with SystemC. Kluwer Academic, 2002.
[5] R. Goering, “Transaction Models Offer New Deal for EDA,” EETimes, http://www.eetimes.comshowArticle.jhtml?articleID=181503693 , Mar. 2006.
[6] A. Gupta, “Assertion-Based Verification Turns the Corner,” IEEE Design and Test of Computers, vol. 19, no. 4, July/Aug. 2002.
[7] D. Maliniak, “Assertion-Based Verification Smoothes the Road to IP Reuse,” http://www.elecdesign.com/Articles/ArticleID/ 27482748.html, Sept. 2002.
[8] IEEE Std 1850-2005, IEEE Standard for Property Specification Language (PSL), IEEE, 2005.
[9] IEEE Std 1800-2005, IEEE Standard for System Verilog: Unified Hardware Design, Specification and Verification Language, IEEE, 2005.
[10] http://www.cadence.com/products/functional_ver incisive_ formal_verifier/, 2008.
[11] http://www.haifa.il.ibm.com/projects/verification RB_Home page, 2008.
[12] http://www.averant.comproducts-solidify.html , 2008.
[13] http:/www.model.com/, 2008.
[14] http://www.synopsys.com/products/simulation simulation. html, 2008.
[15] http://www.cadence.com/products/functional_ver incisive_ unified_simulator, 2008.
[16] http://www.haifa.il.ibm.com/projects/verification focs, 2008.
[17] 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,” Proc. Int'l Symp. Quality Electronic Design, 2005.
[18] J. Havlicek and Y. Wolfsthal, “PSL and SVA: Two Standard Assertion Languages Addressing Complimentary Engineering Needs,” Proc. Design Verification Conf., Feb. 2005.
[19] D. Große and R. Drechsler, “Formal Verification of LTL Formulas for SystemC Designs,” Proc. IEEE Int'l Symp. Circuits and Systems, 2003.
[20] A. Habibi and S. Tahar, “Design for Verification of SystemC Transaction Level Models,” Proc. Conf. Design, Automation and Test in Europe, 2005.
[21] 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.
[22] D. Karlsson, P. Eles, and Z. Peng, “Formal Verification of SystemC Designs Using a Petri-Net Based Representation,” Proc. Conf. Design, Automation and Test in Europe, 2006.
[23] B. Niemann and C. Haubelt, “Assertion-Based Verification of Transaction Level Models,” Proc. ITG/GI/GMM Workshop, Feb. 2006.
[24] Y. Lahbib, “Extension of Assertion-Based Verification Approaches for the Verification of SystemC SoC Models,” PhD dissertation, Univ. of Monastir, 2006.
[25] Y. Lahbib, A. Perrin, L. Maillet-Contoz, A. Clouard, F. Ghenassia, and R. Tourki, “Enriching the Boolean and the Modeling Layers of PSL with SystemC and TLM Flavors,” Proc. Forum Specifications and Design Languages, 2006.
[26] W. Ecker, V. Esen, and M. Hull, “Specification Language for Transaction Level Assertions,” Proc. High-Level Design Validation and Test Workshop, 2006.
[27] W. Ecker, V. Esen, and M. Hull, “Implementation of a Transaction Level Assertion Framework in SystemC,” Proc. Conf. Design, Automation and Test in Europe, 2007.
[28] D. Black and J. Donovan, SystemC: From the Ground Up. Springer, 2004.
[29] N. Bombieri, F. Fummi, G. Pravadelli, and A. Fedeli, “Hybrid, Incremental Assertion-Based Verification for TLM Design Flows,” IEEE Design and Test of Computers, vol. 24, no. 2, Mar.-Apr. 2007.
[30] K. Morin-Allory and D. Borrione, “Proven Correct Monitors from PSL Specifications,” Proc. Conf. Design, Automation and Test in Europe, 2006.
[31] K. Morin-Allory and D. Borrione, “On-Line Monitoring of Properties Built on Regular Expressions,” Proc. Forum Specifications and Design Languages, 2006.
[32] L. Pierre, “A Model for Assertion-Based Verification of TLM Designs,” TIMA Laboratory Research Report TIMA-RR-07/09-01-FR, Sept. 2007.
[33] E. Gamma, R. Helm, R. Johnson, and J. Vlissides, Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, 1995.
[34] Y. Oddos, K. Morin-Allory, and D. Borrione, “On-Line Vector Generation from Temporal Constraints Written in PSL,” Proc. 14th IFIP Int'l Conf. Very Large Scale Integration and System-on-Chip, Oct. 2006.

Index Terms:
Systems specification methodology, Verification
Citation:
Laurence Pierre, Luca Ferro, "A Tractable and Fast Method for Monitoring SystemC TLM Specifications," IEEE Transactions on Computers, vol. 57, no. 10, pp. 1346-1356, Oct. 2008, doi:10.1109/TC.2008.74
Usage of this product signifies your acceptance of the Terms of Use.