From 939438f5e406ad45d0a6b5281f2435ed48ea95bf Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 29 Nov 2025 12:25:44 -0800 Subject: [PATCH] SystemVerilog: checking sequence and property declarations 1800-2017 F.4.1 gives a rewriting algorithm for sequence and property declarations, to be applied when the instance is known. This delays typechecking of sequence and property declarations until the declaration is instantiated. --- regression/verilog/SVA/named_property1.sv | 2 ++ src/trans-netlist/trans_to_netlist.cpp | 6 ++--- src/verilog/sva_expr.h | 33 +++++++++++++++++++---- src/verilog/verilog_synthesis.cpp | 5 +--- src/verilog/verilog_typecheck.cpp | 18 ++++++------- src/verilog/verilog_typecheck_expr.cpp | 15 +++++++---- src/verilog/verilog_typecheck_expr.h | 2 ++ src/verilog/verilog_typecheck_sva.cpp | 23 ++++++++++++++++ 8 files changed, 78 insertions(+), 26 deletions(-) diff --git a/regression/verilog/SVA/named_property1.sv b/regression/verilog/SVA/named_property1.sv index 489055b30..30db7d9fb 100644 --- a/regression/verilog/SVA/named_property1.sv +++ b/regression/verilog/SVA/named_property1.sv @@ -12,4 +12,6 @@ module main(input clk); x_is_ten endsequence + initial assert(some_sequence); + endmodule diff --git a/src/trans-netlist/trans_to_netlist.cpp b/src/trans-netlist/trans_to_netlist.cpp index 7a2f326d9..5801ca948 100644 --- a/src/trans-netlist/trans_to_netlist.cpp +++ b/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 || diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index dbeab7e4c..2c4414a62 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#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(op2()); + } + + const verilog_sequence_property_declaration_baset &declaration() const + { + return static_cast( + 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 & diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 3027b9203..83c81c150 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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) { diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 870f6f046..60c74ec5b 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/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; diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index a74d61420..9076e7aba 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/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 { diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 391315e7b..59a4fdcc1 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/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 &); diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 777cf445c..fe11ef692 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/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; +}