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

1 module reqgen( input logic busy, clk, rst, output logic req);
2

wire idle;

assign idle = !busy;

3

4
5 always @( posedge clk or posedge rst) begin
6 if (rst) req <= 1'b0;
7 else if (busy) req <= 1'b0;
8 else req <= 1'b1;
9 end
10 req_when_idle: assert property (
11 @( posedge clk) disable iff (rst) idle |=> req);
12 endmodule : reqgen

Fig. 20.1 Request generator

example illustrates a very important problem encountered in FV: on the one hand it
is desired to reduce the model to fit the capacity of FV tools, and on the other hand,
it cannot be done by a naïve, mechanical deletion. The boundary around the missing
model part must be carefully characterized by adding relevant assumptions. In our
case, the following assumption needs to be added to define the behavior of idle :
idle_when_not_busy: assume final (idle == !busy);
Of course, in this toy example we just replaced an assignment by an assumption,
and the abstract version can hardly be more efficient than the original one.
In realistic cases, however, model abstraction may bring significant performance
improvement because the benefit of the model reduction outweighs the cost of the
boundary assumptions.

20.3.2 Underapproximation

Underapproximation is very commonly used, although most people do not realize
when they are using it. The most common example is simulation: we check the
model behavior only on a given simulation trace, while other possible traces
remain unchecked. Simulation is safe: if the assertion fails in simulation, the model
is definitely wrong (presuming, of course, that the assertion is written correctly
and no assumption is violated). There may be false positives, however: if the
assertion passes in simulation, it does not mean that the design is correct. Therefore,
simulation is not sound.
Another common example of underapproximation is bounded verification: if the
assertion fails within the verification bound, a bug is discovered and can be analyzed
using the generated counterexample. If the bug cannot be stimulated within the
bound, no assertion violation is reported and we cannot conclude anything about
the validity of the assertion.