From 2555bf0387f3d236f58d64f6b8eb843a94b55845 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 11 Apr 2025 12:00:30 -0400 Subject: [PATCH] sva_sequence_property_expr_baset This introduces sva_sequence_property_expr_baset, to serve as a base class for sva_weak_exprt, sva_strong_exprt, and sva_sequence_property_exprt. --- src/temporal-logic/trivial_sva.cpp | 2 +- src/trans-word-level/property.cpp | 25 +++---------- src/verilog/expr2verilog.cpp | 5 +-- src/verilog/sva_expr.h | 58 +++++++++++++++++++++++++----- 4 files changed, 58 insertions(+), 32 deletions(-) diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp index 857a46ad..13aca48a 100644 --- a/src/temporal-logic/trivial_sva.cpp +++ b/src/temporal-logic/trivial_sva.cpp @@ -111,7 +111,7 @@ exprt trivial_sva(exprt expr) { // We simplify sequences to boolean expressions, and hence can drop // the sva_sequence_property converter - auto &op = to_sva_sequence_property_expr(expr).op(); + auto &op = to_sva_sequence_property_expr(expr).sequence(); if(op.type().id() == ID_bool) return op; } diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 9356d03d..d2f2f61f 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -507,25 +507,6 @@ static obligationst property_obligations_rec( std::max(obligations_true.first, obligations_false.first), if_exprt{cond, obligations_true.second, obligations_false.second}}; } - else if(property_expr.id() == ID_sva_sequence_property) - { - // Sequences can be used as property, and evaluate to true - // when there is at least one match. - auto &sequence = to_sva_sequence_property_expr(property_expr).op(); - auto matches = instantiate_sequence(sequence, current, no_timeframes); - - exprt::operandst disjuncts; - disjuncts.reserve(matches.size()); - mp_integer max = current; - - for(auto &match : matches) - { - disjuncts.push_back(match.condition); - max = std::max(max, match.end_time); - } - - return obligationst{max, disjunction(disjuncts)}; - } else if( property_expr.id() == ID_typecast && to_typecast_expr(property_expr).op().type().id() == ID_bool) @@ -665,9 +646,11 @@ static obligationst property_obligations_rec( return obligationst{t, disjunction(disjuncts)}; } else if( - property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak) + property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak || + property_expr.id() == ID_sva_sequence_property) { - auto &sequence = to_unary_expr(property_expr).op(); + auto &sequence = + to_sva_sequence_property_expr_base(property_expr).sequence(); // sequence expressions -- these may have multiple potential // match points, and evaluate to true if any of them matches diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index aea99bab..2ccb0b15 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -537,7 +537,8 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary( if(op.id() == ID_typecast) op_operands = to_typecast_expr(op).op().operands().size(); else if(src.op().id() == ID_sva_sequence_property) - op_operands = to_sva_sequence_property_expr(op).op().operands().size(); + op_operands = + to_sva_sequence_property_expr(op).sequence().operands().size(); else op_operands = op.operands().size(); @@ -1816,7 +1817,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return convert_function("weak", src); else if(src.id() == ID_sva_sequence_property) - return convert_rec(to_sva_sequence_property_expr(src).op()); + return convert_rec(to_sva_sequence_property_expr(src).sequence()); else if(src.id()==ID_sva_sequence_concatenation) return convert_sva_sequence_concatenation( diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 45af75d0..c8bb9186 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1111,44 +1111,86 @@ static inline sva_if_exprt &to_sva_if_expr(exprt &expr) return static_cast(expr); } -class sva_strong_exprt : public unary_exprt +/// Base class for sequence property expressions. +/// 1800-2017 16.12.2 Sequence property +class sva_sequence_property_expr_baset : public unary_predicate_exprt +{ +public: + sva_sequence_property_expr_baset(irep_idt __id, exprt __op) + : unary_predicate_exprt(__id, std::move(__op)) + { + } + + const exprt &sequence() const + { + return op(); + } + + exprt &sequence() + { + return op(); + } + +protected: + using unary_predicate_exprt::op; +}; + +inline const sva_sequence_property_expr_baset & +to_sva_sequence_property_expr_base(const exprt &expr) +{ + sva_sequence_property_expr_baset::check(expr); + return static_cast(expr); +} + +inline sva_sequence_property_expr_baset & +to_sva_sequence_property_base_expr(exprt &expr) +{ + sva_sequence_property_expr_baset::check(expr); + return static_cast(expr); +} + +class sva_strong_exprt : public sva_sequence_property_expr_baset { public: - sva_strong_exprt(exprt __op, typet __type) - : unary_exprt(ID_sva_strong, std::move(__op), std::move(__type)) + sva_strong_exprt(exprt __op) + : sva_sequence_property_expr_baset(ID_sva_strong, std::move(__op)) { } }; inline const sva_strong_exprt &to_sva_strong_expr(const exprt &expr) { + PRECONDITION(expr.id() == ID_sva_strong); sva_strong_exprt::check(expr); return static_cast(expr); } inline sva_strong_exprt &to_sva_strong_expr(exprt &expr) { + PRECONDITION(expr.id() == ID_sva_strong); sva_strong_exprt::check(expr); return static_cast(expr); } -class sva_weak_exprt : public unary_exprt +class sva_weak_exprt : public sva_sequence_property_expr_baset { public: - sva_weak_exprt(exprt __op, typet __type) - : unary_exprt(ID_sva_weak, std::move(__op), std::move(__type)) + sva_weak_exprt(exprt __op) + : sva_sequence_property_expr_baset(ID_sva_weak, std::move(__op)) { } }; inline const sva_weak_exprt &to_sva_weak_expr(const exprt &expr) { + PRECONDITION(expr.id() == ID_sva_weak); sva_weak_exprt::check(expr); return static_cast(expr); } inline sva_weak_exprt &to_sva_weak_expr(exprt &expr) { + PRECONDITION(expr.id() == ID_sva_weak); sva_weak_exprt::check(expr); return static_cast(expr); } @@ -1517,11 +1559,11 @@ to_sva_sequence_first_match_expr(exprt &expr) /// 1800-2017 16.12.2 Sequence property /// Equivalent to weak(...) or strong(...) depending on context. -class sva_sequence_property_exprt : public unary_predicate_exprt +class sva_sequence_property_exprt : public sva_sequence_property_expr_baset { public: explicit sva_sequence_property_exprt(exprt op) - : unary_predicate_exprt(ID_sva_sequence_property, std::move(op)) + : sva_sequence_property_expr_baset(ID_sva_sequence_property, std::move(op)) { } };