Hardware equivalence and property verification

In this chapter we survey the two most important hardware verification problems: equivalence checking and property verification. The objective of equivalence checking is to ensure that, in a design developed through phases that refine previous stages, the refinement process preserves the original behavior. In theory these transformations should be correct by construction; however the same tools that perform them should be formally verified, and the process would be endless. In property verification, given a transition system, we test whether the informal description of the specification has been captured correctly by a formal description with a hardware description language, by checking whether the system satisfies some property. Properties capture functionality, timing and temporal relations, safety (is it possible for a bad event to happen ?), liveness (does an expected good event eventually take place ?) and fairness (does every request eventually receive service ?). In this chapter we focus on safety properties because they are the most commonly used in hardware verification. Their violation can be detected by analyzing finite executions of the system. They can be posed as checking that some property holds in the reachable states of system starting from the initial state(s). This checking justifies the crucial role played by reachability analysis in the verification of safety properties.