Hardware Reference
In-Depth Information
Solution: The behavior of these assertions differs in case sig is high at clock tick 0.
At clock tick 0, the antecedent of a2 is true because the past value of sig prior to the
initial clock tick is 0. Therefore, assertion a2 requires sig to remain true for four
additional clock ticks. Assertion a1 does not have a nonvacuous attempt starting at
clock tick 0, and it skips the comparison with the “prehistoric” value of sig .
Discussion: It is difficult to argue which solution is more natural, but consider the
dual case when we want to check that the signal remains low during 5 cycles:
b1: assert property (@( posedge clk) ##1 $fell(sig) |=> !sig[ * 4]);
b2: assert property (@( posedge clk) $fell(sig) |=> !sig[ * 4]);
The behavior of assertions a1 and b1 is similar, but the behavior of assertions a2
and b2 is different! If at clock tick 0 the value of sig is low, $fell(sig) will return
false, so that assertions b1 and b2 are equivalent. One could argue that if sig were
of type logic , the behavior of assertions a2 and b2 would be consistent, as $fell
returns true in case of transition from x to 0. This is true in simulation, but usually
not in FV, because most FV tools treat all variables as two-valued as mentioned
above.
This example shows again that one should be very careful with the behavior of
sampled value functions in the initial clock tick, and that it is better to introduce
an initial delay. Specifying a reset with assertions a2 and b2 makes their behavior
unpredictable at the moment when the reset goes low, as explained in Example 7.14 .
To
conclude
this
example,
we
mention
that
the
assertion
suggested
in
t
Example 6.29 is more efficient than assertion a1 .
Example 7.22. Assertion triggers in Examples 6.23 , 6.42 , and 6.24 are level-
sensitive events: “When request is high ...”. In many cases, it is desirable to
have edge-sensitive triggers: “When request becomes high ...”. For instance,
Example 6.42 may be reformulated as: “When request becomes high it should
be granted within 5 cycles.” The corresponding assertion is (note the nexttime
operator!):
a1: assert property (@( posedge clk)
nexttime ($rose(req) |-> ##[1:5] gnt));
or
a2: assert property (@( posedge clk)
##1 $rose(req) |-> ##[1:5] gnt);
The same assertion is probably better written as 3 :
a3: assert property (@( posedge clk)
!req ##1 req |-> ##[1:5] gnt);
t
3 Assertions a1 and a2 are equivalent, but assertions a1 and a3 are not completely equivalent: If
at clock tick 0 req has value x, and in clock tick 1—value 1, the consequent at clock tick 1 is
checked in a1 , but not in a3 . If the variable values are 2-valued, both assertions are equivalent.
The situation when assertions behave differently in presence of unknown values is quite common,
we will not always explicitly comment on it.
Search WWH ::




Custom Search