SVA: sequence and property instance expressions

IEEE 1800-2017 refers to sequence and property instances, and rewriting
algorithms for them (F.4.1).

This introduces an expression class each for sequence and property instance
expressions.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -80,6 +80,7 @@ IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)
 IREP_ID_ONE(sva_sequence_non_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_property)
+IREP_ID_ONE(sva_sequence_property_instance)
 IREP_ID_ONE(sva_sequence_repetition_star)
 IREP_ID_ONE(sva_sequence_repetition_plus)
 IREP_ID_ONE(sva_sequence_throughout)

src/verilog/expr2verilog.cpp

@@ -1483,6 +1483,45 @@ expr2verilogt::convert_inside(const verilog_inside_exprt &src)
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_sequence_property_instance
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_sequence_property_instance(
+  const sva_sequence_property_instance_exprt &src)
+{
+  if(src.arguments().empty())
+    return convert_rec(src.symbol());
+
+  auto fkt = convert_rec(src.symbol());
+
+  std::string dest = fkt.s;
+  bool first = true;
+  dest += "(";
+
+  for(const auto &op : src.arguments())
+  {
+    if(first)
+      first = false;
+    else
+      dest += ", ";
+
+    dest += convert_rec(op).s;
+  }
+
+  dest += ")";
+
+  return {verilog_precedencet::MEMBER, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_value_range
 
   Inputs:
@@ -2015,6 +2054,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id() == ID_zero_extend)
     return convert_rec(to_zero_extend_expr(src).op());
 
+  else if(src.id() == ID_sva_sequence_property_instance)
+  {
+    return convert_sequence_property_instance(
+      to_sva_sequence_property_instance_expr(src));
+  }
+
   // no VERILOG language expression for internal representation
   return convert_norep(src);
 }

src/verilog/expr2verilog_class.h

@@ -17,6 +17,7 @@ class sva_if_exprt;
 class sva_ranged_predicate_exprt;
 class sva_cycle_delay_exprt;
 class sva_sequence_first_match_exprt;
+class sva_sequence_property_instance_exprt;
 class sva_sequence_repetition_exprt;
 
 // Precedences (higher means binds more strongly).
@@ -180,6 +181,9 @@ class expr2verilogt
 
   resultt convert_value_range(const class verilog_value_range_exprt &);
 
+  resultt convert_sequence_property_instance(
+    const class sva_sequence_property_instance_exprt &);
+
 protected:
   const namespacet &ns;
 };

src/verilog/sva_expr.h

@@ -2047,4 +2047,56 @@ enum class sva_sequence_semanticst
   STRONG
 };
 
+/// a base class for both sequence and property instance expressions
+class sva_sequence_property_instance_exprt : public binary_exprt
+{
+public:
+  sva_sequence_property_instance_exprt(
+    symbol_exprt _symbol,
+    exprt::operandst _arguments)
+    : binary_exprt{
+        _symbol,
+        ID_sva_sequence_property_instance,
+        multi_ary_exprt{ID_arguments, std::move(_arguments), typet{}},
+        _symbol.type()}
+  {
+  }
+
+  const symbol_exprt &symbol() const
+  {
+    return static_cast<const symbol_exprt &>(op0());
+  }
+
+  symbol_exprt &symbol()
+  {
+    return static_cast<symbol_exprt &>(op0());
+  }
+
+  exprt::operandst &arguments()
+  {
+    return op1().operands();
+  }
+
+  const exprt::operandst &arguments() const
+  {
+    return op1().operands();
+  }
+};
+
+inline const sva_sequence_property_instance_exprt &
+to_sva_sequence_property_instance_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_property_instance);
+  sva_sequence_property_instance_exprt::check(expr);
+  return static_cast<const sva_sequence_property_instance_exprt &>(expr);
+}
+
+inline sva_sequence_property_instance_exprt &
+to_sva_sequence_property_instance_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_property_instance);
+  sva_sequence_property_instance_exprt::check(expr);
+  return static_cast<sva_sequence_property_instance_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_synthesis.cpp

@@ -71,6 +71,12 @@ exprt verilog_synthesist::synth_expr_rec(exprt expr, symbol_statet symbol_state)
   {
     return expand_function_call(to_function_call_expr(expr), symbol_state);
   }
+  else if(expr.id() == ID_sva_sequence_property_instance)
+  {
+    auto &instance = to_sva_sequence_property_instance_expr(expr);
+    const symbolt &symbol = ns.lookup(instance.symbol());
+    return synth_expr(symbol.value, symbol_state);
+  }
   else if(expr.id() == ID_hierarchical_identifier)
   {
     expand_hierarchical_identifier(

src/verilog/verilog_typecheck_expr.cpp

@@ -1360,6 +1360,16 @@ exprt verilog_typecheck_exprt::convert_symbol(
       result.add_source_location()=source_location;
       return result;
     }
+    else if(
+      symbol->type.id() == ID_verilog_sva_sequence ||
+      symbol->type.id() == ID_verilog_sva_property)
+    {
+      // A named sequence or property. Use an instance expression.
+      expr.type() = symbol->type;
+      expr.set_identifier(symbol->name);
+      return sva_sequence_property_instance_exprt{expr, {}}
+        .with_source_location(expr);
+    }
     else
     {
       expr.type()=symbol->type;