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

@@ -250,8 +250,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     auto &followed_by = to_sva_followed_by_expr(expr);
     auto not_b = not_exprt{followed_by.consequent()};
     return rec(
-      not_exprt{
-        sva_overlapped_implication_exprt{followed_by.antecedent(), not_b}},
+      not_exprt{sva_overlapped_implication_exprt{
+        followed_by.antecedent(), not_b, bool_typet{}}},
       mode);
   }
   else if(expr.id() == ID_sva_nonoverlapped_followed_by)
@@ -262,8 +262,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     auto &followed_by = to_sva_followed_by_expr(expr);
     auto not_b = not_exprt{followed_by.consequent()};
     return rec(
-      not_exprt{
-        sva_non_overlapped_implication_exprt{followed_by.antecedent(), not_b}},
+      not_exprt{sva_non_overlapped_implication_exprt{
+        followed_by.antecedent(), not_b, bool_typet{}}},
       mode);
   }
   else if(expr.id() == ID_sva_sequence_property)

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);
@@ -63,24 +64,32 @@ exprt normalize_property_rec(exprt expr)
   else if(expr.id() == ID_sva_nexttime)
   {
     auto one = natural_typet{}.one_expr();
-    expr = sva_ranged_always_exprt{one, one, to_sva_nexttime_expr(expr).op()};
+    expr = sva_ranged_always_exprt{
+      one, one, to_sva_nexttime_expr(expr).op(), bool_typet{}};
   }
   else if(expr.id() == ID_sva_s_nexttime)
   {
     auto one = natural_typet{}.one_expr();
-    expr = sva_s_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()};
+    expr = sva_s_always_exprt{
+      one, one, to_sva_s_nexttime_expr(expr).op(), bool_typet{}};
   }
   else if(expr.id() == ID_sva_indexed_nexttime)
   {
     auto &nexttime_expr = to_sva_indexed_nexttime_expr(expr);
     expr = sva_ranged_always_exprt{
-      nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
+      nexttime_expr.index(),
+      nexttime_expr.index(),
+      nexttime_expr.op(),
+      bool_typet{}};
   }
   else if(expr.id() == ID_sva_indexed_s_nexttime)
   {
     auto &nexttime_expr = to_sva_indexed_s_nexttime_expr(expr);
     expr = sva_s_always_exprt{
-      nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()};
+      nexttime_expr.index(),
+      nexttime_expr.index(),
+      nexttime_expr.op(),
+      bool_typet{}};
   }
 
   // normalize the operands
@@ -104,7 +113,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:$]