Hardware Reference
In-Depth Information
To overcome the limitation, the assertion can be rewritten in the following way:
a2:
assert property
(@$global_clock $changing_gclk(sig) -> !en);
This example shows that the global clock may be used as a “carrier” for other
signals that cannot be used as a clock directly.
t
Clock Fairness.
Example 7.33.
Clock is always ticking.
Solution:
It is required to check the clock fairness, i.e., that in any given moment
there is some future moment when the clock ticks (see also Example
5.15
):
a_fclk:
assert property
(@($global_clock)
s_eventually
$rising_gclk(clk));
Discussion:
The assertion clock is
$global_clock
relative to which the ticking of
clk
is checked. This assertion works only if
$global_clock
ticks on both edges
of
clk
or faster. If
$global_clock
is the same as
posedge
clk
, ticking of the
clk
cannot be detected: when
posedge
clk
happens the sampled value of
clk
is
always 0.
Efficiency Tip.
Assertion
a_fclk
is efficient in FV.
6
In simulation, this assertion
is not optimal, as it may accumulate several overlapping attempts, as explained in
Sect.
19.3
.
However, checking this assertion in simulation is not useful. The simulation
run is finite, and thus by analyzing the run it is not possible to conclude that the
clock is always ticking. It is only possible to check that the clock ticks at least
some predefined number of times during the simulation run (see Exercise
7.8
). For
practical needs, it may be sufficient to examine the simulation trace.
t
One could wonder why general sampled value functions contain only the past
version. Why is there no
$future(e, @clk)
function in the language? The answer
is simple: we do not know whether an arbitrary clock is fair, i.e., never stops ticking.
If
clk
stops ticking at some moment, the value
$future(e, @clk)
is undefined. As
for the global clock—the primary system clock—is concerned, it is required to be
fair by definition, and
$future_gclk(e)
always makes sense. This consideration
is important in FV, where infinite traces are handled. See Sect.
21.2.3.1
for an
additional explanation.
7
6
This assertion is still rather expensive to check in FV. What we mean that among various versions
of the same assertion, this assertion is one of the most efficient.
7
In simulation, the assertion behavior is usually ignored at the last tick of the global clock.
Search WWH ::
Custom Search