In reply to ben@SystemVerilog.us:
Hi Ben ,
My apologies , I should have specified that current_st is clocked to posedge of clk .
Since the current_st may have the same state across multiple clocks , I used current_st as clocking event for better simulation performance .
I tried changing property and added an always block for debugging :
property illegal_transitn ;
@( current_st ) ( current_st == State2 ) |=> ( current_st == State4 ) ##0 ( 1 , $display(" TIME:%2t ( current_st == State4 ) " , $time ) )
##1 ( current_st == State6 ) ##0 ( 1 , $display(" TIME:%2t ( current_st == State6 ) " , $time ) ) ##0 0 ;
endproperty
always @( current_st ) begin
$display(" TIME:%2t current_st Changes to %0s " , $time , current_st.name() ) ;
end
For +define+M1 : The always block is triggered thrice as per expectations whereas the display for ( current_st == State4 ) is observed at T:84 instead of T:54
My understanding was for property :
property illegal_transitn ;
@( current_st ) $rose( current_st == State2 ) |=> ( current_st == State4 ) ##1 ( current_st == State6 ) ##0 0 ;
endproperty
For +define+M1 :
Antecedent is True at T:14 , then consequent is evaluated whenever current_st changes next .
So 1st part of consequent expression ( current_st == State4 ) should be True at T:54 ,
then the last part ( current_st == State6 ) should be True at T:84 .
However the assertion doesn’t seem to work this way , any suggestions why ?