Merge pull request #680 from diffblue/sva_and1

SVA Boolean connectives

Author: tautschnig

regression/verilog/SVA/eventually1.desc

@@ -1,7 +1,7 @@
 CORE
 eventually1.sv
 --bound 20
-^\[main\.property\.p0\] always \(main\.counter == 1 |-> eventually \[1:2\] main\.counter == 3\): PROVED up to bound 20$
+^\[main\.p0\] always main\.counter == 1 implies \(eventually \[1:2\] main\.counter == 3\): PROVED up to bound 20$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/sva_and1.desc

@@ -0,0 +1,11 @@
+CORE
+sva_and1.sv
+--bound 0
+^\[main\.p0\] always 1 and 1: PROVED up to bound 0$
+^\[main\.p1\] always 1 and 0: REFUTED$
+^\[main\.p2\] always 1 and 32'b0000000000000000000000000000000x: PROVED up to bound 0$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sva_and1.sv

@@ -0,0 +1,12 @@
+module main;
+
+  // should pass
+  p0: assert property (10 and 20);
+
+  // should fail
+  p1: assert property (10 and 0);
+
+  // should fail
+  p2: assert property (10 and 'bx);
+
+endmodule

regression/verilog/SVA/sva_iff1.desc

@@ -0,0 +1,11 @@
+CORE
+sva_iff1.sv
+--bound 0
+^\[main\.p0\] always 1 iff 1: PROVED up to bound 0$
+^\[main\.p1\] always 1 iff 0: REFUTED$
+^\[main\.p2\] always 1 iff 32'b0000000000000000000000000000000x: PROVED up to bound 0$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sva_iff1.sv

@@ -0,0 +1,12 @@
+module main;
+
+  // should pass
+  p0: assert property (10 iff 20);
+
+  // should fail
+  p1: assert property (10 iff 0);
+
+  // should fail
+  p2: assert property (10 iff 'bx);
+
+endmodule

regression/verilog/SVA/sva_implies1.desc

@@ -0,0 +1,11 @@
+CORE
+sva_implies1.sv
+--bound 0
+^\[main\.p0\] always 1 implies 1: PROVED up to bound 0$
+^\[main\.p1\] always 1 implies 0: REFUTED$
+^\[main\.p2\] always 1 implies 32'b0000000000000000000000000000000x: PROVED up to bound 0$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/SVA/sva_implies1.sv

@@ -0,0 +1,12 @@
+module main;
+
+  // should pass
+  p0: assert property (10 implies 20);
+
+  // should fail
+  p1: assert property (10 implies 0);
+
+  // should fail
+  p2: assert property (10 implies 'bx);
+
+endmodule

regression/verilog/SVA/sva_not1.desc

@@ -0,0 +1,9 @@
+CORE
+sva_not1.sv
+--k-induction
+^\[main\.p0] always not 0: PROVED$
+^\[main\.p1] always not 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/SVA/sva_not1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  // should pass
+  p0: assert property (not 0);
+
+  // should fail
+  p1: assert property (not 1);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -55,6 +55,8 @@ IREP_ID_ONE(sva_nonoverlapped_followed_by)
 IREP_ID_ONE(sva_overlapped_implication)
 IREP_ID_ONE(sva_non_overlapped_implication)
 IREP_ID_ONE(sva_and)
+IREP_ID_ONE(sva_iff)
+IREP_ID_ONE(sva_implies)
 IREP_ID_ONE(sva_not)
 IREP_ID_ONE(sva_or)
 IREP_ID_ONE(module_instance)