Verilog: KNOWNBUG test for $past when using the BDD engine

Author: kroening

regression/verilog/system-functions/past2.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+past2.sv
+--bdd
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The AIG translation is yet to support $past.

regression/verilog/system-functions/past2.sv

@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg [31:0] counter = 0;
+
+  always @(posedge clk)
+    if(counter < 10)
+      counter++;
+
+  p0: assert property (counter == 0 |-> $past(counter, 1) == 0);
+//  p1: assert property (counter != 0 && counter != 10 |-> $past(counter, 1) == counter - 1);
+
+endmodule