Formal verification in hardware design: a survey

ABSTRACT

In recent years, formal methods have emerged as an alternative approach to ensuring the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing. There are two main aspects to the application of formal methods in a design process: the formal framework used to specify desired properties of a design and the verification techniques and tools used to reason about the relationship between a specification and a corresponding implementation. We survey a variety of frameworks and techniques proposed in the literature and applied to actual designs. The specification frameworks we describe include temporal logics, predicate logic, abstraction and refinement, as well as containment between &ohgr;-regular languages. The verification techniques presented include model checking, automata-theoretic techniques, automated theorem proving, and approaches that integrate the above methods. In order to provide insight into the scope and limitations of currently available techniques, we present a selection of case studies where formal methods were applied to industrial-scale designs, such as microprocessors, floating-point hardware, protocols, memory subsystems, and communications hardware.

REFERENCES

• 1: Mark D. Aagaard , Carl-Johan H. Seger, The formal verification of a pipelined double-precision IEEE floating-point multiplier, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.7-10, November 05-09, 1995, San Jose, California, United States
• 2: Mark Aagaard , Miriam Leeser , Phillip J. Windley, Toward a Super Duper Hardware Tactic, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.399-412, August 11-13, 1993
• 3: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 4: Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993 [doi>10.1145/151646.151649]
• 5: ALBIN, K. L., BROCK, B. C., HUNT, W. A., AND SMITH, L. M 1995. Testing the FM9001 microprocessor. Tech. Rep. 90. Computational Logic, Inc., Austin, TX.
• 6: Rajeev Alur , Thomas A. Henzinger, Logics and Models of Real Time: A Survey, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.74-106, June 03-07, 1991
• 7: K. D. Anon , N. Boulerice , Eduard Cerny , Francisco Corella , Michel Langevin , Xiaoyu Song , Sofiène Tahar , Y. Xu , Z. Zhou, MDG Tools for the Verification of RTL Designs, Proceedings of the 8th International Conference on Computer Aided Verification, p.433-436, August 03, 1996
• 8: D. P. Appenzeller, Formal verification of a PowerPC microprocessor, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.79, October 02-04, 1995
• 9: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, Validity Checking for Combinations of Theories with Equality, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.187-201, November 06-08, 1996
• 10: Derek Lee Beatty, A methodology for formal hardware verification, with application to microprocessors, Carnegie Mellon University, Pittsburgh, PA, 1993
• 11: Derek L. Beatty , Randal E. Bryant, Formally verifying a microprocessor using a simulation methodology, Proceedings of the 31st annual conference on Design automation, p.596-602, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196575]
• 12: Ilan Beer , Shoham Ben-David , Cindy Eisner , Avner Landver, RuleBase: an industry-oriented formal verification tool, Proceedings of the 33rd annual conference on Design automation, p.655-660, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240642]
• 13: Orna Bernholtz , Moshe Y. Vardi , Pierre Wolper, An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract), Proceedings of the 6th International Conference on Computer Aided Verification, p.142-155, June 21-23, 1994
• 14: Mark Birman , Allen Samuels , George Chu , Ting Chuk , Larry Hu , John McLeod , John Barnes, Developing the WTL3170/3171 Sparc Floating-Point Coprocessors, IEEE Micro, v.10 n.1, p.55-64, January 1990 [doi>10.1109/40.46769]
• 15: Nikolaj Bjørner , Anca Browne , Eddie Chang , Michael Colón , Arjun Kapur , Zohar Manna , Henny Sipma , Tomás E. Uribe, STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems, Proceedings of the 8th International Conference on Computer Aided Verification, p.415-418, August 03, 1996
• 16: Jörg Bormann , Jörg Lohse , Michael Payer , Gerd Venzl, Model checking in industrial hardware design, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.298-303, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217545]
• 17: BOYER, R. S. AND MOORE, J. S. 1979. A Computational Logic. Academic Press, Inc., New York, NY.
• 18: Robert S. Boyer , J. Strother Moore, A computational logic handbook, Academic Press Professional, Inc., San Diego, CA, 1988
• 19: Karl S. Brace , Richard L. Rudell , Randal E. Bryant, Efficient implementation of a BDD package, Proceedings of the 27th ACM/IEEE conference on Design automation, p.40-45, June 24-27, 1990, Orlando, Florida, United States [doi>10.1145/123186.123222]
• 20: Julian Charles Bradfield, Verifying temporal properties of systems, Birkhauser Boston Inc., Cambridge, MA, 1991
• 21: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.248-256, November 06-08, 1996
• 22: BROCK, B. AND HUNT, W.A. 1990. Report on the formal specification and partial verification of the VIPER microprocessor. Tech. Rep. 46. Computational Logic, Inc., Austin, TX.
• 23: BROCK, B., HUNT, W. A., AND KAUFMANN, M. 1994. The FM9001 microprocessor proof. Tech. Rep. 86. Computational Logic, Inc., Austin, TX.
• 24: Bishop Brock , Matt Kaufmann , J. Strother Moore, ACL2 Theorems About Commercial Microprocessors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.275-293, November 06-08, 1996
• 25: Bishop C. Brock , Warren A. Hunt, Jr., The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor, Formal Methods in System Design, v.11 n.1, p.71-104, July 1997 [doi>10.1023/A:1008685826293]
• 26: R. E. Bryant , D. Beatty , K. Brace , K. Cho , T. Sheffler, COSMOS: a compiled simulator for MOS circuits, Proceedings of the 24th ACM/IEEE conference on Design automation, p.9-16, June 28-July 01, 1987, Miami Beach, Florida, United States [doi>10.1145/37888.37890]
• 27: Randal E. Bryant , Yirng-An Chen, Verification of arithmetic circuits with binary moment diagrams, Proceedings of the 32nd ACM/IEEE conference on Design automation, p.535-541, June 12-16, 1995, San Francisco, California, United States [doi>10.1145/217474.217583]
• 28: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 29: Randal E. Bryant, A methodology for hardware verification based on logic simulation, Journal of the ACM (JACM), v.38 n.2, p.299-328, April 1991 [doi>10.1145/103516.103519]
• 30: Randal E. Bryant, On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication, IEEE Transactions on Computers, v.40 n.2, p.205-213, February 1991 [doi>10.1109/12.73590]
• 31: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 32: Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.236-243, November 05-09, 1995, San Jose, California, United States
• 33: Randal E. Bryant, Bit-level analysis of an SRT divider circuit, Proceedings of the 33rd annual conference on Design automation, p.661-665, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240643]
• 34: BURCH, J., CLARKE, E., LONG, D., MCMILLAN, K., AND DILL, D. 1994. Symbolic model checking for sequential circuit verification. IEEE Trans. Comput.-Aided Des. Integr. Circuits 13, 4 (Apr.), 401-424.
• 35: Jerry R. Burch, Techniques for verifying superscalar microprocessors, Proceedings of the 33rd annual conference on Design automation, p.552-557, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240623]
• 36: BURCH, J. R., CLARKE, E. M., MCMILLAN, K. L., DILL, D. L., AND HWANG, L.J. 1990. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90, June). 428-439.
• 37: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 38: Joseph J. F. Cavanagh, Digital Computer Arithmetic, McGraw-Hill, Inc., New York, NY, 1983
• 39: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 40: Yirng-An Chen , Edmund M. Clarke , Pei-Hsin Ho , Yatin Vasant Hoskote , Timothy Kam , Manpreet Khaira , John W. O'Leary , Xudong Zhao, Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.19-33, November 06-08, 1996
• 41: CHURCH, A. 1940. A formulation of the simple theory of types. J. Symb. Logic 5, 56-115.
• 42: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 43: E. M. Clarke , M. Fujita , X. Zhao, Hybrid decision diagrams, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.159-163, November 05-09, 1995, San Jose, California, United States
• 44: Edmund M. Clarke , Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness, Verification of the Futurebus+ Cache Coherence Protocol, Proceedings of the 11th IFIP WG10.2 International Conference sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC on Computer Hardware Description Languages and their Applications, p.15-30, April 26-28, 1993
• 45: Edmund M. Clarke , Kenneth L. McMillan , Sérgio Vale Aguiar Campos , Vassili Hartonas-Garmhausen, Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.419-427, August 03, 1996
• 46: E. M. Clarke , K. L. McMillan , X Zhao , M. Fujita , J. Yang, Spectral transforms for large boolean functions with applications to technology mapping, Proceedings of the 30th international conference on Design automation, p.54-60, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164569]
• 47: E. M. Clarke , I. A. Browne , R. P. Kurshan, A unified approach for showing language containment and equivalence between various types of &ohgr;-automata, Proceedings of the fifteenth colloquium on CAAP'90, p.103-116, May 1990, Copenhagen, Denmark
• 48: Edmund M. Clarke , Steven M. German , Xudong Zhao, Verifying the SRT Division Algorithm Using Theorem Proving Techniques, Proceedings of the 8th International Conference on Computer Aided Verification, p.111-122, August 03, 1996
• 49: Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi, Another Look at LTL Model Checking, Proceedings of the 6th International Conference on Computer Aided Verification, p.415-427, June 21-23, 1994
• 50: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 51: E. M. Clarke , M. Khaira , X. Zhao, Word level model checking—avoiding the Pentium FDIV error, Proceedings of the 33rd annual conference on Design automation, p.645-648, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240640]
• 52: COHN, A. 1988. A proof of correctness of the Viper microprocessor: The first level. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam, Eds. Kluwer Academic Publishers, Hingham, MA, 27-71.
• 53: Avra Cohn, Correctness properties of the Viper block model: the second level, Current trends in hardware verification and automated theorem proving, Springer-Verlag New York, Inc., New York, NY, 1989
• 54: A. Cohn, The notion of proof in hardware verification, Journal of Automated Reasoning, v.5 n.2, p.127-139, June 1989
• 55: F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997 [doi>10.1023/A:1008663530211]
• 56: O. Coudert , C. Berthet , J. C. Madre, Verification of synchronous sequential machines based on symbolic execution, Proceedings of the international workshop on Automatic verification methods for finite state systems, p.365-373, February 1990, Grenoble, France
• 57: COUDERT, O. AND MADRE, J. C. 1990. A unified framework for the formal verification of sequential circuits. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'90). 126-129.
• 58: CURZON, P. 1994. The formal verification of the Fairisle ATM switching element: An overview. Tech. Rep. 328,. Univ. of Cambridge Computer Laboratory, Cambridge, UK.
• 59: CURZON, P. AND LESLIE, I. 1996. Improving hardware design whilst simplyfying their proof. In Proceedings of the Third Workshop on Designing Correct Circuits (DCC, Bastad, Sweden, Sept.).
• 60: David Cyrluk , Patrick Lincoln , Natarajan Shankar, On Shostak's Decision Procedure for Combinations of Theories, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.463-477, August 03, 1996
• 61: David Cyrluk , S. Rajan , Natarajan Shankar , Mandayam K. Srivas, Effective Theorem Proving for Hardware Verification, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.203-222, September 26-28, 1994
• 62: DAC EXHIBITS, 1997. Thirty-Fourth DAC exhibit information, http://www.dac.com/ 34exhibits.html.
• 63: David Déharbe , Dominique Borrione, Semantics of a verification-oriented subset of VHDL, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.293-310, October 02-04, 1995
• 64: David L. Dill, The Murphi Verification System, Proceedings of the 8th International Conference on Computer Aided Verification, p.390-393, August 03, 1996
• 65: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 66: David A. Duffy, Principles of automated theorem proving, John Wiley & Sons, Inc., New York, NY, 1991
• 67: Ásgeir Th. Eiríksson, Integrating formal verification methods with a conventional project design flow, Proceedings of the 33rd annual conference on Design automation, p.666-671, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240644]
• 68: Ásgeir Th. Eiríksson , Kenneth L. McMillan, Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study, Proceedings of the 7th International Conference on Computer Aided Verification, p.367-380, July 03-05, 1995
• 69: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 70: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• 71: Urban Engberg , Peter Grønning , Leslie Lamport, Mechanical Verification of Concurrent Systems with TLA, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.44-55, June 29-July 01, 1992
• 72: FILKORN, T. 1991. A method for symbolic verification of synchronous circuits. In Computer Hardware Description Languages and their Applications (CHDL '91, Apr.), D. Borrione and R. Waxman, Eds. North-Holland Publishing Co., Amsterdam, The Netherlands, 249-259.
• 73: FUJITA, M., FUJISAWA, H., AND MATSUNAGA, Y. 1993. Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Trans. Comput.-Aided Des. Integr. Circuits 12, 1 (Jan.), 6-12.
• 74: S. J. Garland , J. V. Guttag, An overview of LP, the larch power, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.137-151, January 1989
• 75: R. Gerth, Foundation of compositional program refinement—safety properties, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.777-807, May 1990, Mook, The Netherlands
• 76: GORDON, M. 1985. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design, G. J. Milne and P. A. Subrahmanyam, Eds. Elsevier Science Inc., New York, NY, 153-177.
• 77: GORDON, M. J., Ed. 1988. HOL: A proof generating system for higher-order logic. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam, Eds. Kluwer Academic Publishers, Hingham, MA, 74-128.
• 78: GORDON, M. J. C., WADSWORTH, C. P., AND MILNER, A. J. 1979. Edinburgh LCF: a mechanised logic of computation. In Lecture Notes in Computer Science. Lecture Notes in Computer Science, vol. 78. Springer-Verlag, New York.
• 79: Orna Grumberg , David E. Long, Model checking and modular verification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.843-871, May 1994 [doi>10.1145/177492.177725]
• 80: Aarti Gupta, Formal hardware verification methods: a survey, Formal Methods in System Design, v.1 n.2-3, p.151-238, Oct. 1992 [doi>10.1007/BF00121125]
• 81: HARDIN, R. H., HAR'EL, Z., AND KURSHAN, R. P. 1996. COSPAN. In Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV '96, Aug.). Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, 423-427.
• 82: David Harel, On visual formalisms, Communications of the ACM, v.31 n.5, p.514-530, May 1988 [doi>10.1145/42411.42414]
• 83: Cheryl Harkness , Elizabeth Wolf, Verifying the summit bus converter protocols with symbolic model checking, Formal Methods in System Design, v.4 n.2, p.83-97, Feb. 1994 [doi>10.1007/BF01384079]
• 84: John Harrison, A HOL Decision Procedure for Elementary Real Algebra, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.426-435, August 11-13, 1993
• 85: John Harrison, Floating Point Verification in HOL, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, p.186-199, September 11-14, 1995
• 86: Scott Edward Hazelhurst , Carl-Johan H. Seger, Compositional model checking of partially ordered state spaces, 1996
• 87: Scott Hazelhurst , Carl-Johan H. Seger, Composing Symbolic Trajectory Evaluation Results, Proceedings of the 6th International Conference on Computer Aided Verification, p.273-285, June 21-23, 1994
• 88: HAZELHURST, S. AND SEGER, C.-J. H. 1995. A simple theorem prover based on symbolic trajectory evaluation and BDDs. IEEE Trans. Comput.-Aided Des. Integr. Circuits 14, 4 (Apr.), 413-422.
• 89: David A. Patterson , John L. Hennessy, Computer architecture: a quantitative approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1990
• 90: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 91: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 92: Ramin Hojati , Robert K. Brayton , Robert P. Kurshan, BDD-Based Debugging Of Design Using Language Containment and Fair CTL, Proceedings of the 5th International Conference on Computer Aided Verification, p.41-58, June 28-July 01, 1993
• 93: Ramin Hojati , Vigyan Singhal , Robert K. Brayton, Edge-Streett/ Edge-Rabin Automata Environment for, University of California at Berkeley, Berkeley, CA, 1994
• 94: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 95: Alan J. Hu , David L. Dill, Reducing BDD size by exploiting functional dependencies, Proceedings of the 30th international conference on Design automation, p.266-271, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164888]
• 96: Alan J. Hu , David L. Dill , Andreas Drexler , C. Han Yang, Higher-Level Specification and Verification with BDDs, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.82-95, June 29-July 01, 1992
• 97: Alan J. Hu , Gary York , David L. Dill, New techniques for efficient verification with implicitly conjoined BDDs, Proceedings of the 31st annual conference on Design automation, p.276-282, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196377]
• 98: Warren A. Hunt, Jr., Microprocessor design verification, Journal of Automated Reasoning, v.5 n.4, p.429-460, Dec. 1989
• 99: Warren A. Hunt, Jr., FM8501: a verified microprocessor, Springer-Verlag, London, 1994
• 100: C. Norris Ip , David L. Dill, Better verification through symmetry, Formal Methods in System Design, v.9 n.1-2, p.41-75, Aug. 1996 [doi>10.1007/BF00625968]
• 101: C. Norris Ip , David L. Dill, State reduction using reversible rules, Proceedings of the 33rd annual conference on Design automation, p.564-567, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240625]
• 102: Paul B. Jackson, Nuprl and Its Use in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, p.311-336, June 22-24, 1992
• 103: JAIN, J., ABRAHAM, J. A., BITNER, J., AND FUSSELL, D. S. 1996. Probabilistic verification of boolean functions. Formal Methods Syst. Des. 1, 1 (July), 63-115.
• 104: Jawahar Jain , Amit Narayan , M. Fujital , A. Sangiovanni-Vincentelli, Formal Verification of Combinational Circuit, Proceedings of the Tenth International Conference on VLSI Design: VLSI in Multimedia Applications, p.218, January 04-07, 1997
• 105: Robert B. Jones , David L. Dill , Jerry R. Burch, Efficient validity checking for processor verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.2-6, November 05-09, 1995, San Jose, California, United States
• 106: JOYCE, J. J. 1988. Formal verification and implementation of a microprocessor. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam, Eds. Kluwer Academic Publishers, Hingham, MA, 129-157.
• 107: Jeffrey J. Joyce , Carl-Johan H. Seger, Linking BDD-based symbolic evaluation to interactive theorem-proving, Proceedings of the 30th international conference on Design automation, p.469-474, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164981]
• 108: Deepak Kapur , Hantao Zhang, RRL: A Rewrite Rule Laboratory, Proceedings of the 9th International Conference on Automated Deduction, p.768-769, May 23-26, 1988
• 109: KAUFMANN, M. AND MOORE, J. S. 1994. Design goals for ACL2. Tech. Rep. 101. Computational Logic, Inc., Austin, TX.
• 110: KAUFMANN, M. AND MOORE, J. S. 1996. ACL2: an industrial strength version of Nqthm. In Proceedings of the 11th Annual Conference on Computer Assurance (COMPASS '96, Gaithersburg, MD, June), S. Faulk and C. Heitmayer, Eds. 23-34.
• 111: Yonit Kesten , Zohar Manna , Hugh McGuire , Amir Pnueli, A Decision Algorithm for Full Propositional Temporal Logic, Proceedings of the 5th International Conference on Computer Aided Verification, p.97-109, June 28-July 01, 1993
• 112: KLEENE, S. C. 1967. Mathematical Logic. John Wiley & Sons, Inc., New York, NY.
• 113: Carlos Delgado Kloos , Peter T. Breuer, Formal Semantics for VHDL, Kluwer Academic Publishers, Norwell, MA, 1995
• 114: KOZEN, D. 1993. Results on the propositional tL-calculus. Theor. Comput. Sci. 27, 3 (Dec.), 333-354.
• 115: A. Kuehlmann , A. Srinivasan , D. P. LaPotin, Verity—a formal verification program for custom CMOS circuits, IBM Journal of Research and Development, v.39 n.1-2, p.149-165, Jan./March 1995
• 116: Ramayya Kumar , Christian Blumenröhr , Dirk Eisenbiegler , Detlef Schmid, Formal Synthesis in Circuit Design - A Classification and Survey, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.294-309, November 06-08, 1996
• 117: Ramayya Kumar , Klaus Schneider , Thomas Kropf, Structuring and automating hardware proofs in a higher-order theorem-proving environment, Formal Methods in System Design, v.2 n.2, p.165-223, April 1993 [doi>10.1007/BF01383880]
• 118: R. P. Kurshan, Analysis of discrete event coordination, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.414-453, May 1990, Mook, The Netherlands
• 119: R. P. Kurshan, Formal verification in a commercial setting, Proceedings of the 34th annual conference on Design automation, p.258-262, June 09-13, 1997, Anaheim, California, United States [doi>10.1145/266021.266089]
• 120: Robert P. Kurshan , Leslie Lamport, Verification of a Multiplier: 64 Bits and Beyond, Proceedings of the 5th International Conference on Computer Aided Verification, p.166-179, June 28-July 01, 1993
• 121: Y.-T. Lai , S. Sastry, Edge-valued binary decision diagrams for multi-level hierarchical verification, Proceedings of the 29th ACM/IEEE conference on Design automation, p.608-613, June 08-12, 1992, Anaheim, California, United States
• 122: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 123: Leslie Lamport , Fred B. Schneider, The ``Hoare Logic'' of CSP, and All That, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.2, p.281-296, April 1984 [doi>10.1145/2993.357247]
• 124: Trevor W. S. Lee , Mark R. Greenstreet , Carl-Johan Seger, Automatic Verification of Asynchronous Circuits, IEEE Design & Test, v.12 n.1, p.24-31, March 1995 [doi>10.1109/54.350687]
• 125: Wing Sang Lee , Mark R. Greenstreet , Carl-Johan H. Seger, Automatic Verification of Refinement, Proceedings of the1994 IEEE International Conference on Computer Design: VLSI in Computer & Processors, p.225-229, October 10-12, 1994
• 126: Miriam Leeser , John W. O'Leary, Verification of a subtractive radix-2 square root algorithm and implementation, Proceedings of the 1995 International Conference on Computer Design: VLSI in Computers and Processors, p.526-531, October 02-04, 1995
• 127: Daniel Lenoski , James Laudon , Kourosh Gharachorloo , Wolf-Dietrich Weber , Anoop Gupta , John Hennessy , Mark Horowitz , Monica S. Lam, The Stanford Dash Multiprocessor, Computer, v.25 n.3, p.63-79, March 1992 [doi>10.1109/2.121510]
• 128: Ian Leslie , Derek McAuley, Fairisle: an ATM network for the local area, ACM SIGCOMM Computer Communication Review, v.21 n.4, p.327, Sept. 1991
• 129: Jeremy Levitt , Kunle Olukotun, A scalable formal verification methodology for pipelined microprocessors, Proceedings of the 33rd annual conference on Design automation, p.558-563, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240624]
• 130: Jean-Christophe Madre , Jean-Paul Billon, Proving circuit correctness using formal comparison between expected and extracted behaviour, Proceedings of the 25th ACM/IEEE conference on Design automation, p.205-210, June 12-15, 1988, Atlantic City, New Jersey, United States
• 131: MADRE, J. C., COUDERT, O., AND BILLON, J. P. 1989. Automating the diagnosis and the rectification of design errors with PRIAM. In Proceedings of the International Conference on Computer-Aided Design (ICCAD, Nov.). 30-33.
• 132: MALIK, S., WANG, A., BRAYTON, R., AND SANGIOVANNI-VINCENTELLI, A. 1988. Logic verification using binary decision diagrams in a logic synthesis environment. In Proceedings of the International Conference on Computer-Aided Design (ICCAD '88, Santa Clara, CA, Nov.). 6-9.
• 133: Z Manna , Anuchit Anuchitanukul , Nikolaj Bjorner , Anca Browne , Edward Chang , Michael Colon , Luca de Alfaro , Harish Devarajan , Henny Sipma , Tomas Uribe, STeP: The Stanford Temporal Prover, Stanford University, Stanford, CA, 1994
• 134: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 135: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 136: Niels Maretti, Mechanized Verification of Refinement, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.185-202, September 26-28, 1994
• 137: MCCUNE, W. 1994. OTTER 3.0. Preprint MCS-P399-1193. Argonne National Laboratory, Argonne, IL.
• 138: MCFARLAND, M. C. 1993. Formal verification of sequential hardware: A tutorial. IEEE Trans. Comput.-Aided Des. Integr. Circuits 12, 5 (May), 663-654.
• 139: Kenneth Lauchlin McMillan, Symbolic model checking: an approach to the state explosion problem, Carnegie Mellon University, Pittsburgh, PA, 1992
• 140: K. L. McMillan, Fitting formal methods into the design cycle, Proceedings of the 31st annual conference on Design automation, p.314-319, June 06-10, 1994, San Diego, California, United States [doi>10.1145/196244.196392]
• 141: Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
• 142: MCMILLAN, K. L. AND SCHWALBE, J. 1991. Formal verification of the Encore Gigamax cache consistency protocol. In Proceedings of the 1991 International Symposium on Shared Memory Multiprocessors.
• 143: MELHAM, T. F. 1988. Abstraction mechanisms for hardware verification. In VLSI Specification, Verification and Synthesis, G. Birtwistle and P. Subrahmanyam, Eds. Kluwer Academic Publishers, Hingham, MA, 267-291.
• 144: S. P. Miller , M. Srivas, Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods, Proceedings of the 1st Workshop on Industrial-Strength Formal Specification Techniques, p.2, April 05-08, 1995
• 145: Paul S. Miner , James F. Leathrum, Verification of IEEE Compliant Subtractive Division Algorithms, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.64-78, November 06-08, 1996
• 146: MOORE, J. S., LYNCH, T., AND KAUFMANN, M. 1996. Mechanically checked proof of the correctness of the kernel of the AMDI~86TM floating-point division algorithm, http://devil.ece.utexas.edu:80/Mynch/divide/divide.html.
• 147: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 148: NOWATZYK, A., AYBAY, G., BROWNE, M., KELLY, E., PARKIN, M., RADKE, W., AND VISHIN, S. 1995. The S3.mp scalable shared memory multiprocessor. In Proceedings of the 9th International Symposium on Parallel Processing (Apr.).
• 149: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 150: Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
• 151: Sam Owre , John M. Rushby , Natarajan Shankar, PVS: A Prototype Verification System, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.748-752, June 15-18, 1992
• 152: Shipra Panda , Fabio Somenzi, Who are the variables in your neighborhood, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.74-77, November 05-09, 1995, San Jose, California, United States
• 153: Manish Pandey , Richard Raimi , Derek L. Beatty , Randal E. Bryant, Formal verification of PowerPC arrays using symbolic trajectory evaluation, Proceedings of the 33rd annual conference on Design automation, p.649-654, June 03-07, 1996, Las Vegas, Nevada, United States [doi>10.1145/240518.240641]
• 154: PAULSON, L. C. 1994. Isabelle: A generic theorem prover. In Lecture Notes in Computer Science, vol. 828. Springer-Verlag, New York.
• 155: PIXLEY, C., JEONG, S.-W., AND HACHTEL, G. D. 1994. Exact calculation of synchronizing sequences based on binary decision diagrams. IEEE Trans. Comput.-Aided Des. Integr. Circuits 13, 8 (Aug.), 1024-1034.
• 156: PNUELI, A. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 46-57.
• 157: A Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
• 158: Fong Pong , Michel Dubois, The verification of cache coherence protocols, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.11-20, June 30-July 02, 1993, Velen, Germany [doi>10.1145/165231.165233]
• 159: Fong Pong , Andreas Nowatzyk , Gunes Aybay , Michel Dubois, Verifying Distributed Directory-Based Cahce Coherence Protocols: S3.mp, a Case Study, Proceedings of the First International Euro-Par Conference on Parallel Processing, p.287-300, August 29-31, 1995
• 160: S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995
• 161: Kavita Ravi , Fabio Somenzi, High-density reachability analysis, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.154-158, November 05-09, 1995, San Jose, California, United States
• 162: Richard Rudell, Dynamic variable ordering for ordered binary decision diagrams, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.42-47, November 07-11, 1993, Santa Clara, California, United States
• 163: Harald Rueß , Natarajan Shankar , Mandayam K. Srivas, Modular Verification of SRT Division, Proceedings of the 8th International Conference on Computer Aided Verification, p.123-134, August 03, 1996
• 164: James B. Saxe , James J. Horning , John V. Guttag , Stephen J. Garland, Using transformations and verification in circuit design, Formal Methods in System Design, v.3 n.3, p.181-209, Dec. 1993 [doi>10.1007/BF01384073]
• 165: Klaus Schneider , Thomas Kropf, A Unified Approach for Combining Different Formalisms for Hardware Verification, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.202-217, November 06-08, 1996
• 166: Carl Seger, VOSS - A Formal Hardware Verification System User''s Guide, University of British Columbia, Vancouver, BC, Canada, 1993
• 167: Carl-Johan H. Seger , Randal E. Bryant, Formal verification by symbolic evaluation of partially-ordered trajectories, Formal Methods in System Design, v.6 n.2, p.147-189, March 1995 [doi>10.1007/BF01383966]
• 168: SENTOVICH, E., SINGH, K., LAVAGNO, L., MOON, C., MURGAI, R., SALDANHA, A., SAVOJ, H., STEPHAN, P., BRAYTON, R., AND SANGIOVANNI-VINCENTELLI, A. 1992. SIS: A system for sequential circuit synthesis. Tech. Rep. UCB/ERL M92/41. UC Berkeley, Berkeley, CA.
• 169: A. Udaya Shankar, An introduction to assertional reasoning for concurrent systems, ACM Computing Surveys (CSUR), v.25 n.3, p.225-262, Sept. 1993 [doi>10.1145/158439.158441]
• 170: Robert E. Shostak, A Practical Decision Procedure for Arithmetic with Function Symbols, Journal of the ACM (JACM), v.26 n.2, p.351-360, April 1979 [doi>10.1145/322123.322137]
• 171: Robert E. Shostak, Deciding Combinations of Theories, Journal of the ACM (JACM), v.31 n.1, p.1-12, Jan. 1984 [doi>10.1145/2422.322411]
• 172: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 173: Mandayam Srivas , Mark Bickford, Formal Verification of a Pipelined Microprocessor, IEEE Software, v.7 n.5, p.52-64, September 1990 [doi>10.1109/52.57892]
• 174: Mandayam K. Srivas , Steven P. Miller, Applying formal verification to the AAMP5 microprocessor: a case study in the industrial use of formal methods, Formal Methods in System Design, v.8 n.2, p.153-188, March 1996 [doi>10.1007/BF00122419]
• 175: Jorgen Staunstrup, A Formal Approach to Hardware Design, Kluwer Academic Publishers, Norwell, MA, 1994
• 176: Jørgen Staunstrup , Stephen J. Garland , John V. Guttag, Mechanized Verification of Circuit Descriptions Using the Larch Prover, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, p.277-299, June 22-24, 1992
• 177: Jørgen Staunstrup , Niels Mellergaard, Localized verification of modular designs, Formal Methods in System Design, v.6 n.3, p.295-320, June 1995 [doi>10.1007/BF01384501]
• 178: Ulrich Stern , David L. Dill, Automatic verification of the SCI cache coherence protocol, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.21-34, October 02-04, 1995
• 179: Sofiène Tahar , Paul Curzon, A Comparison of MDG and HOL for Hardware Verification, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, p.415-430, August 26-30, 1996
• 180: Sofiène Tahar , Ramayya Kumar, Implementing a Methodology for Formally Verifying RISC Processors in HOL, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, p.281-294, August 11-13, 1993
• 181: S. Tahar , Z. Zhou , X. Song , E. Cerny , Michel Langevin, Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs, Proceedings of the 6th Great Lakes Symposium on VLSI, p.106, March 22-23, 1996
• 182: TARSKI, A. 1951. Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA.
• 183: Wolfgang Thomas, Automata on infinite objects, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 184: TOUATI, H. J., SAVOJ, H., LIN, B., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. 1990. Implicit state enumeration of finite state machines using BDDs. In Proceedings of the International Conference on Computer-Aided Design (ICCAD'90). 130-133.
• 185: John Van Tassel, A Formalisation of the VHDL Simulation Cycle, Proceedings of the IFIP TC10/WG10.2 Workshop on Higher Order Logic Theorem Proving and its Applications, p.359-374, September 21-24, 1992
• 186: VARDI, M. AND WOLPER, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the First Annual Symposium on Logic in Computer Science (Cambridge, MA, June16-18). IEEE Computer Society Press, Los Alamitos, CA, 332-344.
• 187: Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
• 188: Moshe Y. Vardi , Pierre Wolper, Reasoning about infinite computations, Information and Computation, v.115 n.1, p.1-37, Nov. 15, 1994 [doi>10.1006/inco.1994.1092]
• 189: Ronald J. Vetter, ATM concepts, architectures, and protocols, Communications of the ACM, v.38 n.2, p.30-ff., Feb. 1995 [doi>10.1145/204826.204831]
• 190: WEIH, D. AND GREENSTREET, M. 1996. Verifying asynchronous data path circuits. IEE Proc. Comput. Digit. Tech. 143, 5 (Sept.), 295-300.
• 191: Phillip J. Windley, Abstract Theories in HOL, Proceedings of the IFIP TC10/WG10.2 Workshop on Higher Order Logic Theorem Proving and its Applications, p.197-210, September 21-24, 1992
• 192: Phillip J. Windley, Formal Modeling and Verification of Microprocessors, IEEE Transactions on Computers, v.44 n.1, p.54-72, January 1995 [doi>10.1109/12.368009]
• 193: WINDLEY, P.J. 1995. Verifying pipelined microprocessors. Tech. Rep.. Brigham Young University, Provo, UT.
• 194: Phillip J. Windley , Michael L. Coe, A Correctness Model for Pipelined Multiprocessors, Proceedings of the Second International Conference on Theorem Provers in Circuit Design - Theory, Practice and Experience, p.33-51, September 26-28, 1994
• 195: WOLPER, P. 1984. Temporal logic can be more expressive. Inf. Control 56, 1/2 (Jan./Feb. 1983), 72-99.
• 196: Xu, Y., CERNY, E., SILBURT, A., AND HUGHES, R. B. 1997. Property verification using theorem proving and model checking.
• 197: Zheng Zhu , Carl-Johan H. Seger, The Completeness of a Hardware Inference System, Proceedings of the 6th International Conference on Computer Aided Verification, p.286-298, June 21-23, 1994

INDEX TERMS

Primary Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

Additional Classification:
  A. General Literature

General Terms:
Design, Verification

Keywords:
case studies, formal methods, formal verification, hardware verification, language containment, model checking, survey, theorem proving