introduce sva_implies and sva_iff

This introduces separate expressions for SVA iff and SVA implies.

Author: kroening

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_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

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)

src/temporal-logic/normalize_property.cpp

@@ -143,6 +143,16 @@ exprt normalize_property(exprt expr)
   else if(expr.id() == ID_sva_non_overlapped_implication)
     expr = normalize_pre_sva_non_overlapped_implication(
       to_sva_non_overlapped_implication_expr(expr));
+  else if(expr.id() == ID_sva_iff)
+  {
+    expr =
+      equal_exprt{to_sva_iff_expr(expr).lhs(), to_sva_iff_expr(expr).rhs()};
+  }
+  else if(expr.id() == ID_sva_implies)
+  {
+    expr = implies_exprt{
+      to_sva_implies_expr(expr).lhs(), to_sva_implies_expr(expr).rhs()};
+  }
   else if(expr.id() == ID_sva_and)
     expr = normalize_pre_sva_and(to_sva_and_expr(expr));
   else if(expr.id() == ID_sva_not)

src/temporal-logic/normalize_property.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 /// ¬(a ∨ b) --> ¬a ∧ ¬b
 /// ¬(a ∧ b) --> ¬a ∨ ¬b
 /// (a -> b) --> ¬a ∨ b
+/// a sva_iff b --> a <-> b
+/// a sva_implies b --> a -> b
 /// sva_not a --> ¬a
 /// a sva_and b --> a ∧ b                       if a and b are not SVA sequences
 /// a sva_or b --> a ∨ b                        if a and b are not SVA sequences

src/verilog/expr2verilog.cpp

@@ -1273,6 +1273,12 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
   else if(src.id() == ID_sva_and)
     return convert_sva_binary("and", to_sva_and_expr(src));
 
+  else if(src.id() == ID_sva_iff)
+    return convert_sva_binary("iff", to_sva_iff_expr(src));
+
+  else if(src.id() == ID_sva_implies)
+    return convert_sva_binary("implies", to_sva_implies_expr(src));
+
   else if(src.id()==ID_power)
     return convert_binary(
       to_multi_ary_expr(src), "**", precedence = verilog_precedencet::POWER);

src/verilog/parser.y

@@ -2200,9 +2200,9 @@ property_expr_proper:
 	| property_expr "s_until_with" property_expr
 		{ init($$, "sva_s_until_with"); mto($$, $1); mto($$, $3); }
 	| property_expr "implies" property_expr
-		{ init($$, ID_implies); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_sva_implies); mto($$, $1); mto($$, $3); }
 	| property_expr "iff" property_expr
-		{ init($$, ID_iff); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_sva_iff); mto($$, $1); mto($$, $3); }
 	| "accept_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"
 		{ init($$, ID_sva_accept_on); mto($$, $3); mto($$, $5); }
 	| "reject_on" '(' expression_or_dist ')' property_expr %prec "property_expr_abort"