Regarding seq.ended

I was going through examples related to sequence method .ended and came across following code ::


  bit  clk ,  a  , b , endbranch ;   

  initial  forever #5 clk  =  !clk  ;    
    
  sequence  branch( a , b ) ;   
    @( posedge clk )   $rose( a )  ##[1:5]  $rose( b )  ##0 ( 1 , $display("TIME: %2t  Sequence  branch Completes " , $time ) ) ; 
  endsequence 
 
  property  endCycle ;    
    @( posedge clk )  branch( a , b ).ended  |=>  $rose( endbranch ) ;     
  endproperty 

  ap_test: assert property( endCycle )  $display("TIME: %2t  Assertion  PASS " , $time );  
  
                                  else  $display("TIME: %2t  Assertion  FAILS " , $time );

  initial begin 
    
    `ifdef  M1  

       #4 ; a  =  1 ;

      #30 ; b  =  1 ;

      #10 ; endbranch = 1 ;

    `elsif  M2

       #4 ; a  =  1 ;

      #20 ; endbranch = 1 ;

      #20 ; b  =  1 ;

      #10 ;

    `endif
     
      #2 ; $finish();

    end


For the 2nd case ( +define+M2 ) the assertion fails at TIME : 55 since the Consequent is false .
Consequent is evaluated only at TIME : 55 .

Is it possible to modify the above code such that for +define+M2 the assertion fails when $rose( endbranch ) is True when ’ branch ’ is still executing ?

i.e I want the assertion to fail at TIME: 25 for +define+M2

In reply to Have_A_Doubt:

Note that the .ended method has been deprecated since 1800-2009 and is unnecessary here.

An implication property vacuously passes every cycle the antecedent fails. That means you cannot fail the assertion until b rises.

In reply to dave_59:

Hi Dave ,

Have updated the code using .triggered . The following code works as intended


sequence  branch( b ) ;          
    @( posedge clk )  ##[1:5]  $rose( b )  ##0 ( 1 , $display("TIME: %2t  Sequence  branch Completes " , $time ) ) ; 
  endsequence 
 

  property  endCycle ;
    @( posedge clk )  $rose( a )  |->  not(  !branch( b ).triggered   until  $rose( endbranch ) )  ;        
  endproperty 


Any suggestions on a cleaner way to write the above code ?

In reply to Have_A_Doubt:

You need to express what your new requirements are for the assertion. There is no way to get a failure at time 25 for the original set of requirements.

In reply to dave_59:

Have the following requirements::

  1. $rose( endbranch ) must be true at the Next clock after sequence branch completes
  2. If $rose( endbranch ) is True while sequence is still executing , the assertion should fail at the nearest clock