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

@@ -74,9 +74,11 @@ IREP_ID_ONE(sva_cycle_delay)
 IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
 IREP_ID_ONE(sva_disable_iff)
+IREP_ID_ONE(sva_property_instance)
 IREP_ID_ONE(sva_sequence_disable_iff)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_sequence_goto_repetition)
+IREP_ID_ONE(sva_sequence_instance)
 IREP_ID_ONE(sva_sequence_intersect)
 IREP_ID_ONE(sva_sequence_non_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_property)

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,14 @@ 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_instance ||
+    src.id() == ID_sva_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,142 @@ 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(
+    irep_idt _id,
+    symbol_exprt _symbol,
+    exprt::operandst _arguments,
+    typet _type)
+    : binary_exprt{
+        std::move(_symbol),
+        _id,
+        multi_ary_exprt{ID_arguments, std::move(_arguments), typet{}},
+        std::move(_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_instance ||
+    expr.id() == ID_sva_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_instance ||
+    expr.id() == ID_sva_property_instance);
+  sva_sequence_property_instance_exprt::check(expr);
+  return static_cast<sva_sequence_property_instance_exprt &>(expr);
+}
+
+class sva_sequence_instance_exprt : public sva_sequence_property_instance_exprt
+{
+public:
+  sva_sequence_instance_exprt(
+    symbol_exprt _sequence,
+    exprt::operandst _arguments)
+    : sva_sequence_property_instance_exprt{
+        ID_sva_sequence_instance,
+        std::move(_sequence),
+        std::move(_arguments),
+        verilog_sva_sequence_typet{}}
+  {
+  }
+
+  const symbol_exprt &sequence() const
+  {
+    return symbol();
+  }
+
+  symbol_exprt &sequence()
+  {
+    return symbol();
+  }
+};
+
+inline const sva_sequence_instance_exprt &
+to_sva_sequence_instance_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_instance);
+  sva_sequence_instance_exprt::check(expr);
+  return static_cast<const sva_sequence_instance_exprt &>(expr);
+}
+
+inline sva_sequence_instance_exprt &to_sva_sequence_instance_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_instance);
+  sva_sequence_instance_exprt::check(expr);
+  return static_cast<sva_sequence_instance_exprt &>(expr);
+}
+
+class sva_property_instance_exprt : public sva_sequence_property_instance_exprt
+{
+public:
+  sva_property_instance_exprt(
+    symbol_exprt _property,
+    exprt::operandst _arguments)
+    : sva_sequence_property_instance_exprt{
+        ID_sva_property_instance,
+        std::move(_property),
+        std::move(_arguments),
+        verilog_sva_property_typet{}}
+  {
+  }
+
+  const symbol_exprt &property() const
+  {
+    return symbol();
+  }
+
+  symbol_exprt &property()
+  {
+    return symbol();
+  }
+};
+
+inline const sva_property_instance_exprt &
+to_sva_property_instance_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_property_instance);
+  sva_property_instance_exprt::check(expr);
+  return static_cast<const sva_property_instance_exprt &>(expr);
+}
+
+inline sva_property_instance_exprt &to_sva_property_instance_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_property_instance);
+  sva_property_instance_exprt::check(expr);
+  return static_cast<sva_property_instance_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_synthesis.cpp

@@ -71,6 +71,14 @@ 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_property_instance ||
+    expr.id() == ID_sva_sequence_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,20 @@ exprt verilog_typecheck_exprt::convert_symbol(
       result.add_source_location()=source_location;
       return result;
     }
+    else if(symbol->type.id() == ID_verilog_sva_sequence)
+    {
+      // A named sequence. Use an instance expression.
+      expr.type() = symbol->type;
+      expr.set_identifier(symbol->name);
+      return sva_sequence_instance_exprt{expr, {}}.with_source_location(expr);
+    }
+    else if(symbol->type.id() == ID_verilog_sva_property)
+    {
+      // A named property. Use an instance expression.
+      expr.type() = symbol->type;
+      expr.set_identifier(symbol->name);
+      return sva_property_instance_exprt{expr, {}}.with_source_location(expr);
+    }
     else
     {
       expr.type()=symbol->type;