Abstract
Functional verification has traditionally focused on providing tools to generate tests and measuring their so-called coverage. The need to provide the correct reference data has had however relatively little attention. This chapter describes how to apply TLM models as executable functional specifications to generate the compulsory reference data required by functional verification environments. We further explain how these models can be used in conjunction with other verification techniques such as hardware emulators, and how formal verification techniques can be applied to TLM models.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K.L. McMillan, Symbolic Model Checking, Boston: 1993.
R. Drechsler and D. Grosse, “Formal Verification of LTL Formulas for SystemC Designs,” in Proc. of ISCAS, 2003.
[3]_T. Sakunkonchak and M. Fujita, “Verification of Synchronization in SpecC Description with the Use of Difference Decision Diagrams,” in Proc. of the Forum on Specification & Design Languages (FDL’02), 2002.
[4]_E. Clarke and D. Kroening, “Hardware Verification using ANSI-C Programs as a Reference,” in Proc. of ASP-DAC 2003, 2003, pp. 308–311.
[5]_E. Clarke, D. Kroening, and F. Lerda, “A Tool for Checking ANSI-C Programs,” in Proc. of Tools and Algorithms for the Construction and Analysis of Systems Conference (TACAS’04), 2004, pp. 168–176.
T. Ball and S.K. Rajamani, “Boolean Programs: A Model and Process for Software Analysis,” Microsoft Research, Feb 2000.
K. Havelund, “Java PathFinder: A Translator from Java to Promela,” in Proc. of SPIN, 1999, pp. 152.
W. Visser, K. Havelund, G. Brat, and S. Park, “Java PathFinder-Second Generation of a Java Model Checker,” in Proc. of Post-CAV Workshop on Advances in Verification, 2000.
M. Moy, “Pinapa: A SystemC Front-end,” Online Open Source Software and Manual, Available at: http://greensocs.sourceforge.net/pinapa/
N. Halbwachs, F. Lagnier, and C. Ratel, “Programming and Verifying Critical Systems by Means of the Synchronous Data-Flow Programming Language Lustre,” IEEE Transactions on Software Engineering, 1992.
B. Jeannet, “Dynamic Partitioning In Linear Relation Analysis. Application to the Verification of Reactive Systems,” Formal Methods in System Design, vol. 23, no. 1, pp. 5–37, 2003.
L. Lamport, “Proving the Correctness of Multiprocess Programs,” IEEE Transactions on Software Engineering, vol. SE-3, no. 2, pp. 125–143, 1977.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer
About this chapter
Cite this chapter
Bultiaux, T., Guenot, S., Hustin, S., Blampey, A., Bulone, J., Moy, M. (2005). Functional Verification. In: Ghenassia, F. (eds) Transaction Level Modeling with SystemC. Springer, Boston, MA. https://doi.org/10.1007/0-387-26233-4_5
Download citation
DOI: https://doi.org/10.1007/0-387-26233-4_5
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-26232-1
Online ISBN: 978-0-387-26233-8
eBook Packages: EngineeringEngineering (R0)