Automatic verification of asynchronous circuits
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.
KeywordsModel Checker Temporal Logic Signalling Scheme Atomic Proposition Kripke Structure
Unable to display preview. Download preview PDF.
- [BO82]G. V. Bochmann, “Hardware Specification with Temporal Logic: An Example”, IEEE Transactions on Computers, Vol C-31,No. 3, March 1982.Google Scholar
- [BMP81]M. Ben-Ari, Z. Manna and A. Pnueli, “The Logic of Nexttime”, Eighth ACM Symposium on Principle of Programming Languages, Williamsburg, VA, January 1981.Google Scholar
- [CES83]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.Google Scholar
- [EC80]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.Google Scholar
- [GI68]A. Ginzburg, Algebraic Theory of Automata, Academic Press, New York. London, 1968.Google Scholar
- [HMM83]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.Google Scholar
- [MC80]C. A. Mead and L. A. Conway, Introduction to VLSI System, Reading, MA, Addison-Wesley, 1980, Ch. 7.Google Scholar
- [MC83]B. Mishra and E. Clarke, “Automatic Verification of Asynchronous Circuits”, C.-M. U. Tech Report, 1983. (To Appear)Google Scholar
- [MI80]R. Miluer, A Calculus of Communicating Systems, University of Edinburgh, June 1980.Google Scholar
- [MO81]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.Google Scholar