A system model for formal verification of TLM based transaction properties

ABSTRACT

Verifying functional models is state of the art in the electronic design automation (eda) industry. Improved methods enable the application in industry sized projects. These methods basically work on a detailed state model, properties must be expressible on states. On system level, behavior is expressed in terms of (timed) transactions between functional or architectural artifacts of the design. While recent model checking methods use some workarounds to map transaction models onto state models, we present an alternative approach with an extended system model to verify transaction properties.

REFERENCES

• 1: Charles S. Wasson, System Analysis, Design, and Development: Concepts, Principles, and Practices (Wiley Series in Systems Engineering and Management), Wiley-Interscience, 2005
• 2: Frank Ghenassia, Transaction-Level Modeling with Systemc: Tlm Concepts and Applications for Embedded Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 2006
• 3: Department of EECS, UC B.: Official Homepage of the Ptolemy Project. UC Bercley, EECS, 2006. - http://ptolemy.eecs.berkeley.edu/
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: Thomas Kropf, Introduction to Formal Hardware Verification: Methods and Tools for Designing Correct Circuits and Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
• 6: Pacholik, A.; Fengler, W.; Salzwedel, H.; Vinogradov, O.: Real Time Constraints in System Level Specifications Improving the Verification Flow of Complex Systems. In: Net.ObjectDays 2005 (2005), September
• 7: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 8: Department of Information Technology, Sweden: Official Homepage of the Uppaal Tool. Department of Information Technology, Uppsala University, Sweden, 2006. - http://www.uppaal.com
• 9: Davis, R.; Alla, H.: Discrete, Continous, and Hybrid Petri Nets. Springer-Verlag Berlin Heidelberg, 2005. - ISBN 3-540-22480-7
• 10: Berthomieu, Bernard: Official Homepage of the TINA Toolbox. LAAS-CNRS, france, 2006. - http://www.laas.fr/tina
• 11: Chaochen Zhou , Michael R. Hansen, Duration Calculus: A Formal Approach to Real-Time Systems (Monographs in Theoretical Computer Science. an Eatcs Seris), SpringerVerlag, 2004
• 12: Hummel, Thorsten; Fengler, Wolfgang: Design of Embedded Control Systems Using Hybrid Petri Nets and Time Interval Petri Nets. In: Design of Embedded Control Systems (2005), S. 141--154. ISBN 0-387-23630-9

INDEX TERMS

Keywords:
Petri nets, discrete event systems, formal verification, temporal logic