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