Formal Hardware Verification

Formal Verification Links

J.M. Wing, A Specifier's Introduction to Formal Methods. IEEE Computer, 23(9):8-24, September 1990.
Snook and Harison, Practitioners Views on the Use of Formal Methods, Information and Software Technology 43 (2001) 275 - 283.
Annette Bunker and Ganesh Gopalalkrishnan, Formal Hardware Specification Languages for Protocol Compliance Verification
Annette Bunker, Sally A. McKee and Ganesh Gopalakrishnan, An Overview of Formal Hardware Specification Languages

Colin Snook, Using a Graphical Design Tool for Formal Specification, University of Southampton (converting UML to the B language).
See also, Bunker - An Overview of Formal Hardware Specification Languages (in Formal Specification)

Randal E. Bryant's (Carnegie Mellon University) publication list with documents available.
Alan J. Hu, Formal Hardware Verification with BDDs: An Introduction, IEEE Pacific Rim Conference on Communications, Computers, and Signal Processing (PACRIM), pp.677-682, 1997.
Randal Bryant, "Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification", International Conference on Computer-Aided Design, pp. 236-243, 1995.

Yuguo Sun, Model Checking - A Tutorial Introduction
An Introduction to Formal Verification, Sandeep K. Shukla
Symbolic Model Checking with BDDs, Edmund M. Clarke, Jr., Computer Science Department, Carnegie Mellon University

Chatterjee, P., "Streamline verification process with formal property verification to meet highly compressed design cycle," Design Automation Conference, 2005. Proceedings. 42nd , vol., no.pp. 674- 677, 13-17 June 2005
Abstract: In this paper, the author describes a methodology and tool flow for using formal verification effectively to reduce the verification burden in large custom ASIC designs.

EETimes.com mentions that Intel has been using Formal Verification techniques since the Pentium 2. Merced (now know as Itanum) also used formal verification techniques heavily.
Seger, C.-J.H.; Jones, R.B.; O'Leary, J.W.; Melham, T.; Aagaard, M.D.; Barrett, C.; Syme, D., "An Industrially Effective Environment for Formal Hardware Verification," Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on , vol.24, no.9pp. 1381- 1405, Sept. 2005
Abstract: The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.

Bormann, J., Lohse, J., Payer, M., and Venzl, G. 1995. Model checking in industrial hardware design. In Proceedings of the 32nd ACM/IEEE Conference on Design Automation (San Francisco, California, United States, June 12 - 16, 1995). DAC '95. ACM Press, New York, NY, 298-303. DOI= http://doi.acm.org/10.1145/217474.217545.
Abstract: This paper describes how model checking has been integrated into an industrial hardware design process. We present an application oriented specifcation language for assumption/commitment style properties and an abstraction algorithm that generates an intuitive and effcient representation of synchronous circuits. These approaches are embedded in our Circuit Verifcation Environment CVE. They are demonstrated on two industrial applications.

Beer, I.; Ben-David, S.; Eisner, C.; Landver, A., "RuleBase: an industry-oriented formal verification tool," Design Automation Conference Proceedings 1996, 33rd , vol., no.pp.655-660, 3-7 Jun, 1996
Abstract: RuleBase is a formal verification tool, developed by the IBM Haifa Research Laboratory. It is the result of three years of experience in practical formal verification of hardware which, we believe, has been a key factor in bringing the tool to its current level of maturity. We present the tool, including several unique features, and summarize our usage experience.