introduce verilog_sva_property_typet

This introduces a type for Verilog SVA properties to distinguish properties
from state predicates and sequences.

Author: kroening

regression/verilog/SVA/named_property1.desc

@@ -0,0 +1,8 @@
+CORE
+named_property1.sv
+
+^file .* line 12: sequence required, but got property$
+^EXIT=2$
+^SIGNAL=0$
+--
+--

regression/verilog/SVA/named_property1.sv

@@ -0,0 +1,15 @@
+module main(input clk);
+
+  wire [31:0] x = 10;
+
+  property x_is_ten;
+    x == 10
+  endproperty : x_is_ten
+
+  // Cannot be used as a sequence, even when it syntactically
+  // qualifies as a sequence.
+  sequence some_sequence;
+    x_is_ten
+  endsequence
+
+endmodule

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/normalize_property.cpp

@@ -27,8 +27,9 @@ exprt normalize_pre_sva_non_overlapped_implication(
   {
     const auto &lhs_cond = to_sva_boolean_expr(expr.lhs()).op();
     auto one = natural_typet{}.one_expr();
-    return or_exprt{
-      not_exprt{lhs_cond}, sva_ranged_always_exprt{one, one, expr.rhs()}};
+    auto ranged_always = sva_ranged_always_exprt{one, one, expr.rhs()};
+    ranged_always.type() = bool_typet{};
+    return or_exprt{not_exprt{lhs_cond}, ranged_always};
   }
   else
     return std::move(expr);
@@ -104,7 +105,7 @@ exprt normalize_property(exprt expr)
 {
   // top-level only
   if(expr.id() == ID_sva_cover)
-    expr = sva_always_exprt{not_exprt{to_sva_cover_expr(expr).op()}};
+    expr = sva_always_exprt{sva_not_exprt{to_sva_cover_expr(expr).op()}};
 
   expr = trivial_sva(expr);
 

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/temporal-logic/trivial_sva.cpp

@@ -23,6 +23,10 @@ static std::optional<exprt> is_state_predicate(const exprt &expr)
 exprt trivial_sva(exprt expr)
 {
   // pre-traversal
+  if(expr.type().id() == ID_verilog_sva_property)
+  {
+    expr.type() = bool_typet{};
+  }
 
   // rewrite the operands, recursively
   for(auto &op : expr.operands())

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:$]