SVA: use declaration for sequence and property symbols

src/verilog/verilog_expr.h

@@ -393,6 +393,12 @@ class verilog_module_itemt:public exprt
   inline verilog_module_itemt()
   {
   }
+
+  static void
+  check(const exprt &expr, validation_modet vm = validation_modet::INVARIANT)
+  {
+    exprt::check(expr, vm);
+  }
 };
 
 inline const verilog_module_itemt &to_verilog_module_item(const irept &irep)
@@ -2882,9 +2888,16 @@ to_verilog_indexed_part_select_plus_or_minus_expr(exprt &expr)
   return static_cast<verilog_indexed_part_select_plus_or_minus_exprt &>(expr);
 }
 
-class verilog_property_declarationt : public verilog_module_itemt
+/// a base class for both sequence and property declarations
+class verilog_sequence_property_declaration_baset : public verilog_module_itemt
 {
 public:
+  verilog_sequence_property_declaration_baset(irep_idt _id, exprt _cond)
+    : verilog_module_itemt{_id}
+  {
+    add_to_operands(std::move(_cond));
+  }
+
   const irep_idt &base_name() const
   {
     return get(ID_base_name);
@@ -2901,55 +2914,99 @@ class verilog_property_declarationt : public verilog_module_itemt
   }
 };
 
+inline const verilog_sequence_property_declaration_baset &
+to_verilog_sequence_property_declaration_base(const exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_verilog_sequence_declaration ||
+    expr.id() == ID_verilog_property_declaration);
+  verilog_sequence_property_declaration_baset::check(expr);
+  return static_cast<const verilog_sequence_property_declaration_baset &>(expr);
+}
+
+inline verilog_sequence_property_declaration_baset &
+to_verilog_sequence_property_declaration_base(exprt &expr)
+{
+  PRECONDITION(
+    expr.id() == ID_verilog_sequence_declaration ||
+    expr.id() == ID_verilog_property_declaration);
+  verilog_sequence_property_declaration_baset::check(expr);
+  return static_cast<verilog_sequence_property_declaration_baset &>(expr);
+}
+
+class verilog_property_declarationt
+  : public verilog_sequence_property_declaration_baset
+{
+public:
+  explicit verilog_property_declarationt(exprt property)
+    : verilog_sequence_property_declaration_baset{
+        ID_verilog_property_declaration,
+        std::move(property)}
+  {
+  }
+
+  const exprt &property() const
+  {
+    return cond();
+  }
+
+  exprt &property()
+  {
+    return cond();
+  }
+};
+
 inline const verilog_property_declarationt &
 to_verilog_property_declaration(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_verilog_property_declaration);
+  verilog_property_declarationt::check(expr);
   return static_cast<const verilog_property_declarationt &>(expr);
 }
 
 inline verilog_property_declarationt &
 to_verilog_property_declaration(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_verilog_property_declaration);
+  verilog_property_declarationt::check(expr);
   return static_cast<verilog_property_declarationt &>(expr);
 }
 
-class verilog_sequence_declarationt : public verilog_module_itemt
+class verilog_sequence_declarationt
+  : public verilog_sequence_property_declaration_baset
 {
 public:
-  explicit verilog_sequence_declarationt(exprt sequence)
-  {
-    add_to_operands(std::move(sequence));
-  }
-
-  const irep_idt &base_name() const
+  explicit verilog_sequence_declarationt(exprt _sequence)
+    : verilog_sequence_property_declaration_baset{
+        ID_verilog_sequence_declaration,
+        std::move(_sequence)}
   {
-    return get(ID_base_name);
   }
 
   const exprt &sequence() const
   {
-    return op0();
+    return cond();
   }
 
   exprt &sequence()
   {
-    return op0();
+    return cond();
   }
 };
 
 inline const verilog_sequence_declarationt &
 to_verilog_sequence_declaration(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
+  verilog_sequence_declarationt::check(expr);
   return static_cast<const verilog_sequence_declarationt &>(expr);
 }
 
 inline verilog_sequence_declarationt &
 to_verilog_sequence_declaration(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_verilog_sequence_declaration);
+  verilog_sequence_declarationt::check(expr);
   return static_cast<verilog_sequence_declarationt &>(expr);
 }
 

src/verilog/verilog_synthesis.cpp

@@ -75,7 +75,9 @@ exprt verilog_synthesist::synth_expr_rec(exprt expr, symbol_statet symbol_state)
   {
     auto &instance = to_sva_sequence_property_instance_expr(expr);
     const symbolt &symbol = ns.lookup(instance.symbol());
-    return synth_expr(symbol.value, symbol_state);
+    auto &declaration =
+      to_verilog_sequence_property_declaration_base(symbol.value);
+    return synth_expr(declaration.cond(), symbol_state);
   }
   else if(expr.id() == ID_hierarchical_identifier)
   {

src/verilog/verilog_typecheck.cpp

@@ -1802,17 +1802,17 @@ void verilog_typecheckt::convert_property_declaration(
   auto base_name = declaration.base_name();
   auto full_identifier = hierarchical_identifier(base_name);
 
-  convert_sva(declaration.cond());
-  require_sva_property(declaration.cond());
+  convert_sva(declaration.property());
+  require_sva_property(declaration.property());
 
+  // The symbol uses the full declaration as value
   auto type = verilog_sva_property_typet{};
   symbolt symbol{full_identifier, type, mode};
 
   symbol.module = module_identifier;
   symbol.base_name = base_name;
   symbol.pretty_name = strip_verilog_prefix(symbol.name);
-  symbol.is_macro = true;
-  symbol.value = declaration.cond();
+  symbol.value = declaration;
   symbol.location = declaration.source_location();
 
   add_symbol(std::move(symbol));
@@ -1840,13 +1840,13 @@ void verilog_typecheckt::convert_sequence_declaration(
   convert_sva(sequence);
   require_sva_sequence(sequence);
 
+  // The symbol uses the full declaration as value
   symbolt symbol{full_identifier, sequence.type(), mode};
 
   symbol.module = module_identifier;
   symbol.base_name = base_name;
   symbol.pretty_name = strip_verilog_prefix(symbol.name);
-  symbol.is_macro = true;
-  symbol.value = declaration.sequence();
+  symbol.value = declaration;
   symbol.location = declaration.source_location();
 
   add_symbol(std::move(symbol));