From 649411d55d93a64c9da057a831858b9e1cf5b883 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 23 Apr 2025 08:03:55 -0700 Subject: [PATCH] Introduce sva_sequence_repetition_exprt This introduces sva_sequence_repetition_exprt as a base class for the SVA repetition operators [*...], [=...], [->...]. --- src/verilog/expr2verilog.cpp | 64 ++++------ src/verilog/expr2verilog_class.h | 10 +- src/verilog/parser.y | 20 ++- src/verilog/sva_expr.cpp | 10 +- src/verilog/sva_expr.h | 175 ++++++++++++++------------ src/verilog/verilog_typecheck_sva.cpp | 53 ++++---- 6 files changed, 170 insertions(+), 162 deletions(-) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index e050ff21e..ba93e737f 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -608,31 +608,6 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary( /*******************************************************************\ -Function: expr2verilogt::convert_sva_binary_repetition - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -expr2verilogt::resultt expr2verilogt::convert_sva_binary_repetition( - const std::string &name, - const binary_exprt &expr) -{ - auto op0 = convert_rec(expr.lhs()); - if(op0.p == verilog_precedencet::MIN) - op0.s = "(" + op0.s + ")"; - - auto op1 = convert_rec(expr.rhs()); - - return {verilog_precedencet::MIN, op0.s + " " + name + op1.s + "]"}; -} - -/*******************************************************************\ - Function: expr2verilogt::convert_sva_sequence_consecutive_repetition Inputs: @@ -643,20 +618,27 @@ Function: expr2verilogt::convert_sva_sequence_consecutive_repetition \*******************************************************************/ -expr2verilogt::resultt -expr2verilogt::convert_sva_sequence_consecutive_repetition( - const sva_sequence_consecutive_repetition_exprt &expr) +expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition( + const std::string &name, + const sva_sequence_repetition_exprt &expr) { auto op = convert_rec(expr.op()); if(op.p == verilog_precedencet::MIN) op.s = "(" + op.s + ")"; - std::string dest = op.s + " [*" + convert_rec(expr.from()).s; + std::string dest = op.s + " [" + name; + + if(expr.is_range()) + { + dest += convert_rec(expr.from()).s; - if(expr.is_unbounded()) - dest += ":$"; - else if(expr.to().is_not_nil()) - dest += ":" + convert_rec(expr.to()).s; + if(expr.is_unbounded()) + dest += ":$"; + else + dest += ":" + convert_rec(expr.to()).s; + } + else + dest += convert_rec(expr.repetitions()).s; dest += ']'; @@ -1877,20 +1859,16 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) // not sure about precedence else if(src.id() == ID_sva_sequence_non_consecutive_repetition) - return precedence = verilog_precedencet::MIN, - convert_sva_binary_repetition( - "[=", to_sva_sequence_non_consecutive_repetition_expr(src)); - // not sure about precedence + return convert_sva_sequence_repetition( + "=", to_sva_sequence_non_consecutive_repetition_expr(src)); else if(src.id() == ID_sva_sequence_consecutive_repetition) - return convert_sva_sequence_consecutive_repetition( - to_sva_sequence_consecutive_repetition_expr(src)); + return convert_sva_sequence_repetition( + "*", to_sva_sequence_consecutive_repetition_expr(src)); else if(src.id() == ID_sva_sequence_goto_repetition) - return precedence = verilog_precedencet::MIN, - convert_sva_binary_repetition( - "[->", to_sva_sequence_goto_repetition_expr(src)); - // not sure about precedence + return convert_sva_sequence_repetition( + "->", to_sva_sequence_goto_repetition_expr(src)); else if(src.id() == ID_sva_ranged_always) { diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index a54808d60..3a41c2b55 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -16,7 +16,7 @@ class sva_abort_exprt; class sva_case_exprt; class sva_if_exprt; class sva_ranged_predicate_exprt; -class sva_sequence_consecutive_repetition_exprt; +class sva_sequence_repetition_exprt; class sva_sequence_first_match_exprt; // Precedences (higher means binds more strongly). @@ -137,11 +137,9 @@ class expr2verilogt resultt convert_sva_binary(const std::string &name, const binary_exprt &); - resultt - convert_sva_binary_repetition(const std::string &name, const binary_exprt &); - - resultt convert_sva_sequence_consecutive_repetition( - const sva_sequence_consecutive_repetition_exprt &); + resultt convert_sva_sequence_repetition( + const std::string &name, + const sva_sequence_repetition_exprt &); resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index a60e14803..16fdba2cc 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2707,12 +2707,28 @@ consecutive_repetition: non_consecutive_repetition: "[=" const_or_range_expression ']' - { init($$, ID_sva_sequence_non_consecutive_repetition); mto($$, $2); } + { init($$, ID_sva_sequence_non_consecutive_repetition); + if(stack_expr($2).id() == ID_sva_cycle_delay) + swapop($$, $2); + else + { + mto($$, $2); + stack_expr($$).add_to_operands(nil_exprt{}); + } + } ; goto_repetition: "[->" const_or_range_expression ']' - { init($$, ID_sva_sequence_goto_repetition); mto($$, $2); } + { init($$, ID_sva_sequence_goto_repetition); + if(stack_expr($2).id() == ID_sva_cycle_delay) + swapop($$, $2); + else + { + mto($$, $2); + stack_expr($$).add_to_operands(nil_exprt{}); + } + } ; cycle_delay_range: diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp index 81a1bac13..37d5ad2f6 100644 --- a/src/verilog/sva_expr.cpp +++ b/src/verilog/sva_expr.cpp @@ -62,10 +62,10 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const PRECONDITION( op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence); - if(to().is_nil()) + if(!is_range()) { // expand x[*n] into x ##1 x ##1 ... - auto n = numeric_cast_v(to_constant_expr(from())); + auto n = numeric_cast_v(repetitions()); DATA_INVARIANT(n >= 1, "number of repetitions must be at least one"); exprt result = op(); @@ -84,11 +84,11 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const { PRECONDITION(false); } - else + else // bounded range { // expand x[*a:b] into x[*a] or x[*a+1] or ... or x[*b] - auto from_int = numeric_cast_v(to_constant_expr(from())); - auto to_int = numeric_cast_v(to_constant_expr(to())); + auto from_int = numeric_cast_v(from()); + auto to_int = numeric_cast_v(to()); DATA_INVARIANT(from_int >= 1, "number of repetitions must be at least one"); DATA_INVARIANT( diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 814a2637d..de8b68f83 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1290,12 +1290,17 @@ inline sva_case_exprt &to_sva_case_expr(exprt &expr) return static_cast(expr); } -class sva_sequence_consecutive_repetition_exprt : public ternary_exprt +/// Base class for [->...], [*...], [=...] +/// The ... constraint may be x, x:y, x:$ +class sva_sequence_repetition_exprt : public ternary_exprt { public: - sva_sequence_consecutive_repetition_exprt(exprt __op, exprt __repetitions) + sva_sequence_repetition_exprt( + exprt __op, + irep_idt __id, + constant_exprt __repetitions) : ternary_exprt{ - ID_sva_sequence_consecutive_repetition, + __id, std::move(__op), std::move(__repetitions), nil_exprt{}, @@ -1303,12 +1308,13 @@ class sva_sequence_consecutive_repetition_exprt : public ternary_exprt { } - sva_sequence_consecutive_repetition_exprt( + sva_sequence_repetition_exprt( exprt __op, - exprt __from, - exprt __to) + irep_idt __id, + constant_exprt __from, + constant_exprt __to) : ternary_exprt{ - ID_sva_sequence_consecutive_repetition, + __id, std::move(__op), std::move(__from), std::move(__to), @@ -1316,8 +1322,7 @@ class sva_sequence_consecutive_repetition_exprt : public ternary_exprt { } - exprt lower() const; - + // May be a sequence for [*...], Boolean otherwise const exprt &op() const { return op0(); @@ -1328,31 +1333,51 @@ class sva_sequence_consecutive_repetition_exprt : public ternary_exprt return op0(); } - const exprt &from() const + // The number of repetitions must be a constant after elaboration. + const constant_exprt &repetitions() const { - return op1(); + PRECONDITION(!is_range()); + return static_cast(op1()); } - exprt &from() + constant_exprt &repetitions() { - return op1(); + PRECONDITION(!is_range()); + return static_cast(op1()); } - // may be nil (just the singleton 'from') or - // infinity (half-open interval starting at 'from') - const exprt &to() const + bool is_range() const { - return op2(); + return op2().is_not_nil(); } - exprt &to() + bool is_unbounded() const { - return op2(); + return op2().id() == ID_infinity; } - bool is_unbounded() const + const constant_exprt &from() const { - return to().id() == ID_infinity; + PRECONDITION(is_range()); + return static_cast(op1()); + } + + constant_exprt &from() + { + PRECONDITION(is_range()); + return static_cast(op1()); + } + + const constant_exprt &to() const + { + PRECONDITION(is_range() && !is_unbounded()); + return static_cast(op2()); + } + + constant_exprt &to() + { + PRECONDITION(is_range() && !is_unbounded()); + return static_cast(op2()); } protected: @@ -1361,6 +1386,49 @@ class sva_sequence_consecutive_repetition_exprt : public ternary_exprt using ternary_exprt::op2; }; +inline const sva_sequence_repetition_exprt & +to_sva_sequence_repetition_expr(const exprt &expr) +{ + sva_sequence_repetition_exprt::check(expr); + return static_cast(expr); +} + +inline sva_sequence_repetition_exprt & +to_sva_sequence_repetition_expr(exprt &expr) +{ + sva_sequence_repetition_exprt::check(expr); + return static_cast(expr); +} + +class sva_sequence_consecutive_repetition_exprt + : public sva_sequence_repetition_exprt +{ +public: + sva_sequence_consecutive_repetition_exprt( + exprt __op, + constant_exprt __repetitions) + : sva_sequence_repetition_exprt{ + std::move(__op), + ID_sva_sequence_consecutive_repetition, + std::move(__repetitions)} + { + } + + sva_sequence_consecutive_repetition_exprt( + exprt __op, + constant_exprt __from, + constant_exprt __to) + : sva_sequence_repetition_exprt{ + std::move(__op), + ID_sva_sequence_consecutive_repetition, + std::move(__from), + std::move(__to)} + { + } + + exprt lower() const; +}; + inline const sva_sequence_consecutive_repetition_exprt & to_sva_sequence_consecutive_repetition_expr(const exprt &expr) { @@ -1377,42 +1445,16 @@ to_sva_sequence_consecutive_repetition_expr(exprt &expr) return static_cast(expr); } -class sva_sequence_goto_repetition_exprt : public binary_exprt +class sva_sequence_goto_repetition_exprt : public sva_sequence_repetition_exprt { public: sva_sequence_goto_repetition_exprt(exprt __op, constant_exprt __repetitions) - : binary_exprt{ + : sva_sequence_repetition_exprt{ std::move(__op), ID_sva_sequence_goto_repetition, - std::move(__repetitions), - verilog_sva_sequence_typet{}} - { - } - - const exprt &op() const - { - return op0(); - } - - exprt &op() - { - return op0(); - } - - // The number of repetitions must be a constant after elaboration. - const constant_exprt &repetitions() const - { - return static_cast(op1()); - } - - constant_exprt &repetitions() + std::move(__repetitions)} { - return static_cast(op1()); } - -protected: - using binary_exprt::op0; - using binary_exprt::op1; }; inline const sva_sequence_goto_repetition_exprt & @@ -1431,44 +1473,19 @@ to_sva_sequence_goto_repetition_expr(exprt &expr) return static_cast(expr); } -class sva_sequence_non_consecutive_repetition_exprt : public binary_exprt +class sva_sequence_non_consecutive_repetition_exprt + : public sva_sequence_repetition_exprt { public: sva_sequence_non_consecutive_repetition_exprt( exprt __op, constant_exprt __repetitions) - : binary_exprt{ + : sva_sequence_repetition_exprt{ std::move(__op), ID_sva_sequence_non_consecutive_repetition, - std::move(__repetitions), - verilog_sva_sequence_typet{}} + std::move(__repetitions)} { } - - const exprt &op() const - { - return op0(); - } - - exprt &op() - { - return op0(); - } - - // The number of repetitions must be a constant after elaboration. - const constant_exprt &repetitions() const - { - return static_cast(op1()); - } - - constant_exprt &repetitions() - { - return static_cast(op1()); - } - -protected: - using binary_exprt::op0; - using binary_exprt::op1; }; inline const sva_sequence_non_consecutive_repetition_exprt & diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index cf6f0785c..4abe8adf0 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -270,26 +270,6 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) return std::move(expr); } - else if( - expr.id() == ID_sva_sequence_non_consecutive_repetition || - expr.id() == ID_sva_sequence_goto_repetition) - { - convert_sva(expr.lhs()); - require_sva_sequence(expr.lhs()); - - convert_expr(expr.rhs()); - - mp_integer n = elaborate_constant_integer_expression(expr.rhs()); - if(n < 0) - throw errort().with_location(expr.rhs().source_location()) - << "number of repetitions must not be negative"; - - expr.rhs() = from_integer(n, integer_typet{}); - - expr.type() = verilog_sva_sequence_typet{}; - - return std::move(expr); - } else if(expr.id() == ID_sva_case) { auto &case_expr = to_sva_case_expr(expr); @@ -341,22 +321,41 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr) } else if(expr.id() == ID_sva_sequence_consecutive_repetition) // x[*1:2] { - auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr); - // This expression takes a sequence as argument. // The grammar allows properties to implement and/or over // sequences. Check here that the argument is a sequence. - convert_sva(repetition.op()); - require_sva_sequence(repetition.op()); + convert_sva(expr.op0()); + require_sva_sequence(expr.op0()); - convert_expr(repetition.from()); + convert_expr(expr.op1()); - if(repetition.to().is_not_nil()) - convert_expr(repetition.to()); + if(expr.op2().is_not_nil()) + convert_expr(expr.op2()); expr.type() = verilog_sva_sequence_typet{}; return std::move(expr); } + else if( + expr.id() == ID_sva_sequence_non_consecutive_repetition || + expr.id() == ID_sva_sequence_goto_repetition) + { + // These take a Boolean as argument. + convert_expr(expr.op0()); + make_boolean(expr.op0()); + + convert_expr(expr.op1()); + + mp_integer n = elaborate_constant_integer_expression(expr.op1()); + if(n < 0) + throw errort().with_location(expr.op1().source_location()) + << "number of repetitions must not be negative"; + + expr.op1() = from_integer(n, integer_typet{}); + + expr.type() = verilog_sva_sequence_typet{}; + + return std::move(expr); + } else if( expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_s_eventually || expr.id() == ID_sva_s_always || expr.id() == ID_sva_ranged_always)