SVA: KNOWNBUG test for a recursive property

Author: kroening

regression/verilog/SVA/recursive_property1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+recursive_property1.sv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The parameter list fails to parse.

regression/verilog/SVA/recursive_property1.sv

@@ -0,0 +1,14 @@
+module main(input clk);
+
+  reg [31:0] x = 0;
+  always_ff @(posedge clk) x = !x;
+
+  // 1800-2017 16.12.17
+  property prop_always(p);
+    p and (1 |=> prop_always(p))
+  endproperty
+
+  // expected to pass
+  assert property (prop_always(x <= 1));
+
+endmodule