Abstract
Timing diagrams are widely used in industrial practice to express precedence and timing relationships amongst a collection of signals. This graphical notation is often more convenient than the use of temporal logic or automata. We introduce a class of timing diagrams called Regular Timing Diagrams (RTD’s). RTD’s have a precise syntax, and a formal semantics that is simple and corresponds to common usage. Moreover, RTD’s have an inherent compositional structure, which is exploited to construct an efficient algorithm for model checking a RTD with respect to a system description. The algorithm has time complexity that is linear in the system size and a small polynomial in the representation of the diagram. The algorithm can be easily used with symbolic (BDDbased) model checkers. We illustrate the workings of our algorithm with the verification of a simple master-slave system.
Acknowledgments
We would like to thank Bob Kurshan, Kathi Fisler and Steve Keckler for helpful discussions and insightful comments.
This work was supported in part by NSF grants CCR 941-5496, CCR 980-4736 and SRC Contract 98-DP-388.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C. Antoine and B. Le Goff. Timing Diagrams for Writing and Checking Logical and Behavioral Properties of Integrated Systems. In Correct Hardware Design Methodologies. Elsevier Sciences Publishers, 1992.
G. Borriello. Formalized Timing Diagrams. In EDAC92. IEEE Comput. Soc. Press, 1992.
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.
V. Cingel. A Graph-based Method for Timing Diagrams Representation and Verification. In Correct Hardware Design and Verification Methods. Springer Verlag, 1993.
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 and J. Helbig. Linking Visual Formalisms: A Compositional proof System for Statecharts cased on Symbolic Timing Diagrams. In E. R. Olderog, editor, Programming Concepts, Methods and Calculi. Elsevier Science B. V. (North Holland), 1994.
W. Damm, H. Hunger, P. Kelb, and R. Schlör. Using Graphical Specification Languages and Symbolic Model Checking in the Verification of a Production Cell. In C. Lewerentz and T. Lindner, editors, Formal Development of Reactive Systems. Case Study Production Cell, LNCS 891. Springer Verlag, 1994.
W. Damm, B. Josko, and Rainer Schlör. Specification and Verification of VHDLbased System-level Hardware Designs. In Egon Borger, editor, Specificatio and Validation Methods. Oxford University Press, 1994.
K. Feyerabend. Real-time Symbolic Timing Diagrams. Technical report, Department of Computer Science, Oldenburg University, September 1994.
K. Feyerabend and B. Josko. A Visual Formalism for Real Time Requirement Specifications. In AMAST Workshop on Real-time systems and Concurrent and Distributed Software. Springer Verlag, 1997.
K. Feyerabend and R. Schlör. Hardware synthesis from requirement specifications. In EURO-DAC'96 with EURO-VHDL'96. IEEE Computer Society Press, September 1996.
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 Specifications into VHDL Code. In Conference on Hardware Description Languages, 1995.
J. Helbig, R. Schlör, W. Damm, G. Doehmen, and P. Kelb. VHDL/S-I ntegrating Statecharts, Timing diagrams, and VHDL. Microprocessing and Microprogramming, 1996.
F. Jin and E. Cerny. Verification of Real-Time Controllers against Timing Diagram Specifications using Constraint Logic Programming. In IFIP EuroMICRO, 1998.
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.
Z. Manna and A. Pnueli. Specification and Verification of Concurrent Programs by ∀-Automata. In POPL, 1987.
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.
Y. S.. Ramakrishna, P. M. Melliar-Smith, L. E. Moser, L. K. Dillon, and G. Kutty. Really Visual Temporal Reasoning. In Real-Time Systems Symposium. IEEE Publishers, 1993.
R. Schlör. A Prover for VHDL-based Hardware Design. In Conference on Hardware Description Languages, 1995.
A. P. Sistla, M. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with Applications to Temporal Logic. TCS, 49, 1987.
E. M. Thurner. Proving System Properties by means of Trigger-Graph and Petri Nets. In EUROCAST. Springer Verlag, 1996.
W. D. Tiedemann. Bus Protocol Conversion: from Timing Diagrams to State Machines. In EUROCAST. Springer Verlag, 1992.
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
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amla, N., Emerson, E.A., Namjoshi, K.S. (1999). Efficient Decompositional Model Checking for Regular Timing Diagrams. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_7
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive