Does Your Design Meet Its Specs? Introduction to Hardware Design Verification
This chapter is from the book
This chapter is from the book
This chapter is from the book
Chapter Highlights
- What is design verification?
- The basic verification principle
- Verification methodology
- Simulation-based verification versus formal verification
- Limitations of formal verification
- A quick overview of Verilog scheduling and execution semantics
From the makeup of a project team, we can see the importance of design verification. A typical project team usually has an equal number of design engineers and verification engineers. Sometimes verification engineers outnumber design engineers by as many as two to one. This stems from the fact that to verify a design, one must first understand the specifications as well as the design and, more important, devise a different design approach from the specifications. It should be emphasized that the approach of the verification engineer is different from that of the design engineer. If the verification engineer follows the same design style as the design engineer, both would commit the same errors and not much would be verified.
From the project development cycle, we can understand the difficulty of design verification. Statistical data show that around 70% of the project development cycle is devoted to design verification. A design engineer usually constructs the design based on cases representative of the specifications. However, a verification engineer must verify the design under all cases, and there are an infinite number of cases (or so it seems). Even with a heavy investment of resources in verification, it is not unusual for a reasonably complex chip to go through multiple tape-outs before it can be released for revenue.
The impact of thorough design verification cannot be overstated. A faulty chip not only drains budget through respin costs, it also delays time-to-market, impacts revenue, shrinks market share, and drags the company into playing the catch-up game. Therefore, until people can design perfect chips, or chip fabrication becomes inexpensive and has a fast turnaround time, design verification is here to stay.
1.1 What Is Design Verification?
A design process transforms a set of specifications into an implementation of the specifications. At the specification level, the specifications state the functionality that the design executes but does not indicate how it executes. An implementation of the specifications spells out the details of how the functionality is provided. Both a specification and an implementation are a form of description of functionality, but they have different levels of concreteness or abstraction. A description of a higher level of abstraction has fewer details; thus, a specification has a higher level of abstraction than an implementation. In an abstraction spectrum of design, we see a decreasing order of abstraction: functional specification, algorithmic description, register-transfer level (RTL), gate netlist, transistor netlist, and layout (Figure 1.1). Along this spectrum a description at any level can give rise to many forms of a description at a lower level. For instance, an infinite number of circuits at the gate level implements the same RTL description. As we move down the ladder, a less abstract description adds more details while preserving the descriptions at higher levels. The process of turning a more abstract description into a more concrete description is called refinement. Therefore, a design process refines a set of specifications and produces various levels of concrete implementations.
)
Figure 1.1 A ladder of design abstraction
Design verification is the reverse process of design. Design verification starts with an implementation and confirms that the implementation meets its specifications. Thus, at every step of design, there is a corresponding verification step. For example, a design step that turns a functional specification into an algorithmic implementation requires a verification step to ensure that the algorithm performs the functionality in the specification. Similarly, a physical design that produces a layout from a gate netlist has to be verified to ensure that the layout corresponds to the gate netlist. In general, design verification encompasses many areas, such as functional verification, timing verification, layout verification, and electrical verification, just to name a few. In this book we study only functional verification and refer to it as design verification. Figure 1.2 shows the relationship between the design process and the verification process.
)
Figure 1.2 The relationship between design and verification
On a finer scope, design verification can be further classified into two types. The first type verifies that two versions of design are functionally equivalent. This type of verification is called equivalence checking. One common scenario of equivalence checking is comparing two versions of circuits at the same abstraction level. For instance, compare the gate netlist of a prescan circuit with its postscan version to ensure that the two are equivalent under normal operating mode.
However, the two versions of the design differ with regard to abstraction level. For example, one version of the design is at the level of specification and the other version is at the gate netlist level. When the two versions differ substantially with regard to level of abstraction, they may not be functionally equivalent, because the lower level implementation may contain more details that are allowed, but are unspecified, at the higher level. For example, an implementation may contain timing constraints that are not part of the original specification. In this situation, instead of verifying the functional equivalence of the two versions, we verify instead that the implementation satisfies the specifications. Note that equivalence checking is two-way verification, but this is a one-way verification because a specification may not satisfy an unspecified feature in the implementation. This type of verification is known as implementation verification, property checking, or model checking. Based on the terminology of property checking, the specifications are properties that the implementation must satisfy. Based on the terminology of model checking, the implementation or design is a model of the circuit and the specifications are properties. Hence, model checking means checking the model against the properties.