From 7e3d3bb91b9601194bbe1096636ca68960e97f3d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 14 Sep 2024 14:28:59 -0700 Subject: [PATCH] SVA: sva_indexed_nexttime_exprt and sva_indexed_s_nexttime_exprt This is to match the pattern used by the ranged and nonranged variants for SVA always and eventually. --- src/hw_cbmc_irep_ids.h | 2 + src/temporal-logic/normalize_property.cpp | 26 +++--- src/verilog/expr2verilog.cpp | 17 +++- src/verilog/parser.y | 8 +- src/verilog/sva_expr.h | 107 +++++++++++++++------- src/verilog/verilog_typecheck_expr.cpp | 17 ++-- 6 files changed, 117 insertions(+), 60 deletions(-) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index c8343a7a0..cf3a9d3f0 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -43,7 +43,9 @@ IREP_ID_ONE(sva_s_always) IREP_ID_ONE(sva_assume) IREP_ID_ONE(sva_cover) IREP_ID_ONE(sva_nexttime) +IREP_ID_ONE(sva_indexed_nexttime) IREP_ID_ONE(sva_s_nexttime) +IREP_ID_ONE(sva_indexed_s_nexttime) IREP_ID_ONE(sva_eventually) IREP_ID_ONE(sva_s_eventually) IREP_ID_ONE(sva_until) diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index a956cd0df..7f2c68978 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -171,21 +171,23 @@ exprt normalize_property(exprt expr) expr = normalize_pre_sva_or(to_sva_or_expr(expr)); else if(expr.id() == ID_sva_nexttime) { - auto &nexttime_expr = to_sva_nexttime_expr(expr); - if(nexttime_expr.is_indexed()) - expr = sva_ranged_always_exprt{ - nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; - else - expr = X_exprt{nexttime_expr.op()}; + expr = X_exprt{to_sva_nexttime_expr(expr).op()}; } else if(expr.id() == ID_sva_s_nexttime) { - auto &nexttime_expr = to_sva_s_nexttime_expr(expr); - if(nexttime_expr.is_indexed()) - expr = sva_s_always_exprt{ - nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; - else - expr = X_exprt{to_sva_s_nexttime_expr(expr).op()}; + expr = X_exprt{to_sva_s_nexttime_expr(expr).op()}; + } + else if(expr.id() == ID_sva_indexed_nexttime) + { + auto &nexttime_expr = to_sva_indexed_nexttime_expr(expr); + expr = sva_ranged_always_exprt{ + nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; + } + else if(expr.id() == ID_sva_indexed_s_nexttime) + { + auto &nexttime_expr = to_sva_indexed_s_nexttime_expr(expr); + expr = sva_s_always_exprt{ + nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; } else if(expr.id() == ID_sva_cycle_delay) expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr)); diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 8a8d71971..b30dcdc8b 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1499,16 +1499,25 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) else if(src.id()==ID_sva_nexttime) return precedence = verilog_precedencet::MIN, - convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src)); + convert_sva_unary("nexttime", to_sva_nexttime_expr(src)); - else if(src.id() == ID_sva_disable_iff) + else if(src.id() == ID_sva_indexed_nexttime) return precedence = verilog_precedencet::MIN, - convert_sva_abort("disable iff", to_sva_abort_expr(src)); + convert_sva_indexed_binary( + "nexttime", to_sva_indexed_nexttime_expr(src)); else if(src.id()==ID_sva_s_nexttime) + return precedence = verilog_precedencet::MIN, + convert_sva_unary("s_nexttime", to_sva_s_nexttime_expr(src)); + + else if(src.id() == ID_sva_indexed_s_nexttime) return precedence = verilog_precedencet::MIN, convert_sva_indexed_binary( - "s_nexttime", to_sva_s_nexttime_expr(src)); + "s_nexttime", to_sva_indexed_s_nexttime_expr(src)); + + else if(src.id() == ID_sva_disable_iff) + return precedence = verilog_precedencet::MIN, + convert_sva_abort("disable iff", to_sva_abort_expr(src)); else if(src.id()==ID_sva_eventually) { diff --git a/src/verilog/parser.y b/src/verilog/parser.y index c87acbd2c..8590f0658 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2179,13 +2179,13 @@ property_expr_proper: | sequence_expr "#=#" property_expr { init($$, ID_sva_nonoverlapped_followed_by); mto($$, $1); mto($$, $3); } | "nexttime" property_expr - { init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); } + { init($$, "sva_nexttime"); mto($$, $2); } | "nexttime" '[' constant_expression ']' property_expr %prec "nexttime" - { init($$, "sva_nexttime"); mto($$, $3); mto($$, $5); } + { init($$, "sva_indexed_nexttime"); mto($$, $3); mto($$, $5); } | "s_nexttime" property_expr - { init($$, "sva_s_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); } + { init($$, "sva_s_nexttime"); mto($$, $2); } | "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime" - { init($$, "sva_s_nexttime"); mto($$, $3); mto($$, $5); } + { init($$, "sva_indexed_s_nexttime"); mto($$, $3); mto($$, $5); } | "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always" { init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); } | "always" property_expr diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 2885b3735..c7b066a4b 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -84,18 +84,62 @@ static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr) return static_cast(expr); } -class sva_nexttime_exprt : public binary_predicate_exprt +/// nonindexed variant +class sva_nexttime_exprt : public unary_predicate_exprt { public: - // nonindexed variant explicit sva_nexttime_exprt(exprt op) - : binary_predicate_exprt(nil_exprt(), ID_sva_nexttime, std::move(op)) + : unary_predicate_exprt(ID_sva_nexttime, std::move(op)) { } +}; + +static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_nexttime); + sva_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_nexttime); + sva_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +/// nonindexed variant +class sva_s_nexttime_exprt : public unary_predicate_exprt +{ +public: + explicit sva_s_nexttime_exprt(exprt op) + : unary_predicate_exprt(ID_sva_s_nexttime, std::move(op)) + { + } +}; + +static inline const sva_s_nexttime_exprt & +to_sva_s_nexttime_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_s_nexttime); + sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_s_nexttime); + sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} - bool is_indexed() const +/// indexed variant of sva_nexttime_exprt +class sva_indexed_nexttime_exprt : public binary_predicate_exprt +{ +public: + sva_indexed_nexttime_exprt(exprt index, exprt op) + : binary_predicate_exprt(std::move(index), ID_sva_nexttime, std::move(op)) { - return index().is_not_nil(); } const exprt &index() const @@ -123,32 +167,32 @@ class sva_nexttime_exprt : public binary_predicate_exprt using binary_predicate_exprt::op1; }; -static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr) +static inline const sva_indexed_nexttime_exprt & +to_sva_indexed_nexttime_expr(const exprt &expr) { - PRECONDITION(expr.id() == ID_sva_nexttime); - sva_nexttime_exprt::check(expr, validation_modet::INVARIANT); - return static_cast(expr); + PRECONDITION(expr.id() == ID_sva_indexed_nexttime); + sva_indexed_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); } -static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr) +static inline sva_indexed_nexttime_exprt & +to_sva_indexed_nexttime_expr(exprt &expr) { - PRECONDITION(expr.id() == ID_sva_nexttime); - sva_nexttime_exprt::check(expr, validation_modet::INVARIANT); - return static_cast(expr); + PRECONDITION(expr.id() == ID_sva_indexed_nexttime); + sva_indexed_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); } -class sva_s_nexttime_exprt : public binary_predicate_exprt +/// indexed variant of sva_s_nexttime_exprt +class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt { public: - // nonindexed variant - explicit sva_s_nexttime_exprt(exprt op) - : binary_predicate_exprt(nil_exprt(), ID_sva_s_nexttime, std::move(op)) - { - } - - bool is_indexed() const + sva_indexed_s_nexttime_exprt(exprt index, exprt op) + : binary_predicate_exprt( + std::move(index), + ID_sva_indexed_s_nexttime, + std::move(op)) { - return index().is_not_nil(); } const exprt &index() const @@ -176,19 +220,20 @@ class sva_s_nexttime_exprt : public binary_predicate_exprt using binary_predicate_exprt::op1; }; -static inline const sva_s_nexttime_exprt & -to_sva_s_nexttime_expr(const exprt &expr) +static inline const sva_indexed_s_nexttime_exprt & +to_sva_indexed_s_nexttime_expr(const exprt &expr) { - PRECONDITION(expr.id() == ID_sva_s_nexttime); - sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT); - return static_cast(expr); + PRECONDITION(expr.id() == ID_sva_indexed_s_nexttime); + sva_indexed_s_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); } -static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr) +static inline sva_indexed_s_nexttime_exprt & +to_sva_indexed_s_nexttime_expr(exprt &expr) { - PRECONDITION(expr.id() == ID_sva_s_nexttime); - sva_s_nexttime_exprt::check(expr, validation_modet::INVARIANT); - return static_cast(expr); + PRECONDITION(expr.id() == ID_sva_indexed_s_nexttime); + sva_indexed_s_nexttime_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); } class sva_ranged_predicate_exprt : public ternary_exprt diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 0b44855cd..151278bb8 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2405,7 +2405,8 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr) expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay_plus || expr.id() == ID_sva_cycle_delay_star || expr.id() == ID_sva_weak || - expr.id() == ID_sva_strong) + expr.id() == ID_sva_strong || expr.id() == ID_sva_nexttime || + expr.id() == ID_sva_s_nexttime) { convert_expr(expr.op()); make_boolean(expr.op()); @@ -2821,24 +2822,22 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) expr.type() = bool_typet(); return std::move(expr); } - else if(expr.id() == ID_sva_nexttime) + else if(expr.id() == ID_sva_indexed_nexttime) { - if(to_sva_nexttime_expr(expr).is_indexed()) - convert_expr(to_sva_nexttime_expr(expr).index()); + convert_expr(to_sva_indexed_nexttime_expr(expr).index()); - auto &op = to_sva_nexttime_expr(expr).op(); + auto &op = to_sva_indexed_nexttime_expr(expr).op(); convert_expr(op); make_boolean(op); expr.type() = bool_typet(); return std::move(expr); } - else if(expr.id() == ID_sva_s_nexttime) + else if(expr.id() == ID_sva_indexed_s_nexttime) { - if(to_sva_s_nexttime_expr(expr).is_indexed()) - convert_expr(to_sva_s_nexttime_expr(expr).index()); + convert_expr(to_sva_indexed_s_nexttime_expr(expr).index()); - auto &op = to_sva_s_nexttime_expr(expr).op(); + auto &op = to_sva_indexed_s_nexttime_expr(expr).op(); convert_expr(op); make_boolean(op); expr.type() = bool_typet();