diff --git a/regression/verilog/SVA/sequence4.desc b/regression/verilog/SVA/sequence4.desc new file mode 100644 index 000000000..bbd662bc2 --- /dev/null +++ b/regression/verilog/SVA/sequence4.desc @@ -0,0 +1,9 @@ +KNOWNBUG +sequence4.sv +--bound 10 +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +sequence concatenation is not supported by the BMC engine diff --git a/regression/verilog/SVA/sequence4.sv b/regression/verilog/SVA/sequence4.sv new file mode 100644 index 000000000..b24d38ed1 --- /dev/null +++ b/regression/verilog/SVA/sequence4.sv @@ -0,0 +1,14 @@ +module main; + + reg [31:0] x; + wire clk; + + initial x=0; + + always @(posedge clk) + x<=x+1; + + // sequence concatenation + initial p0: assert property (x == 0 ##1 x == 1 ##1 x == 2); + +endmodule