Assertion to check ' ack ' is received after ' req ' is asserted

SystemVerilog
,
1

I have the following assertion :: EDA_LINK

For the 2 cases ( +define+M1 N +define+M2 ) I observe different O/P across Simulators ::

(a) For +define+M1 ::

On  Simulator1  I  Observe  :: **TIME : 49  STRICTLY1ACK  FAIL**

While others give No O/P due to Incomplete assertion ( same as my expectation )

My question is the expression within the ’ not ’ Operator is Never True . So the consequent is Never :: not( 1 )

So how come the assertion FAILS ??

The consequent seems to act as an implicit ’ strong ’ operator

(b) For +define+M2 ::

 On  Simulator1  I  Observe  :: **TIME : 45  STRICTLY1ACK  FAIL**

 While  on  Simulator2  I   Observe  :: 

 **TIME : 45  STRICTLY1ACK  FAIL
 TIME : 45  STRICTLY1ACK  PASS**

My expectation is that the assertion would PASS at TIME:45 since consequent would be :: not( 0 )

2

In reply to hisingh:

(a) When you negate a property, you switch its strength. (16.12.3 Negation property). Since the consequent is now strong, an incomplete property fails. To get the behavior you expected, write it as

@( posedge clk )   $rose( req ) |=>  not strong (!ack[*1:$]   ##1  $rose( req )  ) ;

(b) There are two assertion attempts, one starting at time 5, and the other starting at time 45. There is no strength involved in the first attempt, all tools agree it should fail. But since the second attempt begins on the last clock cycle and you are using non overlapping implication, the consequent never begins evaluations, so it is incomplete.
We normally recommend only using the overlapping implication to avoid confusion and writ the property as

    @( posedge clk )   $rose( req ) |->  not  strong((##1 !ack[*1:$]   ##1  $rose( req )  ) ;

If you add a pass message to the assert statement

a_property : assert property ( strictly1ack ) $info(“pass”,$time); else $error(" TIME : %2t STRICTLY1ACK FAIL " , $time , ) ;

You see that the tool that printed the passing message for the cover directive does not print a passing message for the assert directive. That is a contradiction and incorrect behavior.

3

In reply to hisingh:

@( posedge clk ) rose( req ) |=> not( !ack[*1:] ##1 $rose( req ) ) ;
does NOT check ’ ack ’ is received after ’ req ’ is asserted
Your assertion says: If(rose(req) then no new ack until a new req.

The following link addresses the topic
“A grant must at some time have been preceded by a request”
https://verificationacademy.com/forums/systemverilog/grant-must-some-time-have-been-preceded-request#reply-104623

Generally, I tend to avoid the “not” operator unless I have to. It can be hard to understand if the property is complex, like having an implication operator.

BTW, check out my paper at DvCon’s Verification-Horizons issue:
“Reflections on Users’ Experiences with SVA” by Ben Cohen, SystemVerilog Assertions Expert
https://verificationacademy.com/verification-horizons/march-2022-volume-18-issue-1

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/

4

In reply to dave_59:

Dave ,
Thanks for the clear explanation .


LRM  16.12.3 Negation property ::  " The not operator switches the strength of a property "

On updating the stimulus for an addition clock tick for +define+M2 gives Failure for the same reason as +define+M1 .

Although I understand that we don’t discuss tool issues , personally I find it quite amusing that one of the Top Tools falls so short when it comes to assertions ( Even the licensed ones ) .
Apart from this ( not ) peculiar case I have observed that ’ strong ’ , ’ reject_on ’ , ’ s_until_with ’ isn’t supported .

5

In reply to ben@SystemVerilog.us:

Ben ,

A few points

(1) " does NOT check ’ ack ’ is received after ’ req ’ is asserted "

  However  if  ' ack '  is  received  before  next  ' req ' the  assertion  passes 

   Have  updated  the  [EDA_LINK](https://www.edaplayground.com/x/8Scu)  with  3rd  case  for  +define+M3

(2) " If( rose(req) then no new ack until a new req. "

However the assertion would Fails in such case which isn’t the Ideal case but such cases need to be shown as error