Regarding Sequence method .triggered

Hi All ,

I have the following code :


module  top;

  bit  clk , a , b ,  endBranch ;

  always  #5  clk =  !clk ;   

    sequence  branch( a1 , b1 );  //  Declared  as  ' sequence '  to  use  method  ' .ended '  !!  

      @( posedge  clk )  $fell( a1 )  ##[1:5]  $rose( b1 ) ;  
                                                             
    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 
    
       //  endBranch  Goes  True  before  Sequence  branch  Completes .

      #14 ; a =  1 ;           //  $fell( a )  is  True 

      #40 ; endBranch  =  1 ;  //  endBranch  is  True  although  Sequence  ' branch '  hasn't  Completed  

       #2 ; $finish();

    end

endmodule


Consequent is evaluated only when Antecedent is True i.e sequence ’ branch ’ completes . Hence there is No output ( No Pass / Fail ) for above code

What if I wanted the assertion to check that $rose( endBranch ) isn’t True while sequence ’ branch ’ is still executing .
Eg : For above stimulus I would like assertion to Fail at T:55 since sequence ’ branch ’ isn’t complete .

In reply to Have_A_Doubt:
The ended construct is deprecated. Use the triggered construct
For signal generation, use NBA assignments instead of delays.
Your code had a vacuous property. Most tool have a switch to not display passes (vacuous or nonvacuus).
Test your code in edaplayground


module  top;
  bit  clk , a , b ,  endBranch ;
  always  #5  clk =  !clk ;   
  sequence  branch( a1 , b1 );  //  Declared  as  ' sequence '
    // .ended  is deprecated
    @( posedge  clk )  $rose( a1 )  ##[1:5]  $rose( b1 ) ;  
    endsequence 
 
    property  endCycle ;
      @( posedge clk )  branch(a,b).triggered  |=>  $rose( endBranch ) ; 
    endproperty
 
 
    ap_test: assert property( endCycle )  $display("TIME: %2t  Assertion  PASS " , $time );  
                                    else  $display("TIME: %2t  Assertion  FAILS " , $time );
    initial begin 
       $dumpfile("dump.vcd"); $dumpvars;
       //  endBranch  Goes  True  before  Sequence  branch  Completes .
      @( posedge clk ) a <=  1 ;           //  $fell( a )  is  True 
      repeat(2) @( posedge clk );
      endBranch  <=  0 ; 
      b <=  1;
      //  endBranch  is  True  although  Sequence  ' branch '  hasn't  Completed  
       #200; $finish();
    end
endmodule


TIME: 45  Assertion  FAILS 
# ** Note: $finish    : testbench.sv(24)
#    Time: 225 ns  Iteration: 0  Instance: /top
# End time: 18:07:30 on Mar 21,2023, Elapsed time: 0:00:01
# Errors: 0, Warnings: 0
Findin

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

In reply to ben@SystemVerilog.us:

Is .triggered even needed here?

In reply to ben@SystemVerilog.us:

Hi Ben ,

In your code the assertion fails as the consequent isn’t True at time:45 units. The Consequent is only evaluated once sequence ’ branch ’ completes .

However the requirement is to also check for $rose( endbranch ) while sequence ’ branch ’ is still executing .

So if $rose( endbranch ) is True while sequence ’ branch ’ is in middle of execution the assertion should ideally fail .

In the topmost stimulus I would like assertion to Fail at T:55 since sequence ’ branch ’ isn’t complete and $rose( endbranch ) is sampled True ( at Time:55 units ) while sequence ’ branch ’ is still executing .

In reply to Have_A_Doubt:
if $rose( endbranch ) is True while sequence ’ branch ’ is in middle of execution the assertion should ideally fail.

You did not need the .triggered


  ap_1: assert property( @(posedge  clk)  $rose(a) |->  
                 (!endBranch[*1:$]) intersect (a ##[1:5] b)) else err1=err1+1; 
 
 

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs