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

@@ -139,6 +139,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

@@ -23,7 +23,8 @@ Author: Daniel Kroening, [email protected]
 exprt normalize_pre_sva_non_overlapped_implication(
   sva_non_overlapped_implication_exprt expr)
 {
-  // Same as a->always[1:1] b if lhs is not a sequence.
+  // a |=> b is the same as a -> always[1:1] b if the lhs is
+  // not a proper sequence.
   if(!is_SVA_sequence_operator(expr.lhs()))
   {
     auto one = natural_typet{}.one_expr();
@@ -86,7 +87,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

@@ -71,7 +71,7 @@ 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()};
+    // expr = not_exprt{to_sva_not_expr(expr).op()};
   }
   else if(expr.id() == ID_sva_if)
   {

src/trans-word-level/property.cpp

@@ -537,10 +537,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);
 
@@ -576,8 +576,8 @@ static obligationst property_obligations_rec(
     else
     {
       // state formula
-      return obligationst{
-        instantiate_property(property_expr, current, no_timeframes)};
+      auto sampled = instantiate_property(not_exprt{op}, current, no_timeframes);
+      return obligationst{sampled};
     }
   }
   else if(property_expr.id() == ID_sva_implies)

src/verilog/sva_expr.cpp

@@ -118,7 +118,9 @@ exprt sva_sequence_repetition_star_exprt::lower() const
     {
       auto n_expr = from_integer(n, integer_typet{});
       result = sva_or_exprt{
-        std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}};
+        std::move(result),
+        sva_sequence_repetition_star_exprt{op(), n_expr},
+        verilog_sva_sequence_typet{}};
     }
 
     return result;