From 79dc900b11a0839d39b4505415a9dd898b81b0f3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 27 Nov 2025 11:09:47 -0800 Subject: [PATCH 1/2] Introduce verilog_sequence_property_declaration_baset This introduces a base class for verilog_sequence_declarationt and verilog_property_declarationt. --- src/verilog/verilog_expr.h | 79 ++++++++++++++++++++++++++----- src/verilog/verilog_typecheck.cpp | 4 +- 2 files changed, 70 insertions(+), 13 deletions(-) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 3859ae2d8..558618612 100644 --- a/src/verilog/verilog_expr.h +++ b/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(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,10 +2914,53 @@ 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(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(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(expr); } @@ -2912,30 +2968,29 @@ 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(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(); } }; @@ -2943,6 +2998,7 @@ 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(expr); } @@ -2950,6 +3006,7 @@ 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(expr); } diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index ee0a73619..b9ca421d3 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1802,8 +1802,8 @@ 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()); auto type = verilog_sva_property_typet{}; symbolt symbol{full_identifier, type, mode}; From e765ef22d4dd56dd2585395e6865d6f02222bca1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 27 Nov 2025 17:33:19 -0800 Subject: [PATCH 2/2] SVA: use declaration for sequence and property symbols SVA named sequences and properties are now stored using the full declaration, to enable support for ports. --- src/verilog/verilog_synthesis.cpp | 4 +++- src/verilog/verilog_typecheck.cpp | 8 ++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 0d19cbecb..3027b9203 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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) { diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index b9ca421d3..c4721b49f 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1805,14 +1805,14 @@ void verilog_typecheckt::convert_property_declaration( 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));