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

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

@@ -84,7 +84,7 @@ exprt trivial_sva(exprt expr)
   }
   else if(expr.id() == ID_sva_not)
   {
-    // Same as regular 'not'. These do not apply to sequences.
+    // Same as boolean 'not'. These do not apply to sequences.
     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,9 @@ 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;