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.

This is joint work with Mark Aagaard, Robert Jones, John O'Leary, and Carl Seger.
Tom Melham, last updated in December 2011.