Hardware Reference
In-Depth Information
assumption m1 would pass and assumption m2 would be violated. If in clock tick
1, v gets the value of 1 and w gets the value of 2 , then both assumptions will be
violated.
t
Example 23.25.
In the following checker
checker check(..., event clk);
rand bit v;
...
m1: assume property (@clk v |-> ##3 1'b0);
endchecker : check
the value of free variable v must always be low to satisfy assumption m1 :ifin
some clock tick v is high, assumption m1 will fail in three clock ticks. However,
in simulation there is no obligation to satisfy the assumptions in future clock ticks,
and your simulator can choose the value 1 for v in some clock tick, as it does not
result in violation of the assumption in the same clock tick. Of course, in this case,
assumption m1 will fail in three clock ticks.
t
If there are deferred (or final) assumptions in the assume set, 13 all checker free
variables are randomized at every tick of a clock from a concurrent assumption from
the assume set and, in addition, they may also be randomized in any other simulation
time step. 14
Example 23.26.
In the following checker
checker check(..., event clk);
rand bit v, w;
...
m1: assume final ($onehot0({v,w}));
m2: assume property (@clk v |=> w);
endchecker : check
free variables v and w must be randomized every tick of clk and, in addition, they
may be randomized in any simulation tick.
t
Efficiency Tip. Constraining free variables by assumptions significantly slows
down the simulation and sometimes even leads to bogus assumption violations.
It is always preferable to use unconstrained free variables and their assignments
whenever possible. However, from a methodological point of view assumptions on
the model interface may be desirable for assume-guarantee reasoning.
13 One should avoid using free variables in all forms of assertion statements but concurrent, see
Sect. 23.3.4 .
14 This is our interpretation of the standard. The standard is not explicit about free variable
randomization with deferred assumptions.
Search WWH ::




Custom Search