Type of Error when using Empty Sequence as Consequent

SystemVerilog
, ,
1

Hi All,
I was referring to empty.pdf shared by Ben in following thread

As Ben mentions that ::

assert property( @(posedge clk) start |-> b[*0] ##0 c );

Is illegal as the consequent admits only No Match

My question is whether it should be flagged as compilation/elaboration time error or a run-time error ?
Does the LRM clarify this or is a tool free to throw an error at run-time as well ?

2

I think the LRM is not very clear here, but I think the intent was it should be an error. The only place it mentions being an error is if you try to attach a call to a subroutine.

I can see arguments both ways because of automatically generated code that might take advantage of the fact that they knowing start will never happen so they don’t care about their consequence having an empty match.

3

Thanks Dave.

LRM Section 16.11 mentions
"It shall be an error to attach a subroutine call or any sequence_match_item to a sequence that admits an empty match "

Here LRM specifically mentions the word “error” ( although it doesn’t clarify the type of error i.e whether it should be compilation/elaboration or run-time error )

Whereas LRM Section 16.12.22 Nondegeneracy mentions ::
“a) Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.”
Here LRM doesn’t explicitly mention it as an error

I observe that some tools throw a compilation error while some throw run-time error.