Logic of Programs 1983: Logics of Programs pp 101-115 | Cite as

Automatic verification of asynchronous circuits

  • E. Clarke
  • B. Mishra
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 164)


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.


Model Checker Temporal Logic Signalling Scheme Atomic Proposition Kripke Structure 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

7. References

  1. [BO82]
    G. V. Bochmann, “Hardware Specification with Temporal Logic: An Example”, IEEE Transactions on Computers, Vol C-31,No. 3, March 1982.Google Scholar
  2. [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
  3. [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
  4. [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
  5. [GI68]
    A. Ginzburg, Algebraic Theory of Automata, Academic Press, New York. London, 1968.Google Scholar
  6. [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
  7. [MC80]
    C. A. Mead and L. A. Conway, Introduction to VLSI System, Reading, MA, Addison-Wesley, 1980, Ch. 7.Google Scholar
  8. [MC83]
    B. Mishra and E. Clarke, “Automatic Verification of Asynchronous Circuits”, C.-M. U. Tech Report, 1983. (To Appear)Google Scholar
  9. [MI80]
    R. Miluer, A Calculus of Communicating Systems, University of Edinburgh, June 1980.Google Scholar
  10. [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

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • E. Clarke
    • 1
  • B. Mishra
    • 1
  1. 1.Department of Computer ScienceCarnegie-Mellon UniversityPittsburgh

Personalised recommendations