diff --git a/regression/verilog/SVA/sequence5.desc b/regression/verilog/SVA/sequence5.desc new file mode 100644 index 000000000..77fca4b13 --- /dev/null +++ b/regression/verilog/SVA/sequence5.desc @@ -0,0 +1,14 @@ +KNOWNBUG +sequence5.sv +--bound 0 +^\[main\.p0\] 1: PROVED up to bound 0$ +^\[main\.p1\] 0: REFUTED$ +^\[main\.p2\] 1'bx: PROVED up to bound 0$ +^\[main\.p3\] 1'bz: PROVED up to bound 0$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +x and z are recognized as 'true', but 'true' is defined as a "nonzero known +value" (1800-2017 12.4). diff --git a/regression/verilog/SVA/sequence5.sv b/regression/verilog/SVA/sequence5.sv new file mode 100644 index 000000000..884ef8be3 --- /dev/null +++ b/regression/verilog/SVA/sequence5.sv @@ -0,0 +1,15 @@ +module main; + + // passes, since 10 is true + initial p0: assert property (10); + + // fails, since 0 isn't true + initial p1: assert property (0); + + // fails, since 'x' isn't true + initial p2: assert property (1'bx); + + // fails, since 'z' isn't true + initial p3: assert property (1'bz); + +endmodule