Using property expression ( a[*0] ##1 b[*0] ) |=> c

SystemVerilog
, ,
1

Hello Forum ,
I am trying the following concurrent assertion

 bit  clk , a , b , c;
 always #5 clk = !clk;
 ap1:assert property( @(posedge clk) a[*0] ##1 b[*0] |=> c ) 
            $display("T:%0t Pass",$time); else  $display("T:%0t Fails",$time);
  initial  begin
    #4 ; c = 1 ;
    #12 ; $finish();
  end

Based on my understanding: antecedent sequence ( a[*0] ## 1 b[*0] ) is equivalent to a[*0].
Equivalent property expression a[*0] |=> c is equivalent to ( a[*0] ## 1 1 |-> c ) i.e ( 1 |-> c )

My expected output is pass reports at time:5 and time:15 i.e 2 pass reports in total whereas currently the closest matching output ( as it varies across tools ) I observe is only 1 pass report at time:15

As ‘c’ is true on each clocking event I expected a pass report at time:5 and time:15 respectively

What should be the output for ‘ap1’ ?

2

Based on 16.12.22 Nondegeneracy
b) Any sequence that is used as the antecedent of an overlapping implication (|->) shall be nondegenerate.
c) Any sequence that is used as the antecedent of a nonoverlapping implication (|=>) shall admit at least one match.
Such a sequence can admit only empty matches.
This code should display a pass at t5, 15, and t25

  bit  clk , a , b , c;
  int p1, f1;
 always #5 clk = !clk;
  ap1:assert property( @(posedge clk) a[*0] ##1 b[*0] |=> 
                      (c, $display("%t c==1 PASS", $realtime)) ) 
    begin p1++; $display("T:%0t Pass",$time);  end
    else  begin f1++; $display("T:%0t Fails",$time); end
  initial  begin
     $dumpfile("dump.vcd"); $dumpvars;
    #4 ; c = 1 ;
    #22 ; $finish();
  end
endmodule

If a tool does not behave as such and tells you that it is illegal,
or the pass is not at t5, then it is in error.
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

3

Ben,
Atleast one tool does not pass at t5 (and no error either). Things do work after 15ns as expected though. Ideal for SVA Linting/static checking to flag!

4

It looks to me that

a[*0] ##1 b[*0] |=> c;  // is acting as 
1 |=> c; // which is in error
a[*0] |=> c;  // is often interpreted as 0 |=> c, // also in error

In any case, one should avoid degenerate sequences.
Am uploading my paper on degeneracy
Ben
Degeneracy111723Ben (4).pdf (251.6 KB)

5

I believe there is a typo.

a[*0] ##1 b[*0] |=> c;  // is equivalent to 
a[*0] ##0 1 |=> c;  
// Which can re-written as
a[*0] ##1 1 |-> c;   
i.e  1 |-> c ;  // Legal antecedent

Since the antecedent is always true there would be a non-vacuous pass on each clocking event.

LRM 16.12.22 ::

Any sequence that is used as the antecedent of a nonoverlapping implication (|=>) shall admit at
least one match. Such a sequence can admit only empty matches.

Antecedent in our case ( a[*0] ## 1 b[*0] ) is equivalent to ( a[*0] ## 0 1 ) i.e ( a[*0] )
which admits only empty match. Hence it’s legal as per LRM.

6

Blockquote

a[*0] ##1 b[*0] |=> c;  // is acting as

1 |=> c; // which is in error

I believe there is a typo

Blockquote
I meant to say that the tools “ACTED” (i.e., behaved) as if it had "a |=> " instead of “a |->”. That is why it missed the PASS at t5
Your analysis is correct.
Also, if you tried a[*0] |=> c; the tool acted (behaved) as if you had
0 |=> c;
Th point, this whole thing is not processed correctly.