ebmc: add two basic tests for CEGAR

Author: kroening

regression/ebmc/cegar/basic1.desc

@@ -0,0 +1,6 @@
+CORE
+basic1.sv
+--cegar
+^VERIFICATION SUCCESSFUL -- PROPERTY HOLDS$
+^EXIT=0$
+^SIGNAL=0$

regression/ebmc/cegar/basic1.sv

@@ -0,0 +1,12 @@
+module top(input clk);
+
+  reg important;
+  reg not_important;
+
+  initial important = 1;
+  always @(posedge clk)
+    important = important;
+
+  assert property (important == 1);
+
+endmodule

regression/ebmc/cegar/basic2.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+basic2.sv
+--cegar
+^VERIFICATION FAILED -- PROPERTY REFUTED$
+^EXIT=0$
+^SIGNAL=0$

regression/ebmc/cegar/basic2.sv

@@ -0,0 +1,13 @@
+module top(input clk);
+
+  reg important;
+  reg not_important;
+
+  initial important = 1;
+  always @(posedge clk)
+    important = 0;
+
+  // should fail after one transition
+  assert property (important == 1);
+
+endmodule