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