diff --git a/regression/verilog/SVA/empty_sequence1.desc b/regression/verilog/SVA/empty_sequence1.desc new file mode 100644 index 000000000..d59123e6b --- /dev/null +++ b/regression/verilog/SVA/empty_sequence1.desc @@ -0,0 +1,9 @@ +KNOWNBUG +empty_sequence1.sv +--bound 5 +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Repetition with zero is not implemented. diff --git a/regression/verilog/SVA/empty_sequence1.sv b/regression/verilog/SVA/empty_sequence1.sv new file mode 100644 index 000000000..3ffd20f02 --- /dev/null +++ b/regression/verilog/SVA/empty_sequence1.sv @@ -0,0 +1,14 @@ +module main(input clk); + + reg [7:0] x = 0; + + always @(posedge clk) + x<=x+1; + + // The empty sequence does not match + initial p0: assert property (1[*0]); + + // But can be concatenated + initial p1: assert property (1[*0] ##1 x == 0); + +endmodule