Free Trial

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

Share this Page URL

CHAPTER 9 Functional verification > 9.5 Formal approaches - Pg. 540

540 CHAPTER 9 Functional verification can check implementation details, whereas in black-box verification, assertions check against the specification through both module inputs and outputs. For higher-level verification, checker assertions are used to monitor the interfaces across components. Because the interfaces must abide by their corresponding protocols, checker assertions signal errors once unexpected scenarios occur. A two-hot message in a one-hot coded bus is such an example. Writing assertions One of the most frequently asked questions in assertion-based verification is "Who should write the assertions?" In practice, this job is shared by the entire design and verification team. At different levels of the design abstraction, differ- ent properties are converted into assertions. It may be difficult to ask a designer responsible for designing a small block and lacking a system-level view to write high-level assertions. At the architectural level, a design is described by use of the input/output functions of each component and the interface protocols that connect them, without implementation detail. Assertions at this level model high-level relation- ships and ensure that system-level behavior is consistent with the system-level specification. Also at this level, observation points are located at inputs and out- puts of the components and at bus interfaces only. Assertions try to capture one's understanding of the design intent. Once a design component is created, the designer can write assertions for it on the basis of the functionality from the specification and the implementation he or she chooses. At this level, assertions are frequently used for debugging and for measuring coverage. If applicable, verification engineers may use formal methods to prove asser- tions to complement the deficiencies of simulation-based methods. Also, asser- tions accompanied with IP cores from IP providers would need to be integrated into the verification plan. 9.5 FORMAL APPROACHES Advances in modern simulators allow full-chip simulation to be efficiently con- ducted. Nevertheless, the success of simulation-based verification remains dependent largely on the quality of the stimuli. The stimuli exercise a design under verification (DUV) and traverse its state space. Verification can be con- sidered as a process of exploring reachable state space of the design. Modern designs rapidly increase in size and complexity, and, consequently, their reach- able state space can grow exponentially. As a result, it becomes difficult to exhaust all reachable states for complete verification by use of only simulation. Formal approaches aim to make complete verification possible, where com- pleteness is in the sense that all reachable states are explored. The underlying idea is to infer the design properties by reasoning without explicitly simulating