Formal verification of sequential hardware: a tutorial

Abstract
Formal verification involves the use of analytical techniques to prove that the implementation of a system conforms to the specification. The specification could be a set of properties that the system must have, or it could be an alternative representation of the system behavior. Recently, there has been increased interest in the role of formal verification in hardware development. Partly, this is because the hardware being designed now is so complex that exhaustive simulation is no longer possible, so that other techniques are needed to complement simulation. Another reason for the renewed interest is that, as formal verification techniques have become more sophisticated, they have been shown to be usable on sizable pieces of hardware, not just on toy examples. In this paper, we will look at various formal verification techniques and how they can be applied to sequential hardware, especially at the register-transfer level. We will begin with the basic elements of a verification system, as illustrated on the relatively simple problem of verifying combinational circuits. Then we will consider the more complex problems involved in analyzing sequential systems and the techniques that have been developed to solve them. Throughout, we will focus on those techniques whose utility has been demonstrated on real systems, including higher order logic, temporal logic, predicate transformers, state-machine models, and model checkers.

This publication has 45 references indexed in Scilit: