Merge pull request #681 from diffblue/sequence5

KNOWNBUG test for casting z/x to Boolean

Author: tautschnig

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).

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