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/verilog/sva_expr.cpp

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