Hardware Reference
In-Depth Information
Solution:
We have already considered this assertion in Example
7.25
,butthe
implementation there had two drawbacks: we had to delay the assertion by one
clock tick to handle the past value correctly at clock tick 0, and we could specify
stability only relative to a clocking event. Controlling the assertion by the global
clock and using a future value function overcomes these drawbacks:
a_stable:
assert property
(@$global_clock $steady_gclk(sig));
In this implementation, there is no need to have an initial delay since function
$steady_gclk(sig)
checks that the
sig
value is identical to the one in the next
clock tick, hence there is no reference to the values of
sig
prior to clock tick 0, as
in the case with
$stable
.
As
$global_clock
indicates the primary system clock, all signal changes that
we are willing to consider are synchronized with it as explained in Sect.
4.4.2
and
Chap.
21
, and if there is a signal change between the ticks of the global clock, it is
considered to be a glitch and is ignored at the RTL level. Recall, however, that it is
the user responsibility to define
global clocking
.
t
Example 7.31.
Signal
sig
should be stable between two consecutive clock ticks. In
other words, the signal value can change only when the clock is rising.
Solution:
a1:
assert property
(@$global_clock
disable iff
(rst)
$changing_gclk(sig) |-> $rising_gclk(clk));
Discussion:
In this assertion, we consider the clock to be a regular signal, and not
an event. The same assertion may be expressed using past sampled value function,
but this is less natural and usually less efficient in FV:
a2:
assert property
(@$global_clock
disable iff
(rst)
##1 $changed(sig) |-> $rose(clk));
Equivalently, we could use past global clocking function (
$changed_gclk(sig)
,
etc.), but this is more verbose.
t
Clock as a Sampled Signal.
Example 7.32.
Enable
en
should be low when
sig
is going to change.
Solution:
The easiest way to write this assertion is to use
sig
as a clock:
a1:
assert property
(@sig !en);
Discussion:
This solution works always in FV, but it does not always work in
simulation. The reason is that in simulation it is required that the clock value changes
at most once in any simulation tick, otherwise the simulation of the assertion may
not work correctly.
Search WWH ::
Custom Search