Hi all,
I am trying to write a SVA for following requirement : Once ‘a’ is asserted , signal ‘b’ shouldn’t be asserted till end of simulation.
bit clk , simulatn_ends, a , b;
always #5 clk = !clk;
property atob;
@(posedge clk) $rose(a) |=> ( !b throughout $rose(simulatn_ends)[->1] );
endproperty
final begin // Executes after $finish() is called in UVM Tb via uvm_top::run_test()
simulatn_ends = 1;
end
initial begin
#4; a = 1;
#101; $finish(); // assume that $finish() is always called on posedge of clk i.e time: 5n units ( where n>0 )
end
I observe that the pass action block isn’t triggered and I was trying to understand the reason behind it.
I am aware that $finish() executes in active region. SVA property/sequence is evaluated in Observed region and the action block execute in Reactive region [Q1] Once $finish() executes in active region at time:105 will the simulation even reach other SV regions within the same time step for the property to be evaluated ( in Observed region )and action block to be triggered ( in reactive region ) ?
[Q2] Is there any alternative to trigger the action block at end of simulation ?
1800, pg 461 rule3 is a property declared in module top. The assert statement a1 starts checking the property from the beginning to the end of simulation."
1800, [g 493 A final procedure may be specified within a checker in the same manner as in a module (see 9.2.3 ). This allows for the checker to check conditions with immediate assertions or print out statistics at the end of simulation. The operation of the final procedure is independent of the instantiation context of the checker that contains it. It will be executed once at the end of simulation for every instantiation of that checker. There is no implied ordering in the execution of multiple final procedures. A final procedure within a checker may include any construct allowed in a non-checker final procedure.
After the $finish, there are no other clocks.
// instead of
$rose(a) |=> ( !b throughout $rose(simulatn_ends)[->1] );
// what about
$rose(a) |=> s_always[1:2^31] !b );
// you can also do the following instead of the s_always
final assert(!b); // b==0 at end of sim
At time:105 units there occurs a posedge of clk as well as $finish() executes ( possibly a race condition between them as well )
Both the assign statement as well as $finish() executes in active region, however a time step consists of other regions as well.
[Q1] Once $finish() executes at time:105 , will the NBA , observed and reactive region execute at time:105 ?
Since I don’t observe a pass report I have a feeling that observed ( for property evaluation ) and reactive region ( for action block ) don’t execute
// what about
$rose(a) |=> s_always[1:2^31] !b );
The limitation with this approach is the assertion passes only when there are 231 clocks in simulation. Depending on the test being run, the simulation time can vary. As a result there is no guarantee that 231 clock are present in each test.
// you can also do the following instead of the s_always
final assert(!b); // b==0 at end of sim
Yes this can be added to the concurrent assertion ‘atob’ above. Property ‘atob’ checks that ‘b’ is low till end of simulation while the immediate assertion would trigger a pass action block once $finish() executes.
In 1800 / 9.2.3 Final procedures, there are 2 statements that should be read in that order :
1- “A final procedure executes when simulation ends due to an explicit or implicit call to $finish” and that means $finish then final procedure will be executed.
2- “No remaining scheduled events shall execute after all final procedures have executed” and that means if there is an event that is scheduled to be executed after executing the final procedure that won’t happen. i.e. in your case even though simulatn_ends = 1 happens in the active region, the scheduled event of property evaluation that should happen in the observed region won’t have a chance to be executed.
As a suggested solution to your problem, you could try the following
module test;
bit clk, a, b, b_asserted;
always #1 clk = !clk;
function automatic set_b_asserted();
b_asserted = 1;
endfunction
property atob;
@(posedge clk) $rose(a) |-> b[->1] ##0 (1, set_b_asserted());
endproperty
asrt_atob: assert property(atob);
final assert (!b_asserted);
endmodule