diff --git a/regression/verilog/SVA/stable1.desc b/regression/verilog/SVA/stable1.desc new file mode 100644 index 000000000..4cbf41450 --- /dev/null +++ b/regression/verilog/SVA/stable1.desc @@ -0,0 +1,9 @@ +CORE +stable1.sv +--bound 20 +^\[main\.p0\] always \(\$stable\(main\.data\) \|=> main\.counter >= 1\): PROVED up to bound 20$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/stable1.sv b/regression/verilog/SVA/stable1.sv new file mode 100644 index 000000000..6a0d894c8 --- /dev/null +++ b/regression/verilog/SVA/stable1.sv @@ -0,0 +1,17 @@ +module main(input clk, input data); + + reg data_old = 0; + reg [2:0] counter = 0; + + always_ff @(posedge clk) + if(data != data_old) + counter = 0; + else if(counter < 3) + counter++; + + always_ff @(posedge clk) + data_old = data; + + p0: assert property ($stable(data) |=> counter >= 1); + +endmodule