From my degeneracy paper
b[=0] // is equivalent to:
##0 !b[*0]) or (##0 !b[*1:$])
Thus, you are correct in that due to [=0] the consequent admits empty match and violates the quote from
2.LRM 16.12.22 Nondegeneracy*
Any sequence that is used as a property shall be nondegenerate and shall not admit any empty match.
I like your solution
assert property(@(posedge clk) ( (cmd[1:0] == 2'b10)[=1:4] or (cmd[1:0] != 2'b10)[*60] ) intersect 1 [*60]);
I sent this to members of the SV and SVA committee to address this degenracy issue for the next 1800 revision.
Issue:
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.
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 Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.