SystemVerilog Simulation Semantics - SVA: The Power of Assertions in SystemVerilog - page 52

SystemVerilog Simulation Semantics
t
As we could see, the normal flow between regions: Preponed ! Active
! Inactive ! NBA ! Observed ! Reactive ! Re-Inactive ! Re-NBA !
Postponed often complicates by iterations between regions. For example, the
computations in the Reactive region may schedule a new event in the Active region.
It is also possible that the assertion evaluation in the Observed region is triggered
by events in the Reactive region. One such scenario is when an assertion clock is
modified in the Reactive region set.
Example 3.8. We will modify the code from Example 3.7 to generate the clock by
the program test , instead of the module top .
1 module procReq( input logic req, gnt, clk);
2 logic allow;
3 wire proceed;
4 assign proceed = allow && gnt;
5 always @( posedge clk) allow <= req;
6 always @( posedge proceed) processData();
7 a1: assert property (@( posedge clk) req |=> proceed || !gnt);
8 endmodule : procReq
9
10 program test( output logic request, grant, sync);
11 logic oldreq = 1'b0;
12 assign grant = oldreq;
13 initial begin
14 request = 1'b0;
15 sync = 1'b0;
16 for ( int i = 0; i < 100; i++) begin
17 #5 sync <= !sync;
18 if (i % 2) begin
19 oldreq <= request;
20 request <= $random;
21 end
22 end
23 end
24 endprogram : test
25
26 module top();
27 logic r, g, c;
28 procReq dut(r, g, c);
29 test tb(r, g, c);
30 endmodule : top
Since the clock is generated in the Re-NBA region (Line 17 ), it schedules the
event in the Observed region which will be executed after the completion of the Re-
NBA region. Thus, the order of the simulation regions at time 5 in this case will be:
Reactive region set ! Active region set ! Observed region. See also Exercise 3.4 .
t