Request - Acknowledge related Assertion

SystemVerilog
,
1

In my quest to trying out a scenario via different ways I have coded this ::


  property ack_req ;
   
   (  ( ack[=1] )  or  ( $rose( req ) [ = 1 ] )  )  |-> 
    
      if( ack )    //  ' ack '  Written  First   for  cases  where  Both  are  True  !!
    
        ( 1'b1 )   //  No  Semicolon  !!  

     else   
    
        ( 1'b0 )  ;
 
  endproperty 

  property  REQ_ACK ;

    @( posedge clk )  $rose( req )  |=>  ack_req ;

  endproperty

This works fine when ’ ack ’ isn’t received before the Next ’ request ’ .

However for a scenario where ’ ack ’ is received before OR same time as next ’ request ’ I observe No output i.e Incomplete assertion .

Any suggestions ??

2

In reply to hisingh:

ack[=1] is same as
!ack[*0:] ##1 ack ##1 !ack[*0:]
With that in the antecedent, all threads must be evaluated.

Solution: use the goto operator
ack[->1]. Equivalent to
!ack[*0:$] ##1 ack

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Hi Ben ,

Using goto ( → 1 ) instead of Non-Consecutive ( = 1 ) for both ack N $rose( req ) gives the desired results .

However I am still confused between the working of the two .


 @( posedge clk )  a  |=> b[ =2] ##1 c ;  //  (EQ1)

 @( posedge clk )  a  |=> b[ ->2] ##1 c ; //  (EQ2)

My understanding is that for (EQ2) , ’ c ’ should be high exactly 1 clock after
’ b ’ is sampled true twice consecutively / non - consecutively

For (EQ1) ’ c ’ could be high anytime 1 clock after ’ b ’ is sampled true twice consecutively / non - consecutively

So essentially the qualifying event( ##1 c ) differentiates the two .

If I write property as ::


    property  req_ack ;
 
  `ifdef GO_TO

    @( posedge clk )  $rose( req )  |=>  ack [ ->1 ] ; 
 
 `else

    @( posedge clk )  $rose( req )  |=>  ack [ = 1 ] ; 

 `endif

  endproperty

  initial  forever  #10 clk = ! clk ;

  c_property : cover   property ( req_ack )  $display(" TIME : %0t  PASS " , $time ) ;

  initial  begin

    // [1]  ' req '  is  True  on  1st  posedge  N  then  ' req ' is  de - asserted  just  before  Next  posedge .
    //
    //      ' ack '  is  asserted  at  TIME : 49  !!

       #9 ;  req = 1 ;    //  TIME:9

      #20 ;  req = 0 ;    //  TIME:29

      #20 ;  ack = 1 ;    //  TIME:49

      #5 ; 
      $finish(); 
 end

In both cases ( with or without +define+GO_TO ) the assertion passes at TIME : 50 .
My understanding is that since there is no qualifying event after ’ ack ’ they give same results .

Since there is no qualifying event in the original question I posted how do they result in different output ? .

!ack[*0:$] being an empty sequence , which says ‘!ack’ needs to be true on 0 clock tick . Doesn’t it mean that ’ ack ’ need not be false on any clock tick ?


LRM  says  ::

Goto repetition :: "The overall repetition sequence matches at the last iterative match of the operand."

Nonconsecutive repetition  ::  "The overall repetition sequence matches at or after the last iterative match of the operand, but before any later match of the operand"

This too however is confusing to me especially “at or after the last iterative match of the operand, but before any later match of the operand”

4

In reply to hisingh:

…So essentially the qualifying event( ##1 c ) differentiates the two

NO, the difference is the equivalency of the two operators

b[->1] is equivalent to:
!b[*0:$] ##1 b
b[->2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
------------
b[=1] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
b[=2] is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
But !b[*0:$] is equivalent to !b[*0] or !b[*1] or ... 
                Equivalent to empty or !b[*1] or whatever..
If that "whatever" is true or false, it does not affect the results. 
If false, it does not make the consequent false. 
Since there are no other terms after your ack [ = 1 ] 
 (i.e., you do not have ack [ = 1 ] ##1 c)  
----------------
b[=m] is equivalent to ( b [->m] ##1 !b [*0:$] )

Thus, because of that empty  (the !b[*0]term and the other terms being irrelevant. 
remember if sequence==match or true or false // is same as 
            sequence== match // match is like a true
     T or F is T; T or T is T
rose( req )  |=>  ack [ = 1 ];  // is same as 
rose( req )  |=>  !ack[*0:$]  ##1 ack  ##1 empty  // also same as 

rose( req )  |=>  ack[->1];

once ack is true, the consequent matches and that’s it. The trailing !ack sequence is immaterial.

5

In reply to ben@SystemVerilog.us:

Ben as you pointed that the difference between the two is visible when it’s used as antecedent .

Hence I tried the following ::


  property  req_ack ;

  `ifdef GO_TO

    @( posedge clk )  $rose( req ) [ ->1 ]  |=>  $rose( ack ) ;  // [E1]

 `else

    @( posedge clk )  $rose( req ) [ = 1 ]  |=>  $rose( ack ) ;  //  [E2]

 `endif

  endproperty
  
  c_property : cover   property ( req_ack )  $display(" TIME : %0t  PASS " , $time ) ;

  a_property : assert  property ( req_ack )  else  $display(" TIME : %0t  FAIL " , $time ) ;

   initial  forever  #10 clk = ! clk ;

   initial  begin

// [1]  ' req '  is  True  on  2nd  posedge  N  then  ' req ' is  de - asserted  just  before  Next  posedge .
//      ' ack '  is  asserted  at  TIME : 49  !!

           #20;            //  TIME:20

       #9 ;  req = 1 ;    //  TIME:29

      #20 ;  ack = 1 ;    //  TIME:49

      #20 ;  req = 0 ;    //  TIME:69

       #5 ;
    $finish() ;

  end

The O/P for +define+GO_TO ::


  TIME : 50  PASS 
  TIME : 50  PASS    //   [ Q1 ]   Why  the  2nd  Pass  at  TIME : 50  ??

The O/P for No +define i.e Via Non - Consequent Repetition ::


  TIME : 70  FAIL 
  TIME : 70  FAIL    //   [ Q2 ]   Why  the  Two  Failures  ??

I am trying to understand when would the antecedent True in both Cases .

So as you suggested the antecedent is equivalent to ::


 //   For   +define+GO_TO  ::
 
$rose( req ) [ ->1 ]  is  equivalent  to  ::  ( ! $rose( req )[*0:$] )  ##1 $rose( req )
    
i.e  ( ! $rose( req )[*0]  or   ! $rose( req ) [*1]   or   ! $rose( req ) [*2]  or .... )  ##1 $rose( req )

Due to assertion being Multi - threaded ::

(1) First Thread starts on 1st posedge of Clock at TIME : 10

At 1st posedge at TIME : 10 , $rose( req ) is False . Hence ! $rose( req ) [ *1 ] is True !!

At  2nd  posedge  at  TIME : 30  ,  $rose( req )  is  True   .

Hence  antecedent  is  True  at  TIME : 30  !!

At  3rd  posedge  at  TIME : 50  ,  as  $rose( ack )  is  True  it's  a  Match  and

for  Thread 1  the  assertion  Passes  at  TIME : 50  !!

(2) Second Thread starts on 2nd posedge of Clock at TIME : 30

For  the  1st  posedge  for  Thread  2  at  TIME : 30  (  2nd  posedge  for  the  Simulation  )  ::

     ( ! $rose( req )[*0]  )  is  True  at  TIME : 30  

**[ Q3 ]  So  how  is  the  antecedent  True  at  TIME : 30  for  Thread 2  ?  As ##1 $rose( req ) is  still not  True**


 //   For   No  +define  i.e  Via  Non - Consequent  Repetition  ::
 
   Antecedent  ' $rose( req ) [ = 1 ] '  is  equivalent  to  ::  

  ( ! $rose( req )[*0:$] )  ##1 $rose( req )  ##1 ( ! $rose( req )[*0:$] ) 

 i.e  ( ! $rose( req )[*0]  or   ! $rose( req ) [*1]   or  ... )  ##1 $rose( req )  ##1 ( ! $rose( req )[*0]  or   ! $rose( req ) [*1]   or  ... )

 i.e  (    Empty      or   ! $rose( req ) [*1]   or  ... )  ##1 $rose( req )  ##1 ( ! $rose( req )[*0]  or   ! $rose( req ) [*1]   or  ... )

At 1st posedge at TIME : 10 , $rose( req ) is False . Hence ( ! $rose( req ) [ *1 ] ) is True !!

At 2nd posedge at TIME : 30 , $rose( req ) is True .

At 3rd posedge at TIME : 50 , $rose( req ) is False .

Hence ( ! $rose( req ) [ *1 ] ) is True !!

As a result I believe Antecedent is True at TIME : 50 ( Please correct me if wrong )

At TIME : 70 , $rose( ack ) is False hence the Failure ( Please correct me if wrong )

[ Q4 ] But why does Thread2 FAIL at TIME : 70 ? When would the antecedent be True for Thread 2 ??

6

In reply to hisingh:
Comments:

  1. NO on expr[->1] |-> consequent or NO on expr[=1]
    $rose( req ) [ ->1 ] |=> $rose( ack ) ; // BAD STYLE, LOAD on simulator
    The first term should not be a goto or a Non-consecutive repetition operation because at every clocking event you start a new thread; it’s a load on the simulator.
    I strongly suggest that you read my paper Understanding the SVA Engine,
    Verification Horizons - July 2020 | Verification Academy
  2. Threads and attempts
    Your questions on threads and attempts are replied in my book and are supplemented in the above paper. I am providing to you the following sections of my book that addresses these topics:
    http://systemverilog.us/vf/Cohen_SVA_Threads.pdf
    http://systemverilog.us/vf/Content.png
    After you read those documents and expand the [->1] and [=1] operators to their equivalencies then your questions will be answered.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

7

In reply to ben@SystemVerilog.us:

Thanks for the reference . Will look into them .

Have a final question related to the original question I posted


property ack_req ;
 
   (  ( ack[->1] )  or  ( $rose( req ) [ -> 1 ] )  )  |-> 
 
   if( ack )   
 
   ( 1 , $display(" TIME : %0t  ACK  True  " , $time ) )   //  Added  for  Debugging  !!  
 
   else   
 
   ( 1'b0 )  ;
 
  endproperty 
 
  property  req_ack ;
 
    @( posedge clk )  $rose( req )  |=>  ack_req ;
 
  endproperty

  c_property : cover   property ( req_ack )  $display(" TIME : %0t  REQ_ACK  PASS " , $time ) ;

  initial  forever  #10 clk = ! clk ;

  initial  begin
 
// ' req '  is  True  on  1st  posedge  N  then  ' req ' is  de - asserted  just  before  Next  posedge .
//  ' req '  is  Asserted  at  TIME : 69  .  ' ack '  is  asserted  at  TIME : 49  !!
 
 
       #9 ;  req = 1 ;    //  TIME:9
 
      #20 ;  req = 0 ;    //  TIME:29
 
      #20 ;  ack = 1 ;    //  TIME:49

      #20 ;  req = 1 ;    //  TIME:69
 
       #5 ;
    $finish() ;
 
  end

I Observe O/P as ::

TIME : 50 ACK True
TIME : 50 ACK True
TIME : 70 ACK True
TIME : 70 ACK True
TIME : 70 REQ_ACK PASS

[ Q ] Why does the assertion Pass at TIME : 70 instead of TIME : 50 ?

Antecedent ( ack[->1] ) is true at TIME : 50 hence I expect assertion to Pass at TIME : 50

8

In reply to hisingh:
You consequent ack_req for the property ($rose( req ) |=> ack_req ;) IS a property.
That property (ack_req) has two threads in its antecedent, and both threads must be tested for the assertion/cover to pass. See my annotation in the image below.
COMMNETS:

  1. STYLE: Definitely not recommended.
  2. GOTO not as first element in an antecedent
  3. Use of if else is trying to make a single assertion with multiple small pieces within it. You should write multiple small assertions instead
  4. You naming nation implies that the ack_req is a sequence and not a property.
  5. I generally avoid the use of a separate property unless needed.

1508×855 161 KB

1508×855 161 KB

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/