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.