Formal Verification in Hardware Design: A Survey
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 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 which have been proposed
in the literature and applied to actual designs. The specification
frameworks we introduce include temporal logics, predicate logic,
abstraction and refinement, as well as containment between $\go$-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 have been applied to industrial-scale designs, such as
microprocessors, floating-point hardware, protocols, memory subsystems, and
communications hardware.