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

only for the most critical blocks, where correctness is crucial and simulation is too
unreliable. Examples include multipliers, dividers, other arithmetic units, arbiters,
coherency managers, branch predictors, critical controllers, bus protocols, etc.
Verifying that assertions hold on a design is the primary purpose of FV, yet
checking coverage is also useful for several reasons:

￿ To make sure that the FV model is not overconstrained, i.e., that the assumptions
are not too strong and allow meaningful model behavior.
￿ To assist dynamic validation. If a coverage point is proven to be unreachable in
FV, there is no point in trying to construct test cases for it. The benefit of checking
coverage points in FV may be very significant.
￿ To evaluate new FV algorithms and tools. It is difficult to evaluate a new algorithm
by trying to discover assertion violations in a real mature design. Hitting tough
coverage points is more meaningful because the intended design behavior is
known.

20.1 Counterexample and Witness

If an assertion fails in FV, the FV tool reports a counterexample , often abbre-
viated as CEX, a sequence of input stimuli leading to the assertion failure. For
convenience, the tool usually also shows the values of relevant internal signals.
Suppose that a right shift operator >> were specified instead of the left shift
operator << on Line 8 of Fig. 1.7 . The FV tool could produce the counterexample
shown in Table 20.1 . Indeed, we can see that at clock cycle 3 our assertion fails:
shift_reg is 8'b00000000 , while $past({shift_reg[6:0],shift_reg[7]})
is 8'b00000010 .
Note that some values in the counterexample are not important. For example,
the value of val is important only at clock cycle 1, at other clock cycles it may
assume any value without affecting the result. The FV tool may explicitly report a
don't care ( X ) value in this case.
Cover statements may also be checked in FV: if a coverage point can be hit,
the FV tools report a witness . A witness is a sequence of input stimuli leading to
the coverage point hit, while satisfying all the specified assumptions. Otherwise,
if the coverage point cannot be hit FV tools report that this coverage point is

Table 20.1 Counterexample for check_shift
Clock cycle set

rst val shift_reg

0

1'b0 1'b1 8'b00000000 8'b00000000

1

1'b1 1'b0 8'b00000001 8'b00000000

2 1'b0 1'b0 8'b00000000 8'b00000001

3 1'b0 1'b0 8'b00000000 8'b00000000