SystemVerilog: checking sequence and property declarations

regression/verilog/SVA/named_property1.sv

@@ -12,4 +12,6 @@ module main(input clk);
     x_is_ten
   endsequence
 
+  initial assert(some_sequence);
+
 endmodule

src/trans-netlist/trans_to_netlist.cpp

@@ -212,10 +212,10 @@ void convert_trans_to_netlistt::map_vars(
     if (symbol.is_property)
       return; // ignore properties
     else if(
-      symbol.type.id() == ID_verilog_sva_sequence ||
-      symbol.type.id() == ID_verilog_sva_property)
+      symbol.type.id() == ID_verilog_sva_named_sequence ||
+      symbol.type.id() == ID_verilog_sva_named_property)
     {
-      return; // ignore properties
+      return; // ignore sequence/property declarations
     }
     else if(
       symbol.type.id() == ID_natural || symbol.type.id() == ID_integer ||

src/verilog/sva_expr.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_expr.h>
 
+#include "verilog_expr.h"
 #include "verilog_types.h"
 
 /// 1800-2017 16.6 Boolean expressions
@@ -2048,17 +2049,19 @@ enum class sva_sequence_semanticst
 };
 
 /// a base class for both sequence and property instance expressions
-class sva_sequence_property_instance_exprt : public binary_exprt
+class sva_sequence_property_instance_exprt : public ternary_exprt
 {
 public:
   sva_sequence_property_instance_exprt(
     symbol_exprt _symbol,
-    exprt::operandst _arguments)
-    : binary_exprt{
-        _symbol,
+    exprt::operandst _arguments,
+    verilog_sequence_property_declaration_baset _declaration)
+    : ternary_exprt{
         ID_sva_sequence_property_instance,
+        std::move(_symbol),
         multi_ary_exprt{ID_arguments, std::move(_arguments), typet{}},
-        _symbol.type()}
+        std::move(_declaration),
+        typet{}}
   {
   }
 
@@ -2081,6 +2084,26 @@ class sva_sequence_property_instance_exprt : public binary_exprt
   {
     return op1().operands();
   }
+
+  verilog_sequence_property_declaration_baset &declaration()
+  {
+    return static_cast<verilog_sequence_property_declaration_baset &>(op2());
+  }
+
+  const verilog_sequence_property_declaration_baset &declaration() const
+  {
+    return static_cast<const verilog_sequence_property_declaration_baset &>(
+      op2());
+  }
+
+  /// Add the source location from \p other, if it has any.
+  sva_sequence_property_instance_exprt &&
+  with_source_location(const exprt &other) &&
+  {
+    if(other.source_location().is_not_nil())
+      add_source_location() = other.source_location();
+    return std::move(*this);
+  }
 };
 
 inline const sva_sequence_property_instance_exprt &

src/verilog/verilog_synthesis.cpp

@@ -74,10 +74,7 @@ exprt verilog_synthesist::synth_expr_rec(exprt expr, symbol_statet 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());
-    auto &declaration =
-      to_verilog_sequence_property_declaration_base(symbol.value);
-    return synth_expr(declaration.cond(), symbol_state);
+    return synth_expr(instance.declaration().cond(), symbol_state);
   }
   else if(expr.id() == ID_hierarchical_identifier)
   {

src/verilog/verilog_typecheck.cpp

@@ -1802,13 +1802,13 @@ void verilog_typecheckt::convert_property_declaration(
   auto base_name = declaration.base_name();
   auto full_identifier = hierarchical_identifier(base_name);
 
-  convert_sva(declaration.property());
-  require_sva_property(declaration.property());
-
+  // 1800-2017 F.4.1
+  // Typechecking of the property expression has to be delayed
+  // until the instance is known, owing to untyped ports.
   declaration.type() = verilog_sva_named_property_typet{};
 
   // The symbol uses the full declaration as value
-  auto type = verilog_sva_property_typet{};
+  auto type = verilog_sva_named_property_typet{};
   symbolt symbol{full_identifier, type, mode};
 
   symbol.module = module_identifier;
@@ -1838,14 +1838,14 @@ void verilog_typecheckt::convert_sequence_declaration(
   auto base_name = declaration.base_name();
   auto full_identifier = hierarchical_identifier(base_name);
 
-  auto &sequence = declaration.sequence();
-  convert_sva(sequence);
-  require_sva_sequence(sequence);
-
+  // 1800-2017 F.4.1
+  // Typechecking of the sequence expression has to be delayed
+  // until the instance is known, owing to untyped ports.
   declaration.type() = verilog_sva_named_sequence_typet{};
 
   // The symbol uses the full declaration as value
-  symbolt symbol{full_identifier, sequence.type(), mode};
+  auto type = verilog_sva_named_sequence_typet{};
+  symbolt symbol{full_identifier, type, mode};
 
   symbol.module = module_identifier;
   symbol.base_name = base_name;

src/verilog/verilog_typecheck_expr.cpp

@@ -1361,14 +1361,19 @@ exprt verilog_typecheck_exprt::convert_symbol(
       return result;
     }
     else if(
-      symbol->type.id() == ID_verilog_sva_sequence ||
-      symbol->type.id() == ID_verilog_sva_property)
+      symbol->type.id() == ID_verilog_sva_named_sequence ||
+      symbol->type.id() == ID_verilog_sva_named_property)
     {
-      // A named sequence or property. Use an instance expression.
+      // A named sequence or property. Create an instance expression,
+      // and then flatten it.
       expr.type() = symbol->type;
       expr.set_identifier(symbol->name);
-      return sva_sequence_property_instance_exprt{expr, {}}
-        .with_source_location(expr);
+      auto &declaration =
+        to_verilog_sequence_property_declaration_base(symbol->value);
+      auto instance =
+        sva_sequence_property_instance_exprt{expr, {}, declaration}
+          .with_source_location(expr);
+      return flatten_named_sequence_property(instance);
     }
     else
     {

src/verilog/verilog_typecheck_expr.h

@@ -212,6 +212,8 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
   [[nodiscard]] exprt convert_binary_sva(binary_exprt);
   [[nodiscard]] exprt convert_ternary_sva(ternary_exprt);
   [[nodiscard]] exprt convert_other_sva(exprt);
+  [[nodiscard]] exprt
+    flatten_named_sequence_property(sva_sequence_property_instance_exprt);
 
   // system functions
   exprt bits(const exprt &);

src/verilog/verilog_typecheck_sva.cpp

@@ -493,3 +493,26 @@ exprt verilog_typecheck_exprt::convert_sva_rec(exprt expr)
     return convert_other_sva(expr);
   }
 }
+
+/// 1800-2017 F.4.1
+exprt verilog_typecheck_exprt::flatten_named_sequence_property(
+  sva_sequence_property_instance_exprt instance)
+{
+  auto &cond = instance.declaration().cond();
+  convert_sva(cond);
+
+  if(instance.symbol().type().id() == ID_verilog_sva_named_sequence)
+  {
+    require_sva_sequence(cond);
+    instance.type() = verilog_sva_sequence_typet{};
+  }
+  else if(instance.symbol().type().id() == ID_verilog_sva_named_property)
+  {
+    require_sva_property(cond);
+    instance.type() = verilog_sva_property_typet{};
+  }
+  else
+    PRECONDITION(false);
+
+  return instance;
+}