Discrepancy on legality of the consequent

SystemVerilog
, , ,
1

Hi All,
I was trying to model dynamic repeat using a user-defined sequence.
Here is my attempt :: edalink

LRM 16.12.22 Nondegeneracy states

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.

I observe that one tool treats the consequent as illegal whereas as per my understanding the consequent is legal.
Refer the right side ( design.sv ) in edalink where I have noted my interpretation of the consequent

[Q1] Just wanted to check with forum moderators if my understanding is correct

I tried a simplified version of the consequent in edalink2 where the output matches my understanding

2

I sent this for the next 1800 version. Did you see it?
SVA: 1800’2023 Degeneracy Issue to Hopefully be Addressed in 1800’2028
When faced with degenerate sequences, 1800’2023 is unclear on what a simulator should do, particularly in situations resulting from parameter substitution that creates a degenerate sequence. In that situation, it would be undesirable to have to rewrite the code to get to a successful compilation. Existing tools differ in their interpretation of degenerate sequences - some report it as a degenerate situation, some issue a warning, and some proceed with the simulation.
This linked document identifies the sections in the LRM that define degeneracy and highlights cases that pose challenges for users and tool vendors. Additionally, it proposes solutions for the next revision of the LRM.
Ben, in collaboration with Ed Cerny

3

Ben,
(1) I was referring to following quote from Degeneracy_1800_2028.pdf

5) Never be matched, no match can exist 
  (ii) a ##1 1’b0-- logically impossible- a followed by false

case (5.ii) is attributed to a false logical value resulting from parameter substitution. In both scenarios, if utilized in a property, they would lead to an unsatisfied property

I am not clear on “attributed to a false logical value resulting from parameter substitution”

I found a thread related to using hard zero in concurrent assertion where Dave commented

“In the hard_zero assertion, the (0) does not get evaluated until run-time”

(2) In the original post the irony is that the same tool ( VCS ) that throws compilation error for edalink treats ‘sva2’ in edalink2 as legal.

It seems like a tool issue/limitation as in both cases the consequent is equivalent to
( 1'b0 ) or ( Non_Degenerate_Sequence ) i.e ( Non_Degenerate_Sequence )

As consequent :: ( 1'b0 ) or ( Non_Degenerate_Sequence ) doesn’t violate the following LRM quote

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.

I am of the opinion that consequent is legal in edalink

Please correct me if I am wrong in my interpretation.

4

[YOU] I am not clear on “attributed to a false logical value resulting from parameter substitution”
[Ben] Example or param substitution: Edit code - EDA Playground

module m #(parameter K = 1) // parameter with default value

(input bit clk, a, b);

ap_impossible: assert property(@(posedge clk) a |-> b ##1 K);

endmodule

module top;

bit a=1, b=1, clk;

always #1 clk=!clk;

m #(0) m1 (.clk(clk), .a(a), .b(b)); // override parameter value

initial #100 $finish;

endmodule

[YOU] I found a thread related to using hard zero in concurrent assertion where Dave commented
“In the hard_zero assertion, the (0) does not get evaluated until run-time”

(2) In the original post the irony is that the same tool ( VCS ) that throws compilation error for edalink treats ‘sva2’ in edalink2 as legal.

It seems like a tool issue/limitation as in both cases the consequent is equivalent to
( 1’b0 ) or ( Non_Degenerate_Sequence ) i.e ( Non_Degenerate_Sequence )

As consequent :: ( 1’b0 ) or ( Non_Degenerate_Sequence ) doesn’t violate the following LRM quote

Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.

I am of the opinion that consequent is legal in edalink
 [Ben]
1800 says a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
You are addressing case 3 in the pdf:
Empty and non-empty matches
a[*0:1] – empty and a possible non-empty match
It does admit an empty match.

This is why we wrote this potential change to 1800…

5

Ben ,
There is a difference between the following sequences when used as consequent
(1) a[*0:1] // Admits ‘Empty match’ via a[*0]
(2) a[*0:1] ##0 1 // Admits ‘No match’ ( 1’b0 ) via ( a[*0] ##0 1 )

(1) is illegal as it violates the LRM quote since the consequent admits empty match via a[*0]

(2) is legal as consequent since it doesn’t violate the above LRM quote

The same can be comfirmed in edalink2 where ‘sva1’ is illegal and ‘sva2’ is legal

In my original post the consequent in edalink resembles (2) and not (1)

VCS treats ‘sva2’ in eda2 legal whereas it treats consequent in eda as illegal

In both cases a sub-sequence in the consequent is ( empty_seq ##0 seq )
i.e it admits ‘No match’ ( 1’b0 )

Hence I believe the compilation error observed in edalink is a tool limitation/issue as the consequent doesn’t admit any empty match.

6

I found a related example on Pg 41 in empty.pdf shared in empty-sequence-in-systemverilog

a |-> b[*0:1] ##0 c; // is equivalent to  
a |-> (b[*0] ##0 c) or (b[*1] ##0 c); // is equivalent to 
a |-> 0 or (b[*1] ##0 c); // is equivalent to 
a |-> b[*1] ##0 c;

The above consequent is considered legal ( although a sub-seq. admits “No match” ) as it ::
(1) Doesn’t admit any empty match
(2) Admits non-empty match

On the same note, sub-sequence ((count == 0) ##0 (seq[*0] ##0 seq3)) in edalink
is equivalent to ( seq_expr ##0 (1'b0) ) i.e “No Match” ( 1’b0 )

7

(b[*0] ##0 c) // is (empty ##0 c) and that is degenerate
// it is not (0 ##0 c). We talked about degeneracy rues
(count == 0) is legal and can evaluate to true or false depending on the value of count. That is different than
a |-> 0 ##1 1; // it is degenrate by construction

8

Ben,
As you mentioned in your 1st reply

When faced with degenerate sequences, 1800’2023 is unclear on what a simulator should do

Since we are not supposed to discuss tool related issues, I am curious to know
From a strict LRM perspective is the consequent sequence ‘abd_dynamic_repeat’ in edalink legal ?

As per my understanding it doesn’t violate the following LRM quote

1800 says a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.

The consequent is essentially :: sub_seq1 or sub_seq2

Sub-sequence1 ( (count == 0) ##0 ( seq[*0] ##0 seq3 ) ) is equivalent to
seq_expr1 ##0( empty_seq ##0 seq_expr2 ) i.e seq_expr1 ##0 ( 1'b0 )

Hence sub-sequence1 admits “No Match”
The other Sub-sequence2 admits only non-empty match

Consequent Is same as :: ( 1'b0 ) or ( sub_seq2 ) i.e sub_seq2

9 

(a[*0] ##0 b) // degenerate

or c;

Is not degenerate because it does admit a non empty match “c”.

And it does not admit empty matches. Hence it is OK as a property. Equivalent to just a “c”.

Q: What is the meaning of “admit”?

A: That is can accept or match a certain sequence.

10

So to conclude the thread

  • The consequent sequence in edalink is nondegenerate and it doesn’t admit any empty match. Hence it’s legal.

  • The compilation error thrown by one of the tool is incorrect