Free Trial

Safari Books Online is a digital library providing on-demand subscription access to thousands of learning resources.

  • Create BookmarkCreate Bookmark
  • Create Note or TagCreate Note or Tag
  • PrintPrint
Share this Page URL
Help

Chapter 1. An Invitation to Design Verification > What Is Design Verification?

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.

  • Safari Books Online
  • Create BookmarkCreate Bookmark
  • Create Note or TagCreate Note or Tag
  • PrintPrint