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