In this chapter the authors briefly review techniques used in formal hardware verification. An advanced flow emerges from integrating two major methodological improvements: debugging support and coverage analysis. The verification engineer can locate the source of a failure with an automatic debugging support. Components are identified which explain the discrepancy between the property and the circuit behavior. This method is complemented by an approach to analyze functional coverage of the proven Bounded Model Checking (BMC) properties. The approach automatically determines whether the property set is complete or not. In the latter case coverage gaps are returned. Both techniques are integrated in an enhanced verification flow. A running example demonstrates the resulting advantages.
Top1 Introduction
For economic reasons the number of components in integrated circuits grows at an exponential pace according to Moore’s law. This growth is expected to continue for another decade. Resulting is the so-called design gap – the productivity in circuit design does not increase as fast as the technical capabilities. Thus, more components can be integrated on a physical device than can be assembled in a meaningful way during circuit design. The verification gap, i.e. how to ensure the correctness of a design, is even wider. This is of particular importance in safety critical areas like traffic or security related systems storing confidential information. Thus, techniques and tools for the verification of circuits received a lot of attention in the area of Computer Aided Design (CAD).
Simulation has always been in use as a fast method to validate the expected functionality of circuits. Once the circuit is described in a Hardware Description Language (HDL) like Verilog or VHDL, a test bench is used to excite the circuit under stimuli expected during in-field operation. But the full space of potential assignments and states of a circuit is exponential in the number of inputs and state elements. Therefore the search space cannot be exhausted by simulation. Even emulation using prototypical hardware is not sufficient to completely cover the full state space.
Thus, more powerful techniques for formal verification have been developed. In particular, to prove the correctness of a hardware design with respect to a given textual specification property checking (or model checking) has been developed. Formal properties are derived from the textual specification. The properties are proven fully automatically to hold on the design. In Symbolic Model Checking (Burch et. al, 1990; Bryant, 1995) Binary Decision Diagrams (BDDs) (Bryant, 1986) are used to represent the state space symbolically. This approach has been used successfully in practice. However, BDDs may suffer from memory explosion. As an alternative methods based on Boolean Satisfiability (SAT) have been proposed. In Bounded Model Checking (BMC) (Biere et al., 1999) the system is unfolded for k time frames and together with the property converted into a SAT problem. If the corresponding SAT instance is satisfiable, a counter-example of length k has been found. Due to the significant improvements in the tools for SAT solving BMC is particularly effective. Even for very large designs meaningful properties can be handled (Amla et al., 2005; Ngyuen et al., 2008). Still the verification gap remains due to low productivity, and intensive training of verification engineers is required to apply property checking in practice. Therefore besides powerful reasoning engines, tool support is necessary for several tasks during formal verification.
Here we propose an enhanced verification flow enriched by techniques to ease the verification task. The flow is based on previous results by the authors. Figure 1 illustrates this flow. Dark boxes denote automatic tools while light boxes require manual interaction.
Typically only a property checker is available that returns a counter-example if a property fails. The subsequent debugging task is only supported by standard simulators. But techniques automating debugging in the context of property checking have been presented (Fey et al., 2008) to speed up the work flow. The debugger uses multiple counter-examples to determine candidate sites for the bug location and thus decreases the amount of manual interaction.
Another major problem in property checking is to decide when a property set is complete. This is usually done by manual inspection of all properties – a threat to correctness for any larger design. The work in (Große, Kühne, & Drechsler, 2008) automates this step. The coverage analyzer determines whether the properties describe the behaviour of the design under all possible input stimuli. If some input sequences are not covered, this scenario is returned to the verification engineer for manual inspection. Additional properties may be required or existing properties have to be modified.