Introduction to Assertion-Based Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 446

t 2

t 1

— detected bug

Fig. 20.6 Hybrid verification

pure FV. Actually, hybrid verification is a special case of underapproximation. There
are many variations of hybrid verification methods, but usually their main idea is to
interleave conventional or random simulation and FV [ 17 , 42 ].
The concept of hybrid verification is illustrated in Fig. 20.6 . The design is
simulated until simulation time t 1 , and starting from the system state in time t 1
bounded FV is performed. Then the system is simulated until another time moment
t 2 , and bounded FV is performed again starting from the new state of the system, and
so on. Figure 20.6 shows a case when no bugs have been found during the proper
simulation, but two bugs are detected by bounded FV in neighborhoods of states of
the simulation trace.
Hybrid verification requires that state information from the design and assertions
can be mapped between the simulation and formal model. In turn this may require
that the design and the assertions be synthesizable.

Exercises

20.1. What are counterexamples and witnesses? What is the purpose of reporting
counterexamples and witnesses in formal verification?

20.2. Assume that in Fig. 1.7 Line 9 is omitted. Provide a counterexample exhibit-
ing violation of check_shift .
20.3. Based on the shift register shown in Fig. 1.7 , provide a witness for the
following cover statement:

cover property (@( posedge clk) disable iff (rst)
shift_reg == 8'b10000000 && ##1 8'b000000010);

20.4. What are complete and incomplete methods in formal verification?

20.5. What is the meaning of abstraction as used in formal verification?