In this chapter, we apply the verification process of Chapter 10, Post-Partitioning verification to implementation models of the hardware and software. The hardware models will be implemented at the RT rather than the behavioral level. The software will comprise the actual embedded production code of the design compiled for the target processor. The verification plan developed in Chapter 10 is extended to address the particular needs of these lower-level abstraction models.

On the road to a unified design and verification process, functional coverage and generation are both candidates for improved fidelity and performance. Coverage models may better reflect design requirements by incorporating heterogeneous metric sources and giving equal weight to temporal behavior. Almost all coverage models today are composed of attributes derived from the design data domain: input, output, and internal sources. More precise models make use of structural, property, and sequential coverage metrics.

Likewise, complementary improvements are possible in stimulus generation by encompassing temporal expressions in generation constraints. Also, coveragedirected generation dramatically increases the rate of coverage closure. In this chapter, we discuss hybrid verification approaches such as simulate-then-prove and prove-then-simulate.

Beginning with verification planning, the scope of the implementation verification problem will be refined from the earlier feature set to comprehend the details available at this level. For example, algorithmic features captured in coverage models after partitioning need to be augmented with architectural and microarchitectural features present at this level. FSM implementation corner cases and software data structure limits must be captured in the coverage models of this plan section.

The solution to the implementation verification problem must also accommodate the realities of RTL and embedded production software. A primary difference is that the complexity and size of both the hardware and software code is much larger, resulting in slower execution speeds for any dynamic verification environment. This demands higher coverage density from any stimulus generator and restricts the module sizes that may be verified using static verification (e.g., model checking).

The coverage model design process—top-level design, detailed design, and implementation—is the same for implementation verification as it is for postpartitioning verification. However, the abstraction level of the attributes, their sampling times, correlation times, and model structure, is lower and more detailed.

13.1 What This Chapter Is Not About
13.2 Positive and Negative Verification
13.3 Verification Focus
13.4 Clear Box Verification
13.5 Verification IP
    13.5.1 Dynamic Verification IP
    13.5.2 Assertion Libraries
13.6 Properties and Assertions
    13.6.1 Assertions
    13.6.2 Formal Methods
        13.6.2.1 Starting State
        13.6.2.2 Limiting the Future
        13.6.2.3 Speeding Up the Design
        13.6.2.4 Limiting States
13.7 Coverage
13.8 System Verification
13.9 Post-Silicon Debug
    13.9.1 Observability and Debug
        13.9.1.1 Processors
        13.9.1.2 Internal Logic Analyzer
    13.9.2 Dynamic Modifications
13.10 Provocative Thoughts
    13.10.1 Sequential Equivalence Checking
    13.10.2 Property-Based Design
13.11 Summary
13.12 The Prescription

Errata

Feedback