Abstract
Firstly, we show how to deal with bounded uncertain delays of (speed-dependent) asynchronous circuits for symbolic model checking based on temporal logic. We adopt discrete-time model. In the modeling of uncertain delays, we consider two models, i.e. static delay and dynamic delay. These models are interpreted as parameterized sequential machines and nondeterministic sequential machines respecitively.
Secondly, we show a symbolic model checking algorithm for the above sequential machines. As a specification description language, a temporal logic named Branching Time Regular Temporal Logic (BRTL) is employed.
A prototype of verification system based on the proposed method has been implemented and some experimental results are reported.
This research is partially supported by Japan-USA cooperative research sponsored by JSPS and NSF.
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
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. In 10th ACM Symposium on Principles of Programming Languages, pages 117–126, January 1983.
J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of 5th IEEE Symposium on Logic in Computer Science, June 1990.
M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Transactions on Computers, C-35(12):1035–1044, December 1986.
D. L. Dill and E. M. Clarke. Automatic Verification of Asynchronous Circuits Using Temporal Logic. IEE Proceedings, 133:276–282, September 1986.
R. Alur and D. Dill. Automata for Modeling Real-Time Systems. In Proceedings of ICALP 90', 1990.
R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In Proceedings of 5th IEEE Symposium on Logic in Computer Science, pages 414–425, June 1990.
H.R. Lewis. A Logic of Concrete Time Intervals. In Proceedings of 5th IEEE Symposium on Logic in Computer Science, pages 380–389, 1990.
J.S. Ostroff. Automated Verification of Timed Transition Models. Automated Verification Methods for Finite State Systems, pages 247–256, 1989.
O. Coudert, C. Berthet, and J-C. Madre. Verification of Sequential Machines Using Functional Vectors. Proceedings of IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, pages 111–128, November 1989.
K. Hamaguchi and H. Hiraishi and S. Yajima. Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. Workshop on Computer-Aided Verification, June 1990.
Nagisa Ishiura, Yutaka Deguchi, and Shuzo Yajima. Coded Time-Symbolic Simulation Using Shared Binary Decision Diagram. Proceedings of 27th Design Automation Conference, pages 130–135, 1990.
M. Abramovici, M. A. Breuer, and A. D. Freidman. Digital Systems Testing and Testable Design. Computer Science Press, 1990.
Shin ichi Minato, Nagisa Ishiura, and Shuzo Yajima. Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation. Proceedings of 27th Design Automation Conference, pages 52–57, 1990.
R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.
J. R. Burch, E. M. Clarke, and D. E. Long. Representing Circuits More Efficiently in Symbolic Model Checking. Proceedings of 28th Design Automation Conference, June 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamaguchi, K., Hiraishi, H., Yajima, S. (1992). Formal verification of speed-dependent asynchronous circuits using symbolic model checking of Branching Time Regular Temporal Logic. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_38
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive