Hardware Reference
In-Depth Information
An evaluation attempt has a start time and an end time. The end time may
also be infinite, but in simulation bounded by the extent of the simulation.
Evaluation of more than one attempt may be in flight at the same time.
If an assertion is always enabled, then there will be a series of evalua-
tion attempts, starting at every tick of the leading clock. This is the case when
the assertion is placed outside any procedure. However, if it is placed in an always
procedure, then the start of an attempt is also controlled by the execution of the
body of the always procedure reaching the position of the assertion. Furthermore,
if an assertion is placed in an initial procedure, there will be only one evaluation
attempt starting at the first tick of the leading clock.
We can thus see that a concurrent assertion outside a procedure will execute
“always”, inside an initial procedure it will execute once, and inside an always
procedure it may execute more than “once”. This is to some extent different
from the more classical interpretation of assertions that are not part of a design
language (e.g., in PSL). There, unless an explicit top-level always operator is
specified in the assertion, the evaluation only starts at the first clock tick. For users
who have been using PSL and plan to use SystemVerilog assertions, care must
be taken not to include this top-level always operator, because it could lead to
some performance penalty in simulation, although the behavior remains correct as
illustrated in Example 4.5 .
Example 4.5.
Operator always as a top-level property in an assertion.
module m;
bit clk,a,b;
default clocking ccc @( posedge clk); endclocking
a_always: assert property ( always (a ##1 b));
//...
endmodule
Assertion a_always does not make practical sense for the following reason: it
will start an evaluation attempt at every tick of it clock. The top-level operator is
always , and thus in each such attempt it will redundantly fork off a new version
of the always operator to perpetually check for every pair of consecutive values of
a and b . Unless the simulator can detect this situation and do something about it,
there may be an ever increasing number of evaluation attempts that never terminate,
causing a heavier and heavier burden on the simulator. See also Sect. 6.3.2 .
t
Example 4.6. The following two assertions provide an interesting illustration of the
meaning of an evaluation attempt.
module m;
bit clk,a,b;
a1: assert property (@( posedge clk) a |=> b);
initial
a2: assert property (@( posedge clk) always (a |=> b));
endmodule
Search WWH ::




Custom Search