Abstract
Model checking is an automated approach to the formal verification of hardware and software. To allow model checking tools to be used by the hardware or software designers themselves, instead of by veri.cation experts, the tools should support speci.cation methods that correspond closely to the common usage. For hardware systems, timing diagrams form such a commonly used and visually appealing specification method. In this paper, we introduce a class of synchronous timing diagrams with a syntax and a formal semantics that is close to the informal usage. We present an e.cient, decompositional algorithm for model checking such timing diagrams. This algorithm has been implemented in a user-friendly tool called RTDT (the Regular Timing Diagram Translator). We have applied this tool to verify several properties of Lucent's PCI synthesizable core.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
N. Amla and E.A. Emerson. Regular Timing Diagrams. In LICS Workshop on Logic and Diagrammatic Information, June 1998.
N. Amla, E.A. Emerson, and K.S. Namjoshi. Efficient Decompositional Model Checking for Regular Timing Diagrams. In CHARME. Springer-Verlag, September 1999.
T. Amon, G. Borriello, T. Hu, and J. Liu. Symbolic Timing Verification of Timing Diagrams Using Presburger Formulas. In DAC, 1997.
Bell Laboratories, Lucent Technologies. PCI Core User’s Manual (Version 1.0). Technical report, July 1996.
A. Benveniste. Safety Critical Embedded Systems Design: the SACRES approach. Technical report, INRIA, May 1998. URL: http://www.tni.fr/sacres/index.html
R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS. In FMCAD, 1996.
U. Brockmeyer and G. Wittich. Tamagotchis need not die-Veri.cation of STATEMATE Designs. In TACAS. Springer-Verlag, March 1998.
E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In Workshop on Logics of Programs, volume 131. Springer Verlag, 1981.
E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic. ACM Transactions on Programming Languages and Systems, 8(2), 1986.
W. Damm, B. Josko, and Rainer Schlör. Specification and Verification of VHDLbased System-level Hardware Designs. In Egon Borger, editor, Specification and Validation Methods. Oxford University Press, 1994.
K. Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, August 1996.
K. Fisler. Containment of Regular Languages in Non-Regular Timing Diagrams Languages is Decidable. In CAV. Springer Verlag, 1997.
W. Grass, C. Grobe, S. Lenk, W. Tiedemann, C.D. Kloos, A. Marin, and T. Robles. Transformation of Timing Diagram Speci.cations into VHDL Code. In Conference on Hardware Description Languages, 1995.
R.H. Hardin, Z. Har'El, and R.P. Kurshan. COSPAN. In CAV, volume 1102, 1996.
K. Kastein and M. McClure. Timing Designer use for Interface Verification at Symbios Logic. Integrated System Design, May 1997. URL: http://www.chronology.com
K. Khordoc and E. Cerny. Semantics and Verification of Timing Diagrams with Linear Timing Constraints. ACM Transactions on Design Automation of Electronic Systems, 3(1), 1998.
R.P. Kurshan. Computer-aided verification of coordinating processes: the Automata-theoretic approach. Princeton University Press, 1994.
O. Lichtenstein and A. Pnueli. Checking that Finite State Concurrent Programs satisfy their Linear Specifications. In POPL, 1985.
K. Luth. The ICOS Synthesis Environment. In Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998. au]20._Z. Manna and A. Pnueli. Speci.cation and Veri.cation of Concurrent Programs by ∨-Automata. In POPL, 1987.
K.L. McMillan. Symbolic Model Checking. Kluwer Academic Press, 1993.
D. Mitchell. Test Bench Generation from Timing Diagrams. In David Pellerin, editor, VHDL Made Easy. 1996. URL: http://www.syncad.com
PCI Special Interest Group. PCI Local Bus Speci.cation Rev 2.1. Technical report, June 1995.
J.P. Queille and J. Sifakis. Specification and Verification of Concurrent Systems in CESAR. In Proc. of the 5th International Symposium on Programming, volume 137 of LNCS, 1982.
M. Vardi. Verification of Concurrent Programs. In POPL, 1987.
M. Vardi and P. Wolper. An Automata-theoretic Approach to Automatic Program Verification. In LICS, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amla, N., Emerson, E.A., Kurshan, R.P., Namjoshi, K.S. (2002). Model Checking Synchronous Timing Diagrams. In: Hunt, W.A., Johnson, S.D. (eds) Formal Methods in Computer-Aided Design. FMCAD 2000. Lecture Notes in Computer Science, vol 1954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40922-X_18
Download citation
DOI: https://doi.org/10.1007/3-540-40922-X_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41219-9
Online ISBN: 978-3-540-40922-9
eBook Packages: Springer Book Archive