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