Newbie to assertions: Can someone explain this?

SystemVerilog
, ,
1

Hello,

property p1;
    @(posedge clk)  $rose(a) ##1 b[->0] ##1 c |-> 1;
endproperty

At posedge of clk, when a goes HIGH, 1 clk cycle later b goes HIGH (not clear [->0] is doing).
Continuing, 1 clk cycle AFTER b, c goes HIGH (not clear |-> 1 is doing)

Can some please help?

Many thanks.

2

In reply to Verif Engg:

$rose(a) ##1 b[->0] ##1 c |-> 1 // is same as 
$rose(a) ##1 b[*0] ##1 c |-> 1 // same as 
<---------------> become $rose(a) ##0 1
$rose(a) ##0  1    ##1 c |-> 1 // same as

see my Paper: Understanding SVA Degeneracy
A MUST READ PAPER FOR SVA USERS!

  • Explains “degenerate sequences” and restrictions.
  • Explains “empty match” when integrating into other sequences.
  • Intriguing case study illustrates potential issues caused by ‘empty’ and ‘within’.

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

1 Like