SOFSEM 2001 28th Annual Conference on Current Trends in Theory and Practice of Informatics November 24 - December 1, 2001 Piestany, Slovak Republic, Europe

Formal Verification Methods for Industrial Hardware Design

by Anna Slobodova

Functional validation of hardware designs is a major challenge for circuit design companies. Unlike software bugs that can be patched by post-delivery software releases, post-delivery hardware bugs are very expensive to correct. Simulation remains the dominating validation method for functional verification, but in the last decade formal verification (FV) has emerged as an important complementary verification approach. In our presentation, we describe basic FV methods -- equivalence checking, symbolic trajectory evaluation, model checking, and theorem proving. We illustrate these methods on examples taken from applying FV techniques to the Alpha microprocessor design. Although theoretically FV can provide much more complete verification coverage than testing, our ability to apply FV is limited due to capacity limits of existing tools and availability of trained personnel. The application of formal methods to industrial designs is an active research area with huge opportunities for researchers from academia and industry.