In reply to ben@SystemVerilog.us:
Hi Ben,
Generally b[=m] means that ‘b’ must be true on ‘m’ clocks (not necessarily consecutive)
So b[=0] would mean that ‘b’ must be true on ‘0’ clocks i.e ‘b’ should never be true.
The same can be cross checked via it’s equivalent expression: !b[*0:$] i.e ‘b’ should never be true.
However the assertion passes/fails on the very 1st clock that the consequent is evaluated using
property ab;
@(posedge clk) a |=> !b[0:$];
endproperty
It doesn’t actually check that ‘b’ is false throughout simulation, hence I tried the following:
// Attempt 1
property ab1;
@(posedge clk) a |=> always !b ;
endproperty
Using ‘ab1’ the assertion doesn’t pass even if ‘b’ is false throughout simulation
// Attempt 2
property ab2;
@(posedge clk) a |=> always strong(!b);
endproperty
Similar to ‘ab1’, the assertion doesn’t pass even if ‘b’ is false throughout simulation for ‘ab2’
// Attempt 3
property ab3;
@(posedge clk) a |=> s_always[1:10]!b; // s_always can't be unbounded
endproperty
Have a few questions related to attempt 3
[Q1] The simulation time could vary based on the test that is being run, so how do I generalize the range in s_always ?
[Q2] What does the 1 and 10 signify ?
If I were to write s_always[3:10] !b , if the antecedent is true at T0, then the consequent is evaluated from T1. What does range [3:10] indicate ?
[Q3] Is there any alternative to s_always to check that ‘b’ is false throughout simulation ?
I was thinking of something along the lines of :
bit simulatn_ends;
property ab4;
@(posedge clk) a |=> strong( !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