introduce verilog_sva_property_typet

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

Author: kroening

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

@@ -105,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/trivial_sva.cpp

@@ -32,17 +32,32 @@ exprt trivial_sva(exprt expr)
     auto rhs = is_state_predicate(sva_implication.rhs());
 
     if(lhs.has_value() && rhs.has_value())
-      expr = implies_exprt{*lhs, *rhs};
+      expr = sva_boolean_exprt{
+        implies_exprt{*lhs, *rhs}, verilog_sva_property_typet{}};
   }
   else if(expr.id() == ID_sva_iff)
   {
+    // same as boolean iff when both lhs/rhs are state predicates
     auto &sva_iff = to_sva_iff_expr(expr);
-    expr = equal_exprt{sva_iff.lhs(), sva_iff.rhs()};
+
+    auto lhs = is_state_predicate(sva_iff.lhs());
+    auto rhs = is_state_predicate(sva_iff.rhs());
+
+    if(lhs.has_value() && rhs.has_value())
+      expr = sva_boolean_exprt{
+        equal_exprt{*lhs, *rhs}, verilog_sva_property_typet{}};
   }
   else if(expr.id() == ID_sva_implies)
   {
+    // same as boolean implication when both lhs/rhs are state predicates
     auto &sva_implies = to_sva_implies_expr(expr);
-    expr = implies_exprt{sva_implies.lhs(), sva_implies.rhs()};
+
+    auto lhs = is_state_predicate(sva_implies.lhs());
+    auto rhs = is_state_predicate(sva_implies.rhs());
+
+    if(lhs.has_value() && rhs.has_value())
+      expr = sva_boolean_exprt{
+        implies_exprt{*lhs, *rhs}, verilog_sva_property_typet{}};
   }
   else if(expr.id() == ID_sva_and)
   {
@@ -84,11 +99,16 @@ exprt trivial_sva(exprt expr)
   }
   else if(expr.id() == ID_sva_not)
   {
-    // Same as regular 'not'. These do not apply to sequences.
-    expr = not_exprt{to_sva_not_expr(expr).op()};
+    // Same as boolean 'not' when applied to a state predicate.
+    auto &op = to_sva_not_expr(expr).op();
+    auto predicate = is_state_predicate(op);
+    if(predicate.has_value())
+      expr =
+        sva_boolean_exprt{not_exprt{*predicate}, verilog_sva_property_typet{}};
   }
   else if(expr.id() == ID_sva_if)
   {
+    // same as boolean 'if' when both cases are state predicates.
     auto &sva_if_expr = to_sva_if_expr(expr);
     auto false_case = sva_if_expr.false_case().is_nil()
                         ? true_exprt{}

src/trans-word-level/property.cpp

@@ -530,10 +530,10 @@ static obligationst property_obligations_rec(
     return property_obligations_rec(
       to_typecast_expr(property_expr).op(), current, no_timeframes);
   }
-  else if(property_expr.id() == ID_not)
+  else if(property_expr.id() == ID_sva_not)
   {
     // We need NNF, try to eliminate the negation.
-    auto &op = to_not_expr(property_expr).op();
+    auto &op = to_sva_not_expr(property_expr).op();
 
     auto op_negated_opt = negate_property_node(op);
 
@@ -570,8 +570,9 @@ static obligationst property_obligations_rec(
     else
     {
       // state formula
-      return obligationst{
-        current, instantiate_property(property_expr, current, no_timeframes)};
+      auto sampled =
+        instantiate_property(not_exprt{op}, current, no_timeframes);
+      return obligationst{current, sampled};
     }
   }
   else if(property_expr.id() == ID_sva_implies)