Hardware Reference
In-Depth Information
Table 20.2 Witness for cov_shift
Clock cycle set
rst
val
shift_reg
0
1'b0 1'b1 8'b00000000 8'b00000000
1
1'b1 1'b0 8'b10000000 8'b00000000
2
1'b0 1'b0 8'b00000000 8'b10000000
3
1'b0 1'b0 8'b00000000 8'b00000001
unreachable under the specified assumptions. It may also be impossible to hit the
coverage point if the FV tool runs out of memory or allocated run time.
Consider the following cover statement for the shift register in Fig. 1.7 :
cov_shift: cover property (@( posedge clk) disable iff (rst)
shift_reg == 8'b10000000 && !set
##1 shift_reg == 8'b000000001);
The cover statement states that we wish to cover two consecutive clock cycles such
that in the first cycle shift_reg has the value 8'b10000000 and set is inactive, and
in the second cycle shift_reg has the value 8'b000000001 . A possible witness is
shown in Table 20.2 .
As with assertion counterexamples, coverage point witnesses may contain don't
care values. In our example, all values of val are actually don't cares except for the
one in clock cycle 1.
20.2
Complete and Incomplete Methods
So far we discussed complete FV methods: these methods report for each assertion
whether it passes or fails. Of course, this is the best thing to have, but because of
capacity limitations, incomplete FV methods are often used. These methods have
three possible outcomes: passed , failed ,or unknown . Strictly speaking, even the
methods we called complete can also report an unknown status for assertions when
they time out or exceed memory limitations. The difference is that the complete
methods are intended to find the exact solution, while the incomplete methods may
give up even when computing resources are still available. Usually incomplete FV
methods are much faster than complete ones.
Typically, incomplete methods are bounded FV methods: given a verification
bound n they check that there is no assertion violation with a counterexample shorter
than n cycles starting from an initial state. The initial state need not be the reset state.
These methods do not guarantee that an assertion is correct, but only that it cannot
be violated “too soon”. Bounded FV methods are widely used, and they can provide
good confidence in design correctness. For example, if the design is pipelined, then
the bound n equal to or a little bigger than the depth of the pipeline is usually
sufficient.
 
Search WWH ::




Custom Search