[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…