Abstract
Establishing the correctness of complicated asynchronous circuit is in general quite difficult because of the high degree of nondeterminism that is inherent in such devices. Nevertheless, it is also very important in view of the cost involved in design and testing of circuits. We show how to give specifications for circuits in a branching time temporal logic and how to mechanically verify them using a simple and efficient model checker. We also show how to tackle a large and complex circuit by verifying it hierarchically.
This research was partially supported by NSF Grant Number MCS-8216706.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
7. References
G. V. Bochmann, “Hardware Specification with Temporal Logic: An Example”, IEEE Transactions on Computers, Vol C-31,No. 3, March 1982.
M. Ben-Ari, Z. Manna and A. Pnueli, “The Logic of Nexttime”, Eighth ACM Symposium on Principle of Programming Languages, Williamsburg, VA, January 1981.
E. M. Clarke, E. A. Emerson and A. P. Sistla, “Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications: A Practical Approach”, Tenth ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1983.
E. A. Emerson, E. M. Clarke, “Characterizing Properties of Parallel Programs as Fixpoints”, Proceedings of the Seventh International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science No. 85, Springer Verlag, 1981.
A. Ginzburg, Algebraic Theory of Automata, Academic Press, New York. London, 1968.
J. Halpern, Z. Manna and B. Moszkowski, “A Hardware Semantics based on Temporal Intervals”, Report No. STAN-CS-83-963, Department of Computer Science, Stanford University, Stanford University, Stanford, CA 94305, March 1983.
C. A. Mead and L. A. Conway, Introduction to VLSI System, Reading, MA, Addison-Wesley, 1980, Ch. 7.
B. Mishra and E. Clarke, “Automatic Verification of Asynchronous Circuits”, C.-M. U. Tech Report, 1983. (To Appear)
R. Miluer, A Calculus of Communicating Systems, University of Edinburgh, June 1980.
Y. Malchi and S. S. Owicki, “Temporal Specifications of Self-Timed Systems”, in VLSI Systems and Computations (Ed. II. T. Kung, Bob Sproull, and G. Steele), Computer Science Press, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clarke, E., Mishra, B. (1984). Automatic verification of asynchronous circuits. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_358
Download citation
DOI: https://doi.org/10.1007/3-540-12896-4_358
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12896-0
Online ISBN: 978-3-540-38775-6
eBook Packages: Springer Book Archive