Methodology for Practical, Industrial-Scale Formal Verification

Successful use of formal verification in hardware designs of industrial scale requires the best available theoretical basis for verification technology, embodied in highly tuned and well-engineered software implementations. But any serious attempt at practical industrial verification faces many further difficulties, in addition to algorithm capacity and implementation efficiency. Equally important is addressing the problem of managing the complexity of the verification activity itself.

This work, done in collaboration with researchers at Intel Corporation's Strategic CAD Labs, attacks this problem by coupling research into verification algorithms and implementation engineering with research on verification methodology. What we mean by ‘methodology’ is a systematic approach to organising a large verification effort. This includes a clearly articulated plan for the sequence and purpose of each of the many interdependent activities of a typical verification project, together with a guiding structure for the verification code artifacts to be produced.

An overview article in IEEE Design & Test, 2001:
Practical Formal Verification in Microprocessor Design, R. B. Jones, J. W. O'Leary, C.-J. H. Seger, M. D. Aagaard, and T. F. Melham, IEEE Design & Test of Computers, 18(4):16-25, July/August 2001.
A longer article from FMCAD 2000:
A Methodology for Large-Scale Hardware Verification, M. D. Aagaard, R. B. Jones, T. F. Melham, J. W. O'Leary, and C.-J. H. Seger, in Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000: Proceedings, edited by W. A. Hunt, Jr. and S. D. Johnson, Lecture Notes in Computer Science, vol. 1954 (Springer-Verlag, 2000), pp. 263-282.
A presentation given by Robert Jones at FMCAD 2000:
A Methodology for Large-Scale Hardware Verification (PDF of presentation)
Abstract of a talk at ARW 2003:
Abstract: Experience with Practical Formal Verification at an Industrial Scale, T. Melham, in Proceedings of the Tenth Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice: 15th-16th April 2003, edited by C. Dixon (University of Liverpool, 2003), pp. 1-2.

This is joint work with Mark Aagaard, Robert Jones, John O'Leary, and Carl Seger.

Tom Melham, last updated in December 2011.