introduce verilog_sva_property_typet

regression/ebmc/smv-netlist/always_with_range1.desc

@@ -4,7 +4,7 @@ always_with_range1.sv
 ^LTLSPEC node275 & X node275 & X X node275 .*
 ^LTLSPEC G node275$
 ^LTLSPEC node275 & X node275 & X X node275 .*
-^LTLSPEC G \(\!node306 \| X node337\)$
+^LTLSPEC G \(X node306 -> node337\)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/hw_cbmc_irep_ids.h

@@ -147,6 +147,7 @@ IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(verilog_event)
 IREP_ID_ONE(verilog_event_trigger)
 IREP_ID_ONE(verilog_string)
+IREP_ID_ONE(verilog_sva_property)
 IREP_ID_ONE(verilog_sva_sequence)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)

src/temporal-logic/sva_to_ltl.cpp

@@ -238,6 +238,38 @@ exprt SVA_to_LTL(exprt expr)
   {
     return expr;
   }
+  else if(expr.id() == ID_sva_implies)
+  {
+    // maps cleanly to 'implies'
+    auto &sva_implies = to_sva_implies_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_implies.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_implies.rhs());
+    return implies_exprt{rec_rhs, rec_lhs};
+  }
+  else if(expr.id() == ID_sva_iff)
+  {
+    // maps cleanly to =
+    auto &sva_iff = to_sva_iff_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_iff.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_iff.rhs());
+    return equal_exprt{rec_rhs, rec_lhs};
+  }
+  else if(expr.id() == ID_sva_and)
+  {
+    // maps cleanly to Boolean and
+    auto &sva_iff = to_sva_iff_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_iff.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_iff.rhs());
+    return and_exprt{rec_rhs, rec_lhs};
+  }
+  else if(expr.id() == ID_sva_or)
+  {
+    // maps cleanly to Boolean or
+    auto &sva_iff = to_sva_iff_expr(expr);
+    auto rec_lhs = SVA_to_LTL(sva_iff.lhs());
+    auto rec_rhs = SVA_to_LTL(sva_iff.rhs());
+    return or_exprt{rec_rhs, rec_lhs};
+  }
   else if(
     expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or ||
     expr.id() == ID_not)

src/verilog/sva_expr.cpp

@@ -11,6 +11,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/mathematical_types.h>
 
+exprt sva_iff_exprt::implications() const
+{
+  return sva_and_exprt{
+    sva_implies_exprt{lhs(), rhs()}, sva_implies_exprt{rhs(), lhs()}, type()};
+}
+
 exprt sva_cycle_delay_plus_exprt::lower() const
 {
   // same as ##[1:$]