The Community for Technology Leaders
RSS Icon
Issue No.10 - October (2008 vol.57)
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.
Systems specification methodology, Verification
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, October 2008, doi:10.1109/TC.2008.74
[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,” 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] incisive_ formal_verifier/, 2008.
[11] RB_Home page, 2008.
[12] http://www.averant.comproducts-solidify.html , 2008.
[13] http:/, 2008.
[14] simulation. html, 2008.
[15] incisive_ unified_simulator, 2008.
[16] 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.
592 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool