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

@@ -38,24 +38,38 @@ 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}, expr.type()};
   }
   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}, expr.type()};
   }
   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}, expr.type()};
   }
   else if(expr.id() == ID_sva_and)
   {
     auto &sva_and = to_sva_and_expr(expr);
 
     // can be sequence or property
-    if(expr.type().id() == ID_verilog_sva_sequence)
+    if(
+      expr.type().id() == ID_verilog_sva_sequence ||
+      expr.type().id() == ID_verilog_sva_property)
     {
       // Same as a ∧ b if the expression is not a sequence.
       auto lhs = is_state_predicate(sva_and.lhs());
@@ -64,37 +78,36 @@ exprt trivial_sva(exprt expr)
       if(lhs.has_value() && rhs.has_value())
         expr = sva_boolean_exprt{and_exprt{*lhs, *rhs}, expr.type()};
     }
-    else
-    {
-      expr = and_exprt{sva_and.lhs(), sva_and.rhs()};
-    }
   }
   else if(expr.id() == ID_sva_or)
   {
     auto &sva_or = to_sva_or_expr(expr);
 
     // can be sequence or property
-    if(expr.type().id() == ID_verilog_sva_sequence)
+    if(
+      expr.type().id() == ID_verilog_sva_sequence ||
+      expr.type().id() == ID_verilog_sva_property)
     {
-      // Same as a ∨ b if the expression is not a sequence.
+      // Same as a ∨ b if the expression is a state predicate.
       auto lhs = is_state_predicate(sva_or.lhs());
       auto rhs = is_state_predicate(sva_or.rhs());
 
       if(lhs.has_value() && rhs.has_value())
         expr = sva_boolean_exprt{or_exprt{*lhs, *rhs}, expr.type()};
     }
-    else
-    {
-      expr = or_exprt{sva_or.lhs(), sva_or.rhs()};
-    }
   }
   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)

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