For the following code :=>
module SV_Event ;
int a , b ;
bit clk ;
initial begin
forever #10 clk = ! clk ; // Assignment in Active Region
end
always @( posedge clk ) begin
a <= a + 1 ; // Assignment Occurs in NBA Region
end
always_comb begin
b = a ; // Assignment Occurs in Active Region
$display(" b assigned "); // Occurs in Active Region
end
initial begin
#30 ;
$display("End of Simulation at %0t " , $time );
$finish() ;
end
initial begin
$monitor(" At %0t :: a is %0d , b is %0d " , $time , a , b ) ; // Executes in Postponed Region
end
property Obs ; // Assertion Executes in Observed Region . $display() below would execute in Observed Region !!
@( posedge clk ) ( 1 , $display(" a == %0d and b == %0d " , a , b ) ) |-> 1 ;
endproperty
assert property ( Obs ) ;
endmodule
**I was wondering why the following don’t execute at time 30 ::
- $monitor in postponed region
- $display() in the re-entrant active region
- Assertion evaluation in Observed Region
**
When $finish() executes at time 30 , won’t the other regions after Active region execute ?
In reply to hisingh:
No, when executing $finish, simulation is over. (except for final blocks and strong properties). And you have a race condition between another posedge clock at tome 30, or the $finish at time 30.
In reply to dave_59:
Hi Dave ,
A follow-up question related to strong properties ::
bit a , b , c , clk ;
property abc ;
@( posedge clk ) $rose( a ) |=> strong( b ##1 c ) ;
endproperty
assert property ( abc ) else $display(" TIME : %0t Assertion Fails" , $time ) ;
// Posedge occurs at time 5 , 15 , 25 , 35 , etc ..
initial forever #5 clk = ! clk ;
initial begin
#4 ; a = 1 ;
#10 ; b = 1 ;
#1 ; $finish() ;
// At TIME : 15 , Consequent starts evaluation
end
I observe No O/P ( not sure if this is how the LRM defines it ) .
Could you please help me with the code’s working
( If Simulation ends at TIME : 16 I observe Assertion Failure as expected )
In reply to hisingh:
That is because your property is equivalent to
property abc ;
@( posedge clk ) $rose( a ) ##1 1 |-> strong( b ##1 c ) ;
endproperty
So the strong part of your property would not start until time 25.
We recommend avoiding the use of the non overlapping implication operator |=> and just use the overlapping implication |->.
property abc ;
@( posedge clk ) $rose( a ) |-> strong(##1 b ##1 c ) ;
endproperty
In reply to dave_59:
Hi Dave ,
Wouldn’t the strong part of the property start from time 15 ? i.e 2 Clcok tick in Simulation .
The antecedent has Non-Vacuous Pass at 1st clock tick at time 5 .
So Consequent ( strong Operator ) would start evaluation at the next clock tick at time 15 .
My confusion is when $finish() is called at time 15 at exactly the 2nd clock tick .
Would the consequent be evaluated ( b is True at time 15 ) and will the strong operator come into the picture ?
OR Would Simulation end ( hence NO O/P ) before consequent ( strong operator ) is evaluated ?
If I change the code such that $finish() occurs at time 16 , the assertion Fails as the consequent isn’t complete when the simulation ends .
This is as per expectation due to strong operator
In reply to hisingh:
As in your original example, you have a race condition whether the $finish executes before the 2 clock tick. But either way, the observed region never executes at time 15 to complete the antecedent.
In reply to dave_59:
Thanks Dave ,
As the consequent hasn’t started evaluation the ’ strong ’ operator doesn’t come into picture .
Hence the code is similar to the original example i.e the observed region never executes at time 15
If Simulation Ends at time 16 the strong Operator is active . Hence assertion Fails .
Furthermore if I were to change stimulus to ::
initial begin
#4 ; a = 1 ;
#10 ; b = 1 ;
#10 ;
#1 ; c = 1 ; // TIME : 25
$finish() ; // TIME : 25
end
**The assertion fails as the Consequent won’t be evaluated in Observed Region of TIME : 25 ,
due to $finish() being executed in Active Region of T : 25 ( other regions post active region don’t execute )
As ’ strong ’ Operator is Active the assertion fails ( even though ’ c ’ is True )**