From 1450fbc6f76156d9819af043336d89299030e76a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 24 Nov 2025 19:34:13 -0800 Subject: [PATCH] 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. --- src/hw_cbmc_irep_ids.h | 1 + src/verilog/expr2verilog.cpp | 45 ++++++++++++++++++++++ src/verilog/expr2verilog_class.h | 4 ++ src/verilog/sva_expr.h | 52 ++++++++++++++++++++++++++ src/verilog/verilog_synthesis.cpp | 6 +++ src/verilog/verilog_typecheck_expr.cpp | 10 +++++ 6 files changed, 118 insertions(+) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 15011d03d..a48dbb9ea 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -80,6 +80,7 @@ IREP_ID_ONE(sva_sequence_goto_repetition) IREP_ID_ONE(sva_sequence_intersect) IREP_ID_ONE(sva_sequence_non_consecutive_repetition) IREP_ID_ONE(sva_sequence_property) +IREP_ID_ONE(sva_sequence_property_instance) IREP_ID_ONE(sva_sequence_repetition_star) IREP_ID_ONE(sva_sequence_repetition_plus) IREP_ID_ONE(sva_sequence_throughout) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 7bacf2ed0..1d03ba284 100644 --- a/src/verilog/expr2verilog.cpp +++ b/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,12 @@ 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_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); } diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 77ad41adb..3a32e13d6 100644 --- a/src/verilog/expr2verilog_class.h +++ b/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; }; diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 8e3baa35b..dbeab7e4c 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -2047,4 +2047,56 @@ 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( + symbol_exprt _symbol, + exprt::operandst _arguments) + : binary_exprt{ + _symbol, + ID_sva_sequence_property_instance, + multi_ary_exprt{ID_arguments, std::move(_arguments), typet{}}, + _symbol.type()} + { + } + + const symbol_exprt &symbol() const + { + return static_cast(op0()); + } + + symbol_exprt &symbol() + { + return static_cast(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_property_instance); + sva_sequence_property_instance_exprt::check(expr); + return static_cast(expr); +} + +inline sva_sequence_property_instance_exprt & +to_sva_sequence_property_instance_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_property_instance); + sva_sequence_property_instance_exprt::check(expr); + return static_cast(expr); +} + #endif diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 45448b48c..0d19cbecb 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -71,6 +71,12 @@ 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_sequence_property_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( diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index a7f128323..a74d61420 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1360,6 +1360,16 @@ exprt verilog_typecheck_exprt::convert_symbol( result.add_source_location()=source_location; return result; } + else if( + symbol->type.id() == ID_verilog_sva_sequence || + symbol->type.id() == ID_verilog_sva_property) + { + // A named sequence or property. Use an instance expression. + expr.type() = symbol->type; + expr.set_identifier(symbol->name); + return sva_sequence_property_instance_exprt{expr, {}} + .with_source_location(expr); + } else { expr.type()=symbol->type;