Hardware Reference
In-Depth Information
sequence method signals that the end of a sequence has been reached, and it is
described in Sect.
11.2.1
).
sequence
ack; @(
posedge
clk)enable ##[1:10] end_ack;
endsequence
a1:
assert property
(@(
posedge
clk)
req |-> busy
until
ack.triggered)
else
$error("Assertion a1 fails");
We can subdivide the activity as follows:
1. Sample signals
enable
,
req
,
end_ack
, and
busy
which are needed for concur-
rent assertion evaluations.
2. Detect the occurrence of clock
@(
posedge
clk)
, since sequence
ack
and
assertion
a1
evaluations are activated by the clock.
3. Start a new attempt for sequence
ack
.
4. Determine whether there is a match for sequence
ack
.
5. Start a new attempt for assertion
a1
.
6. Resume evaluation of the previous attempts for this clock tick.
7. For an attempt of
a1
resulting in a failure, schedule the action block execution in
the Reactive region.
8. For an attempt of
a1
resulting in a success, report a success.
9. Execute action blocks.
These steps are taken in specific regions. Each region contributes to the execution
of concurrent assertions as shown in Fig.
4.12
.
Normally, the detection of an assertion clock occurs in the Active region. What
sets a concurrent assertion apart from an immediate assertion is that the former is
triggered by its clock. Consequently, its evaluation resumes at the arrival of the clock
and gets suspended at the end of the time slot in which the clock occurs.
Let us now consider assertions embedded in an always procedure. Beside the
clock, the new attempts of procedural concurrent assertions are bound to the
procedural context in which they are specified. For instance,
function bit
f1(
bit
arg);
//...
endfunction
always
@(
posedge
e1)
begin
:B1
a<=b+c;
if
(c1_enb)
a2:
assert property
(f1 (a) ##2 f1(a));
dout <= f1(a);
end
An evaluation attempt of assertion
a2
can only be initiated if the simulation
control reaches the statement. In this case, it means that,
Search WWH ::
Custom Search