Skip to main content
SpringerLink
Log in

Formal hardware verification methods: A survey

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Growing advances in VLSI technology have led to an increased level of complexity in current hardware systems. Late detection of design errors typically results in higher costs due to the associated time delay as well as loss of production. Thus it is important that hardware designs be free of errors. Formal verification has become an increasingly important technique towards establishing the correctness of hardware designs. In this article we survey the research that has been done in this area, with an emphasis on more recent trends. We present a classification framework for the various methods, based on the forms of the specification, the implementation, and the proff method. This framework enables us to better highlight the relationships and interactions between seemingly different approaches.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

Other Surveys

  1. P. Camurati and P. Prinetto. Formal verification of hardware correctness: Introduction and survey of current research. Computer, 21 (7):8–19 (July 1988).

    Google Scholar 

  2. E.M. Clarke and O. Grumberg. Research on automatic verification of finite-state concurrent systems. Annual Review of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 2:269–290 (1987).

    Google Scholar 

  3. A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Current Trends in Concurrency, J.W. de Bakker, W.-P. de Roever, and G. Rozenberg (eds.), volume 224 of Lecture Notes in Computer Science, Springer-Verlag, New York, 1986, pp. 510–584.

    Google Scholar 

  4. M. Yoeli. Formal Verification of Hardware Design. IEEE Computer Society Press, Los Alamitos, CA, 1990.

    Google Scholar 

Logic

  1. J. Barwise (ed.). Handbook of Mathematical Logic. North-Holland, Amsterdam, 1977.

    Google Scholar 

  2. D. Gabbay and F. Guenthner (eds.). Handbook of Philosophical Logic, volumes 1, 2, and 3. D. Reidel, Boston, 1983.

    Google Scholar 

  3. W.S. Hatcher. The Logical Foundations of Mathematics. Pergamon Press, Oxford, England, 1982.

    Google Scholar 

  4. G. Hunter. Metalogic: An Introduction to Metatheory of Standard First Order Logic. University of California Press, Berkeley, 1971.

    Google Scholar 

  5. E. Mendelson. Introduction to mathematical Logic. Van Nostrand, New York, 1964.

    Google Scholar 

First-Order Logic

  1. D.L. Beatty, R.E. Bryant, and C.-J.H. Seger. Synchronous circuit verification by symbolic simulation: An illustration. In Proceedings of the Sixth MIT Conference on Advanced Research in VLSI, W.J. Dally (ed.), MIT Press, Cambridge, 1990, pp. 98–112.

    Google Scholar 

  2. S. Bose and A.L. Fisher. Verifying pipelined hardware using symbolic logic simulation. In Proceedings of the IEEE International Conference on Computer Design, IEEE Computer Society Press, Silver Spring, MD, 1989, pp. 217–221.

    Google Scholar 

  3. R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691 (August 1986).

    Google Scholar 

  4. R.E. Bryant. Algorithmic aspects of symbolic switch network analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 6(4):618–633 (July 1987).

    Google Scholar 

  5. R.E. Bryant. A methodology for hardware verification based on logic simulation. Technical Report CMU-CS-87–128, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, June 1987.

    Google Scholar 

  6. R.E. Bryant. Symbolic analysis of VLSI circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 6(4):634–649 (July 1987).

    Google Scholar 

  7. R.E. Bryant. Verifying a static RAM design by logic simulation. In Proceedings of the Fifth MIT Conference on Advanced Research in VLSI, J. Allen and F.T. Leighton (eds.). MIT Press, Cambridge, 1988, pp. 335–349.

    Google Scholar 

  8. R.E. Bryant, D. Beatty, K. Brace, K. Cho, and T. Sheffler. COSMOS: A compiled simulator for MOS circuits. In Proceedings of the 24th ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, June 1987, pp. 9–16.

    Google Scholar 

  9. J.A. Darringer. The application of program verification techniques to hardware verification. In Proceedings of the Sixteenth ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, June 1979, pp. 375–381.

    Google Scholar 

  10. R.W. Floyd. Assigning meaning to programs. Proceedings of Symposia in Applied Mathematics: Mathematical Aspects of Computer Science, 19:19–31 (1967).

    Google Scholar 

  11. M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, San Francisco, 1979.

    Google Scholar 

  12. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12:576–580 (1969).

    Google Scholar 

  13. C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271–281 (1972).

    Google Scholar 

  14. Z. Kohavi. Swtiching and Finite Automata Theory. McGraw-Hill, New York, 1978.

    Google Scholar 

  15. R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1980.

    Google Scholar 

  16. E.F. Moore. Gedanken-experiments on sequential machines. In Automata Studies, C.E. Shannon (ed.), Princeton University Press, Princeton, NJ, 1956, pp. 129–153.

    Google Scholar 

  17. R.E. Shostak. Formal verification of circuit designs. In Proceedings of the Sixth International Symposium on Computer Hardware Description Languages and their Applications, T. Uehara and M. Barbacci (eds.). IFIP, North-Holland, Amsterdam, 1983.

    Google Scholar 

Boyer-Moore Logic

  1. W.R. Bevier. Kit and the short stack. Journal of Automated Reasoning, 5(4):519–530 (1989).

    Google Scholar 

  2. W.R. Bevier, W.A. HuntJr., J.S. Moore, and W.D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411–428 (1989).

    Google Scholar 

  3. R.S. Boyer and J.S. Moore. Proof-checking, theorem-proving and program verification. Contemporary Mathematics, 29:119–132 (1984).

    Google Scholar 

  4. R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, Boston, 1988.

    Google Scholar 

  5. A. Bronstein and C.L. Talcott. String-functional semantics for formal verification of synchronous circuits. Technical Report 1210, Stanford University, Stanford, CA, 1988.

    Google Scholar 

  6. A. Bronstein and C.L. Talcott. Formal verification of synchronous circuits based on string-functional semantics: The 7 Paillet circuits in Boyer-Moore. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 317–333.

    Google Scholar 

  7. S.M. German and Y. Wang. Formal verification of parameterized hardware designs. In Proceedings of the IEEE International Conference on Computer Design, IEEE Computer Society Press, Silver Spring, MD, 1985, pp. 549–552.

    Google Scholar 

  8. W.A. Hunt, Jr. FM 8501: A verified microprocessor. Ph.D. thesis, Technical Report ICSCA-CMP-47, University of Texas at Austin, 1985.

  9. W.A. HuntJr. The mechanical verification of a microprocessor design. In From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (ed.). North-Holland, Amsterdam, 1987, pp. 89–129.

    Google Scholar 

  10. W.A. HuntJr. Micropocessor design verification. Journal of Automated Reasoning, 5(4):429–460 (1989).

    Google Scholar 

  11. J.S. Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461–492 (1989).

    Google Scholar 

  12. W.D. Young. A mechanically verified code generator. Journal of Automated Reasoning, 5(4):493–518 (1989).

    Google Scholar 

Higher-Order Logic

  1. H.G. Barrow. Proving the correctness of digital hardware designs. VLSI Design, 5:64–77 (July 1984).

    Google Scholar 

  2. A.J. Camilleri, M.J.C. Gordon, and T.F. Melham. Hardware verification using higher-order logic. In From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (ed.). North-Holland, Amserdam, 1987, pp. 43–67.

    Google Scholar 

  3. W.F. Clocksin and C.S. Mellish. Programming in Prolog. Springer-Verlag, New York, 1981.

    Google Scholar 

  4. A. Cohn. A proof of correctness of the VIPER microprocessor: The first level. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.). Kluwer Academic Publishers, Boston, 1987, pp. 27–71.

    Google Scholar 

  5. A. Cohn. The notion of proof in hardware verification. Journal of Automated Reasoning, 5(4):127–139 (1989).

    Google Scholar 

  6. W.J. Cullyer. Implementing safety critical systems: The VIPER microprocessor. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.). Kluwer Academic Publishers, Boston, 1987, pp. 1–26.

    Google Scholar 

  7. I. Dhingra. Formal validation of an integrated circuit design methodology. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.). Kluwer Academic Publishers, Boston, 1987, pp. 293–322.

    Google Scholar 

  8. M.J.C. Gordon. LCF_LSM: A system for specifying and verifying hardware. Technical Report 41, Computer Laboratory, University of Cambridge, 1983.

  9. M.J.C. Gordon. HOL: A machine oriented formulation of higher order logic. Technical Report 68, Computer Laboratory, University of Cambridge, May 1985.

  10. M.J.C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. Technical Report 77, Computer Laboratory, University of Cambridge, September 1985.

  11. M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.). Kluwer Academic Publishers, Boston, 1987, pp. 73–128.

    Google Scholar 

  12. M.J.C. Gordon. Mechanizing programming logics in higher order logic. In Current Trends in Hardware Verification and Automatic Theorem Proving, G. Birtwistle and P.A. Subrahmanyam (eds.). Springer-Verlag, New York, 1989, pp. 387–439.

    Google Scholar 

  13. M.J.C. Gordon and J. Herbert. Formal hardware verification methodology and its application to a network interface chip. IEE Proceedings, 133, Part E(5):255–270 (September 1986).

    Google Scholar 

  14. M.J.C. Gordon, P. Loewenstein, and M. Shahaf. Formal verification of a cell library: A case study in technology transfer. In Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1989, L.J.M. Claesen, (ed.), North-Holland, Amsterdam, 1990, pp. 409–417 (Volume II).

    Google Scholar 

  15. M.J.C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1979.

    Google Scholar 

  16. F.K. Hanna and N. Daeche. Specification and verification of digital systems using higher-order predicate logic. IEE Proceedings, 133 Part E(5):242–254 (September 1986).

    Google Scholar 

  17. J.M.J. Herbert. Formal verification of basic memory devices. Technical Report 124, Computer Laboratory, University of Cambridge, 1988.

  18. C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8): 666–667 (August 1978).

    Google Scholar 

  19. J.J. Joyce. Formal verification and implementation of a microprocessor. In VLSI Specification, Verification and Synthesis G. Birtwistle and P.A. Subrahmanyam, (eds.). Kluwer Academic Publishers, Boston, 1987, pp. 129–158.

    Google Scholar 

  20. J.J. Joyce. Multi-level verification of microprocessor-based systems. Ph.D. thesis, Technical Report 195, Computer Laboratory, University of Cambridge, 1990.

  21. T.F. Melham. Abstraction mechanisms for hardware verification. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds). Kluwer Academic Publishers, Boston, 1987, pp. 267–291.

    Google Scholar 

  22. T.F. Melham. Using recursive types to reason about hardware in higher order logic In Fusion of Hardware Design and Verification, G.J. Milne (ed.). North-Holland, Amsterdam, 1988, pp. 27–50.

    Google Scholar 

  23. T.F.Melham. Formalizing abstraction mechanisms for hardware verification in higher order logic. Ph.D. thesis, Technical Report 201, Computer Laboratory, University of Cambridge, 1990.

Temporal Logic

  1. K. Apt and D. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22 (6): 307–309 (1986).

    Google Scholar 

  2. H. Barringer and R. Kuiper. A temporal logic specification method supporting hierarchical development. Technical report, University of Manchester, November 1983.

  3. H. Barringer, R.Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, ACM, New York, 1984, pp. 51–63.

  4. M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Informatica, 20(3): 207–226 (1983).

    Google Scholar 

  5. G.V. Bochmann. Hardware specification with temporal logic: An example. IEEE Transactions on Computers, C-31 (3): 223–231 (March 1982).

    Google Scholar 

  6. S. Bose and A.L. Fisher. Automatic verification of synchronous circuits using symbolic simulation and temporal logic. In Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1989, L.J.M. Claesen, (ed.), North-Holland, Amsterdam, 1990, pp. 759–764.

    Google Scholar 

  7. M.C. Browne and E.M. Clarke. SML: A high level language for the design and verification of finite state machines. In From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione (eds). North-Holland, Amsterdam, 1987, pp. 269–292.

    Google Scholar 

  8. M.C. Browne, E.M. Clarke and D.L. Dill. Automatic circuit verification using temporal logic: Two new examples. In Formal Aspects of VLSI Design, G.J. Milne and P.A. Subrahmanyam (eds.). North-Holland, Amsterdam, 1986, pp. 113–124.

    Google Scholar 

  9. 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).

    Google Scholar 

  10. R.E. Bryant and C.-J.H. Seger. Formal verification of digital circuits using symbolic ternary system models. In Proceedings of the Workshop on Computer-Aided Verification (CAV 90), E.M. Clarke and R.P. Kurshan (eds.), volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society, Springer-Verlag, New York, 1991.

    Google Scholar 

  11. J. Burch, E.M. Clarke, K. McMillan, and D.L. Dill. Sequential circuit verification using symbolic model checking. In Proceedings of the 27th ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA June, 1990, pp. 46–51.

    Google Scholar 

  12. E.M. Clarke, S. Bose, M.C. Browne, and O. Grumberg. The design and verification of finite state hardware controllers. Technical Report CMU-CS-87–145, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, July 1987.

    Google Scholar 

  13. E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, Springer-Verlag, New York, 1981, pp. 52–71.

    Google Scholar 

  14. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2): 244–263 (April 1986).

    Google Scholar 

  15. E.M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model checking algorithms. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, ACM, New York, August 1987, pp. 294–303.

  16. E.M. Clarke, O. Grumberg, and M.C. Browne. Reasoning about networks with many identifical finite-state processes. In Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing ACM, New York, August 1986, pp. 240–248.

  17. E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages. ACM, New York, January 1992.

    Google Scholar 

  18. E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, D.C., June 1989, pp. 353–361.

    Google Scholar 

  19. E.M. Clarke, D.E. Long, and K.L. McMillan. A language for compositional specification and verification of finite state hardware controllers. In International Symposium on Computer Hardware Description Languages and their Applications, J.A. Darringer and F.J. Rammig (eds.). IFIP. North-Holland, Amsterdam, 1989, pp. 281–295.

    Google Scholar 

  20. O. Coudert, J.C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In Proceedings of the Workshop on Computer-Aided Verification (CAV 90) E.M. Clarke and R.P. Kurshan (eds.). volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, Springer-Verlag, New York, NY, 1991.

    Google Scholar 

  21. D.L. Dill and E.M. Clarke. Automatic verification of asynchronous circuits using temporal logic. IEE Proceedings 133 Part E(5): 276–282 (September 1986).

    Google Scholar 

  22. E.A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, J. van Leeuwen (ed.). Elsevier Science Publishers, Amsterdam, 1990, pp. 995–1071.

    Google Scholar 

  23. E.A. Emerson and E.M. Clarke. Characterizing correctness properties of parallel programs as fixpoints. In Proceedings of the Seventh International Colloquium on Automata, Languages, and Programming, volume 85 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1981, pp. 169–181.

    Google Scholar 

  24. E.A. Emerson and J.Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. In Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing. ACM, New York, 1982, pp. 169–180.

    Google Scholar 

  25. E.A. Emerson and J.Y. Halpern. ‘Sometimes’ and ‘Not Never’ revisited: On branching time versus linear time temporal logic. Journal of the ACM, 33(1): 151–178 (1986).

    Google Scholar 

  26. E.A. Emerson and C.L. Lei. Modalities for model checking: Branching time strikes back. In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, ACM, New York, January 1985, pp. 84–96.

  27. N. Francez. Fairness. Springer-Verlag, New York, 1986.

    Google Scholar 

  28. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In Proceedings of the Seventh Annual ACM Symposium on Principles of Programming Languages, ACM, New York, 1990, pp. 163–173.

  29. O. Grumberg and D.E. Long, Model checking and modular verification. In Proceedings of CONCUR'91: Second International Conference on Concurrency Theory, volume 527 of Lecture Notes in Computer Science, Springer-Verlag, New York, August 1991.

    Google Scholar 

  30. J. Halpern, Z. Manna, and B. Moszkowski. A hardware semantics based on temporal intervals, In Proceedings of the Tenth International Colloquium on Automata, Languages, and Programming. volume 154 of it Lecture Notes in Computer Science, Springer-Verlag, New York, 1983, pp. 278–291.

    Google Scholar 

  31. D. Harel, D. Kozen, and R. Parikh. Process logic: Expressiveness, decidability and completeness. Journal of Computer and System Sciences 25(2): 144–170 (1982).

    Google Scholar 

  32. G.E. Hughes and M.J. Creswell. An Introduction to Modal Logic. Methuen, London, 1977.

    Google Scholar 

  33. H.W. Kamp. Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California, Los Angeles, 1968.

  34. R. Koymans, J. Vytopil, and W.-P. de Roever. Real-time programming and asynchronous message passing. In Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, ACM, New York, 1983, pp. 187–197.

  35. L. Lamport. ‘Sometime’ is sometimes ‘Not Never’-On the temporal logic of programs. In Proceedings of the Seventh Annual ACM Symposium on Principles of Programming Languages, ACM, New York, 1980, pp. 174–185.

  36. L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5 (2): 190–222 (April 1983).

    Google Scholar 

  37. L. Lamport. What good is temporal logic? In Proceedings of the IFIP Congress on Information Processing R.E.A. Mason (ed.). North-Holland, Amsterdam, 1983, pp. 657–667.

    Google Scholar 

  38. M.E. Leeser. Reasoning about the function and timing of integrated circuits with Prolog and temporal logic. Ph.D.thesis, Technical Report 132, Computer Laboratory, University of Cambridge, April 1988.

  39. D. Lehmann, A. Pnueli and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In Proceedings of the Eighth International Colloquium on Automata, Language, and Programming, volume 115 of Lecture Notes in Computer Science, Springer-Verlag, New York, 1981, pp. 264–277.

    Google Scholar 

  40. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specifications In Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, ACM, New York, 1985, pp. 97–107.

  41. O. Lichtenstein, A. Pnueli, and L. Zuck:, The glory of the past. In Proceedings of the Conference on Logics of Programs, volume 193 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1985, pp. 196–218.

    Google Scholar 

  42. Y. Malachi and S.S. Owicki. Temporal specifications of self-timed systems. In VLSI Systems and Computations, H.T. Kung et. al. (eds.). Computer Science Press, Rockville, MD, 1981, pp. 203–212.

    Google Scholar 

  43. Z. Manna and A. Pnueli Verification of concurrent programs: Temporal proof principles. In Proceedings of the Workshop on Logics of Programs, volume 131 of Lecture Notes in Computer Science, Springer-Verlag, New York, 1981, pp. 200–252.

    Google Scholar 

  44. Z. Manna and A. Pnueli. Verification of concurrent programs: The temporal framework. In Correctness Problem in Computer Science, R.S. Boyer and J.S. Moore (eds.), Academic Press, London, 1982, pp. 215–273.

    Google Scholar 

  45. Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages, ACM, New York, 1983, pp. 141–154.

  46. Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4(3): 257–290 (1984).

    Google Scholar 

  47. Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6: 68–93 (1984).

    Google Scholar 

  48. K.L. McMillan. Symbolic Model Checking, An approach to the state explosion problem. Ph.D. thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 1992.

  49. K.L. McMillan and J.Schwalbe. Formal verification of the Encore Gigamax cache consistency protocol. In Proceedings of the International Symposium on Shared Memory Multiprocessing, 1991 (sponsored by Information Processing Society, Tokyo, Japan) pp. 242–251.

  50. B. Mishra and E.M. Clarke. Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science, 38: 269–291 (1985).

    Google Scholar 

  51. B. Moszkowski, Reasoning about Digital Circuits. Ph.D. thesis, Stanford University, Stanford, CA, 1983.

  52. B. Moszkowski, Executing temporal logic programs. Technical Report 55, Computer Laboratory, University of Cambridge, August 1984.

  53. B. Moszkowski. A temporal logic for multi-level reasoning about hardware. Computer, pp. 10–19 (February 1985).

  54. S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transations on Programming Languages and Systems, 4(3): 455–495 (July 1992).

    Google Scholar 

  55. A. Pnueli. The temporal logic of programs. In Proceedings of the Eighth Annual Symposium on Foundations of Computer Science, IEEE, New York, 1977, pp. 46–57.

  56. A. Pneuli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, K. Apt (ed.) Volume 13 of NATO ASI series, Series F, Computer and System Sciences, Springer-Verlag, New York, 1984, pp. 123–144.

    Google Scholar 

  57. A. Pnueli, Linear and branching structures in the semantics and logics of reactive systems. In Proceedings of the Twelfth International Colloquium on Automata, Languages, and Programming, volume 194 of Lecture Notes in Computer Science, Springer-Verlag, New York, 1985, pp. 15–32.

    Google Scholar 

  58. J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the Fifth International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Spring-Verlag, New York, 1982, pp. 337–351.

    Google Scholar 

  59. J.P. Queille and J. Sifakis. Fairness and related properties in transition systems. Acta Informatica, 19:195–220 (1983).

    Google Scholar 

  60. N. Rescher and A. Urquhart. Temporal Logic. Springer-Verlag, Berlin, 1971.

    Google Scholar 

  61. B.-H. Schlingloff. Modal definability of ω-tree languages. In Proceedings of the ESPRIT-BRA ASMICS Workshop on Logics and Recognizable Sets, Germany, 1990.

  62. A.P. Sistla and E.M. Clarke, Complexity of propositional linear temporal logic. Journal of the ACM, 32(3):733–749 (July 1985).

    Google Scholar 

  63. A.P. Sistla, E.M. Clarke, N. Francez, and A.M. Meyer. Can message buffers be axiomatized in temporal logic? Information and Control, 63(1):88–112 (1984).

    Google Scholar 

  64. A.P. Sistla and S. German. Reasoning with many processes. In Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington D.C., 1987, pp. 138–152.

    Google Scholar 

  65. P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proceedings of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, ACM, New York, January 1986, pp. 184–192.

Extended Temporal Logic

  1. E.M. Clarke, O. Grumberg, and R.P. Kurshan, A synthesis of two approaches for verifying finite state concurrent systems. In Proceedings of Symposium on Logical Foundations of Computer Science: Logic at Botik '89, volume 363 of Lecture Notes in Computer Science, Springer-Verlag, New York, July, 1989.

    Google Scholar 

  2. A.C. Shaw. Software specification languages based on regular expressions. Technical report, ETH Zurich, June 1979.

    Google Scholar 

  3. P. Wolper. Temporal logic can be made more expressive. In Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, IEEE, New York, 1981, pp. 340–348.

  4. P. Wolper, M.Y. Vardi, and A.P. Sistla. Reasoning about infinite computation paths. In Proceedings of the 24th Annual Symposium on Foundations of Computer Science, IEEE, New York, 1983, pp. 185–194.

Mu-Calculus

  1. J. Burch, E.M. Clarke, K. McMillan, D. Dill, and J. Hwang, Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, D.C., June 1990, pp. 428–439.

    Google Scholar 

  2. E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mucalculus. In Proceedings of the Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, D.C., 1986, pp. 267–278.

    Google Scholar 

  3. D. Kozen, Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354 (December 1983).

    Google Scholar 

  4. D. Niwinski. Fixed points vs. infinite generation. In Proceedings of the Third Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, D.C., July 1988, pp. 402–409.

    Google Scholar 

  5. D. Park. Finiteness is mu-ineffable. Theory of Computation Report No. 3, University of Warwick, Warwick, England, 1974.

    Google Scholar 

  6. D. Park. Concurrency and automata on infinite sequences. In Proceedings of the Fifth GI-Conference on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, Springer-Verlag, New York, 1981, pp. 167–183.

    Google Scholar 

  7. V. Pratt. A decidable mu-calculus. In Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, IEEE, New York, 1981, pp. 421–427.

Functional Approaches

  1. D. Borrione, P. Camurati, J.L. Paillet, and P. Prinetto, A functional approach to formal hardware verification: The MTI experience. In Proceedings of the IEEE International Conference on Computer Design, IEEE Computer Science Press, Silver Spring, MD, 1988, pp. 592–595.

    Google Scholar 

  2. D. Borrione and J.L. Paillet. An approach to the formal verification of VHDL descriptions. Research Report 683, IMAG/ARTEMIS, Grenoble, France, November 1987.

    Google Scholar 

  3. Z. Chaochen and C.A.R. Hoare, A model for synchronous switching circuits and its theory of correctness. In Proceedings of the Workshop on Designing Correct Circuits, G. Jones and M. Sheeran (eds.). Springer-Verlag, New York, 1990, pp. 196–211.

    Google Scholar 

  4. G.J. Milne. CIRCAL: A calculus for circuit description. In Integration, the VLSI Journal, Volume 1, Nos. 2 & 3, pp. 121–160 (October 1983).

  5. G.J. Milne. A model for hardware description and verification. In Proceedings of the 21st ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA.

  6. M. Sheeran. μFP, An Algebraic VLSI Design Language. Ph.D. thesis, University of Oxford, England, 1983.

  7. M. Sheeran. Design and verification of regular synchronous circuits. IEE Proceedings, 133 Part E(5):295–304 (September 1986).

    Google Scholar 

  8. T.J. Wagner. Hardware Verification. Ph.D. thesis, Stanford University, Stanford, CA, 1977.

  9. T.J. Wagner. Verification of hardware desings through symbolic manipulation. In Proceedings of the International Symposium on Design Automation and Microprocessors, IEEE, New York, 1977, pp. 50–53.

  10. D. Weise. Multilevel verification of MOS circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 9(4):341–351 (April 1990).

    Google Scholar 

  11. G. Winskel. A compositional model of MOS circuits. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.) Kluwer Academic Publishers, Boston, 1987, pp. 323–347.

    Google Scholar 

Machine Equivalence

  1. J.P. Billon. Perfect normal forms for discrete functions. Technical Report 87019, Bull Research Center, Louveciennes, France, June 1987.

    Google Scholar 

  2. J.P. Billon and J.C. Madre. Original concepts of PRIAM, an industrial tool for efficient formal verification of combinational circuits. In Fusion of Hardware Design and Verification, G.J. Milne (ed.). North-Holland, Amsterdam, 1988, pp. 487–501.

    Google Scholar 

  3. O. Coudert, C. Berthet, and J.C. Madre. Verification of sequential machines using Boolean functional vectors. In Proceedings of the IFIP International Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, 1989, L.J.M. Claesen, (ed.), North-Holland, Amsterdam, 1990, pp. 111–128.

    Google Scholar 

  4. O. Coudert, C. Berthet, and J.C. Madre, Verification of synchronous sequential machines using symbolic execution. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 365–373.

    Google Scholar 

  5. O. Coudert and J.C. Madre. Logics over finite domain of interpretation: Proof and resolution procedures. Technical report, Bull Research Center, Louveciennes, France, 1989.

    Google Scholar 

  6. S. Devadas, H-K. T. Ma, and A.R. Newton. On the verification of sequential machines at differing levels of abstraction. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, June 1988, pp. 713–722.

  7. J.E. Hopcroft and J.D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading, MA, 1979.

    Google Scholar 

  8. J.C. Madre and J.P. Billon. Proving circuit correctness using formal comparison between expected and extracted behavior. In Proceedings of the 25th ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA 1988, pp. 205–210.

    Google Scholar 

Language Containment

  1. S. Aggarwal, R.P. Kurshan, and K.K. Sabnani. A calculus for protocol specification and validation. In Protocol Specification, Testing and Verification III. North-Holland, Amsterdam, 1983, pp. 19–34.

    Google Scholar 

  2. J.R. Büchi. On a decision method in restricted second order arithmetic. In Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, E. Nagel et al (ed.). Stanford University Press, Stanford, CA, 1960, pp. 1–12.

    Google Scholar 

  3. E.M. Clarke, I.A. Draghicescu, and R.P. Kurshan, A unified approach for showing language containment and equivalence between various types of ω-automata. In Proceedings of the Fifteenth Colloquium on Trees in Algebra and Programming, volume 431 of Lecture Notes in Computer Science. Springer-Verlag, New York, May 1990.

    Google Scholar 

  4. I. Gertner and R.P. Kurshan. Logical analysis of digital circuits. In Proceedings of the Eighth International Symposium on Computer Hardware Description Languages and their Applications, M.R. Barbacci and C.J. Koomen (eds.) IFIP, North-Holland, Amsterdam, 1987, pp. 47–67.

    Google Scholar 

  5. B. Gopinath and R.P. Kurshan, The Selection/Resolution model of coordinating concurrent processes. Technical report, AT&T Bell Laboratories, Murray Hill, NJ, 1980.

    Google Scholar 

  6. P. Halmos. Lectures on Boolean Algebras. Springer-Verlag, New York, 1974.

    Google Scholar 

  7. Z. Har'El and R.P. Kurshan. Software for analytical development of communication protocols. Technical report, AT&T Bell Laboratories, Murray Hill, NJ, January 1990.

    Google Scholar 

  8. J. Katzenelson and R.P. Kurshan. S/R: A language for specifying protocols and other communicating processes. In Proceedings of the Fifth IEEE International Conference on Computer Communications, IEEE, New York, 1986, pp. 286–292.

  9. R.P. Kurshan, Reducibility in analysis of coordination. In Discrete Event Systems: Models and Applications, volume 103 of Lecture Notes in Control and Information Sciences, Springer-Verlag, New York, 1987, pp. 19–39.

    Google Scholar 

  10. R.P. Kurshan. Analysis of discrete event coordination. In Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, J.W. de Bakker, W.-P. de Roever, and G. Rozenberg (eds.). Springer-Verlag, New York, 1989.

    Google Scholar 

  11. R.P. Kurshan and K.L. McMillan. A structural induction theorem for processes. In Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing, ACM, New York, 1989, pp. 239–247.

  12. R.P. Kurshan and K.L. McMillan. Analysis of digital circuits through symbolic reduction. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 10(11):1356–1371 (November 1991).

    Google Scholar 

  13. W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, volume B, J. van Leeuwen (ed.). Elsevier Science Publishers, Amsterdam, 1990, pp. 133–191.

    Google Scholar 

  14. P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 68–80.

    Google Scholar 

Trace Theory

  1. J.R. Burch. Combining CTL, trace theory and timing models. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 334–348.

    Google Scholar 

  2. T.-A. Chu. On the models for designing VLSI asynchronous digital systems. Integration, the VLSI Journal, 4:99–113 (1986).

    Google Scholar 

  3. D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. Ph.D. thesis, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, 1988. Also published in ACM Distinguished Dissertations Series, MIT Press, Cambridge, MA, 1989.

  4. D.L. Dill. Trace theory for automatic hierarchical verification of speed-independent circuits. In Proceedings of the Fifth MIT Conference on Advanced Research in VLSI, J. Allen and F.T. Leighton (eds.). MIT Press, Cambridge, MA, 1988.

    Google Scholar 

  5. D.L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 197–212.

    Google Scholar 

  6. A.J. Martin. The design of a self-timed circuit for distributed mutual exclusion. In H. Fuchs, ed., Proceedings of the 1985 Chapel Hill Conference on VLSI; W.H. Freeman, New York, 1985, pp. 245–260.

    Google Scholar 

  7. M. Rem. Concurrent computation and VLSI circuits. In Control Flow and Data Flow: Concepts of Distributed Programming, M. Broy (ed.). Volume 14 of NATO ASI series, series F. Computer and System Sciences, Springer-Verlag, New York, 1985, pp. 399–437.

    Google Scholar 

  8. J.L.A. van de Sneupscheut. Trace Theory and VLSI Design. Ph.D. thesis, Department of Computing Science, Eindhoven University of Technology, The Netherlands, 1983.

Hybrid Approaches

  1. E.A. Emerson and C.L. Lei. Temporal model checking under generalized fairness constraints. In Proceedings of the Eighteenth Hawaii International Conference on System Sciences, 1985, Western Periodicals Company, North Hollywood, CA, pp. 277–288, (Vol. I).

  2. M. Fujita and H. Fujisawa. Specification, verification, and synthesis of control circuits with propositional temporal logic. In Proceedings of the Ninth International Symposium on Computer Hardware Description Languages and their Applications, J.A. Darringer and F.J. Rammig (eds.). IFIP, North-Holland, Amsterdam, 1989, pp. 265–279.

    Google Scholar 

  3. M. Fujita, H. Tanaka, and T. Moto-oka. Verification with Prolog and temporal logic. In Proceedings of the Sixth International Symposium on Computer Hardware Description Languages and Their Applications, T. Uehara and M. Barbacci (eds.). IFIP, North-Holland, Amsterdam, 1983, pp. 103–114.

    Google Scholar 

  4. M. Fujita, H. Tanaka, and T. Moto-oka. Logic design assistance with temporal logic. In Proceedings of the Seventh International Symposium on Computer Hardware Description Languages and their Applications, C.J. Koomen and T. Moto-oka (eds.). IFIP, North-Holland, Amsterdam, 1983, pp. 129–138.

    Google Scholar 

  5. P. Loewenstein. Reasoning about state machines in higher-order logic. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, M. Leeser and G. Brown (eds.). volume 408 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1990.

    Google Scholar 

  6. P. Loewenstein and D.L. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic. In Proceedings of the Workshop on Computer-Aided Verification (CAV 90), E.M. Clarke and R.P. Kurshan (eds.). volume 3 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Mathematical Society, Springer-Verlag, New York, 1991.

    Google Scholar 

  7. F. Maruyama and M. Fujita. Hardware verification. IEEE Computer, 18(2):22–32 (February 1985).

    Google Scholar 

  8. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. In Proceedings of the Twelfth International Colloquium on Automata, Languages, and Programming, volume 194 of Lecture Notes in Computer Science. Springer-Verlag, New York, pp. 465–474.

  9. M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., June 1986, pp. 332–344.

    Google Scholar 

  10. M. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences, 32(2): 183–221 (April 1986).

    Google Scholar 

  11. P. Wolper. The tableau method for temporal logic: An overview. Logique et Analyse, 28:119–136 (1985).

    Google Scholar 

Real-Time Verification

  1. R. Alur, C. Courcoubetics, and D.L. Dill. Model checking for real-time systems. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., June 1990, pp. 414–425.

    Google Scholar 

  2. R. Alur and D.L. Dill. Automata for modeling real-time systems. In Proceedings of the Seventeenth International Colloquium on Automata, Languages, and Programming, volume 443 of Lecuture Notes in Computer Science. Springer-Verlag, New York, 1990.

    Google Scholar 

  3. R. Alur and T.A. Henzinger. A really temporal logic. In Proceedings of the 30th Annual Symposium on Foundations of Computer Science, IEEE, New York, pp. 164–169, 1989.

  4. R. Alur and T.A. Henzinger. Real-time logics: Complexity and expressiveness. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, D.C., June 1990, pp. 390–401.

    Google Scholar 

  5. M.R. Barbacci and J.M. Wing. Specifying functional and timing behavior for real-time systems. In Proceedings of the Conference on Parallel Architectures and languages Europe, volume 259 of Lecture Notes in Computer Science. Springer-Verlag, New York, June 1987.

    Google Scholar 

  6. A. Bernstein and P. Harter. Proving real-time properties of programs with temporal logic. In Proceedings of the Eighth Annual ACM Symposium on Operating Systems Principles, ACM, New York, December 1981, pp. 1–11.

  7. J.R. Burch. Modeling timing assumptions with trace theory. In Proceedings of the IEEE International Conference on Computer Design, IEEE Computer Science Press, Silver Spring, MD, October 1989, pp. 208–211.

    Google Scholar 

  8. J.R. Burch. Automatic Verification of Real-Time Concurrent Systems. Ph.D. thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, 1991 (forthcoming).

  9. E.A. Emerson, A.K. Mok, A.P. Sistla, and J. Srinivasan. Quantitative temporal reasoning. Presented at the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 1989.

  10. E. Harel, O. Lichtenstein, and A. Pnueli. Explicit clock temporal logic. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., June 1990, pp. 402–413.

    Google Scholar 

  11. F. Jahanian, R.S. Lee, and A.K. Mok. Semantics of modechart in real time logic. In Proceedings of the 21st Hawaii International Conference on System Sciences, IEEE Computer Science Press, Washington, D.C., January 1988, Volume II, pp. 479–489.

    Google Scholar 

  12. F. Jahanian and A. Mok. Safety analysis of timing properties in real-time systems. IEEE Transactions on Software Engineering, 12(9):890–904 (1986).

    Google Scholar 

  13. F. Jahanian, A. Mok, and D.A. Stuart. Formal specification of real-time systems. Technical Report TR-88-25, Department of Computer Science, University of Texas at Austin, June 1988.

  14. F. Jahanian and D.A. Stuart. A method for verifying properties of modechart specification. In Proceedings of the IEEE Real-Time Systems Symposium, IEEE, New York, December 1988, pp. 12–21.

  15. R. Koymans. Specifying Message-Passing and Time-Critical Systems with Temporal Logic. Ph.D. thesis, Eindhoven University of Technology, The Netherlands, 1989.

  16. H. Lewis. A logic of concrete time intervals. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Washington, D.C., June 1990, pp. 380–389.

    Google Scholar 

  17. G.H. MacEwen and D.B. Skillicorn. Using higher-order logic for modular specification of real-time distributed systems. In Formal Techniques in Real-time and Fault Tolerant Systems: Proceedings of a Symposium, M. Joseph (ed.), Volume 331 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1988, pp. 36–66.

    Google Scholar 

  18. J. Ostroff. Real-time computer control of discrete event systems modeled by extended state machines: A temporal logic approach. Technical Report 8618, University of Toronto, September 1987.

  19. J. Ostroff. Automated verification of timed transition models. In Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1989, pp. 247–256.

    Google Scholar 

  20. A. Pnueli and E. Harel. Applications of temporal logic to the specification of real-time systems. In Formal Techniques in Real-time and Fault Tolerant Systems: Proceedings of a Symposium, M. Joseph (ed.), Volume 331 of Lecture Notes in Computer Science. Springer-Verlag, New York, 1988, pp. 84–98.

    Google Scholar 

  21. A. Zwarico and I. Lee. Proving a network of real-time processes correct. In Proceedings of the IEEE Real-Time Systems Symposium, IEEE, New York, December 1985, pp. 169–177.

  22. J.R. Burch. Using BDDs to verify multipliers. In Proceedings of the 28th ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, June 1991, pp. 408–412.

    Google Scholar 

  23. J.R. Burch. E.M. Clarke, and D.E. Long. Representing circuits more efficiently in symbolic model checking. In Proceedings of the 28th ACM/IEEE Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, June 1991, pp. 403–407.

    Google Scholar 

  24. H. Busch and G. Venzl. Proof-aided design of verified hardware.In Procedings of the 28th ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, June 1991, pp. 391–396.

    Google Scholar 

  25. H. Eveking. Verification, synthesis and correctness-preserving transformations-cooperative approaches to correct hardware design. In From HDL Descriptions to Guranteed Correct Circuit Designs, D. Borrione (ed.). North-Holland, Amsterdam, 1987, pp. 229–239.

    Google Scholar 

  26. W. Luk and G. Jones. From specifications to parameterized architectures. In Fusion of Hardware Design and Verification, G.J. Milne (ed.). North-Holland, Amsterdam, 1988, pp. 267–268.

    Google Scholar 

  27. H. Ochi, N. Ishiura, and S. Yajima. Breadth-first manipulation of SBDD of Boolean functions for vector processing. In Proceedings of the 28th ACM/IEEE Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, June 1991, pp. 413–416.

    Google Scholar 

  28. V. Stavridou, H. Barringer, and D.A. Edwards. Formal specification and verification of hardware: A comparative case study. In Proceedings of the 25th ACM/IEEE Design Automation Conference, 1988, pp. 197–204.

  29. D. Verkest, P. Johannes, L. Claesen, and H. De Man. Formal techniques for proving correctness of parameterized hardware using correctness preserving transformations. In Fusion of Hardware Design and Verification, G.J. Milne (ed.). North-Holland, Amsterdam, 1988, pp. 77–97.

    Google Scholar 

  30. D. Verkest, P. Johannes, L. Claesen, and H. De Man. Correctness proofs of parameterized hardware modules in the Cathedral-II synthesis environment. In Proceedings of the European Design Automation Conference, Glasgow, 1990. IEEE Computer Society Press, Washington, D.C., 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carnegie Mellon University, 5000 Forbes Ave., 15213, Pittsburgh, Pennsylvania

    Aarti Gupta

Authors
  1. Aarti Gupta
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Gupta, A. Formal hardware verification methods: A survey. Form Method Syst Des 1, 151–238 (1992). https://doi.org/10.1007/BF00121125

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00121125

Keywords

Search

Navigation