From 856378750a1f0970c6e83f5422bfdeca0bd4baa1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 17 Oct 2024 09:39:37 -0700 Subject: [PATCH] SVA: consecutive repetition This implements SVA's [*n] sequence operator. --- .../verilog/SVA/sequence_repetition1.desc | 12 ++-- .../verilog/SVA/sequence_repetition3.desc | 11 ++++ .../verilog/SVA/sequence_repetition3.sv | 19 +++++++ src/trans-word-level/property.cpp | 4 -- src/trans-word-level/sequence.cpp | 6 ++ src/verilog/expr2verilog.cpp | 31 ++++++++++- src/verilog/expr2verilog_class.h | 3 + src/verilog/parser.y | 5 +- src/verilog/sva_expr.cpp | 21 +++++++ src/verilog/sva_expr.h | 26 +++++++++ src/verilog/verilog_typecheck_expr.cpp | 55 ++++++++++++++++++- src/verilog/verilog_typecheck_expr.h | 1 + 12 files changed, 177 insertions(+), 17 deletions(-) create mode 100644 regression/verilog/SVA/sequence_repetition3.desc create mode 100644 regression/verilog/SVA/sequence_repetition3.sv diff --git a/regression/verilog/SVA/sequence_repetition1.desc b/regression/verilog/SVA/sequence_repetition1.desc index 938c543e0..3218c18a2 100644 --- a/regression/verilog/SVA/sequence_repetition1.desc +++ b/regression/verilog/SVA/sequence_repetition1.desc @@ -1,12 +1,12 @@ CORE sequence_repetition1.sv --bound 10 -^\[.*\] 1 \[\*\] main\.half_x == 0: FAILURE: property not supported by BMC engine$ -^\[.*\] 1 \[->\] main\.half_x == 0: FAILURE: property not supported by BMC engine$ -^\[.*\] 1 \[=\] main\.half_x == 0: FAILURE: property not supported by BMC engine$ -^\[.*\] 1 \[\*\] main\.x == 0: FAILURE: property not supported by BMC engine$ -^\[.*\] 1 \[->\] main\.x == 0: FAILURE: property not supported by BMC engine$ -^\[.*\] 1 \[=\] main\.x == 0: FAILURE: property not supported by BMC engine$ +^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$ +^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BMC engine$ +^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BMC engine$ +^\[.*\] main\.x == 0 \[\*2\]: REFUTED$ +^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BMC engine$ +^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BMC engine$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/sequence_repetition3.desc b/regression/verilog/SVA/sequence_repetition3.desc new file mode 100644 index 000000000..c17e1afbc --- /dev/null +++ b/regression/verilog/SVA/sequence_repetition3.desc @@ -0,0 +1,11 @@ +CORE +sequence_repetition3.sv +--bound 10 +^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED up to bound 10$ +^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED up to bound 10$ +^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/sequence_repetition3.sv b/regression/verilog/SVA/sequence_repetition3.sv new file mode 100644 index 000000000..e7a7b2f4a --- /dev/null +++ b/regression/verilog/SVA/sequence_repetition3.sv @@ -0,0 +1,19 @@ +module main(input clk); + + reg [31:0] x = 0; + + // 0 1 2 3 4 ... + always_ff @(posedge clk) + x<=x+1; + + // 0 0 1 1 2 2 3 3 ... + wire [31:0] half_x = x/2; + + // should pass + initial p0: assert property (x==0[*1] #=# x==1[*1]); + initial p1: assert property (half_x==0[*2] #=# half_x==1[*2]); + + // should fail + initial p2: assert property (half_x==0[*3]); + +endmodule diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index ea8bd330b..991bc4229 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -138,10 +138,6 @@ bool bmc_supports_SVA_property(const exprt &expr) if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition)) return false; - // sva_sequence_consecutive_repetition is not supported yet - if(has_subexpr(expr, ID_sva_sequence_consecutive_repetition)) - return false; - // sva_sequence_goto_repetition is not supported yet if(has_subexpr(expr, ID_sva_sequence_goto_repetition)) return false; diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 3f4f0e73c..35de68b4e 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -176,6 +176,12 @@ std::vector> instantiate_sequence( return result; } + else if(expr.id() == ID_sva_sequence_consecutive_repetition) + { + // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions + auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr); + return instantiate_sequence(repetition.lower(), t, no_timeframes); + } else { // not a sequence, evaluate as state predicate diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index acf6a4da6..163650334 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -502,6 +502,31 @@ 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_abort Inputs: @@ -1504,17 +1529,17 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) else if(src.id() == ID_sva_sequence_non_consecutive_repetition) return precedence = verilog_precedencet::MIN, - convert_sva_binary("[=]", to_binary_expr(src)); + convert_sva_binary_repetition("[=", to_binary_expr(src)); // not sure about precedence else if(src.id() == ID_sva_sequence_consecutive_repetition) return precedence = verilog_precedencet::MIN, - convert_sva_binary("[*]", to_binary_expr(src)); + convert_sva_binary_repetition("[*", to_binary_expr(src)); // not sure about precedence else if(src.id() == ID_sva_sequence_goto_repetition) return precedence = verilog_precedencet::MIN, - convert_sva_binary("[->]", to_binary_expr(src)); + convert_sva_binary_repetition("[->", to_binary_expr(src)); // not sure about precedence else if(src.id() == ID_sva_ranged_always) diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index f86e17fdc..805ffdd1d 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -124,6 +124,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_abort(const std::string &name, const sva_abort_exprt &); resultt diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 0c395726d..0bcb0682e 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2262,7 +2262,10 @@ expression_or_dist_brace: sequence_expr: expression_or_dist | expression_or_dist boolean_abbrev - { $$ = $2; mto($$, $1); } + { $$ = $2; + // preserve the operand ordering as in the source code + stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($1)); + } | cycle_delay_range sequence_expr { $$=$1; mto($$, $2); } | expression cycle_delay_range sequence_expr diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp index 50f82b650..5911c55c0 100644 --- a/src/verilog/sva_expr.cpp +++ b/src/verilog/sva_expr.cpp @@ -8,6 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "sva_expr.h" +#include +#include + exprt sva_case_exprt::lowering() const { auto &case_items = this->case_items(); @@ -35,3 +38,21 @@ exprt sva_case_exprt::lowering() const return if_exprt{ disjunction(disjuncts), case_items.front().result(), reduced_rec}; } + +exprt sva_sequence_consecutive_repetition_exprt::lower() const +{ + auto n = numeric_cast_v(to_constant_expr(rhs())); + DATA_INVARIANT(n >= 1, "number of repetitions must be at least one"); + + exprt result = lhs(); + + for(; n >= 2; --n) + { + auto cycle_delay = + sva_cycle_delay_exprt{from_integer(1, integer_typet{}), lhs()}; + result = sva_sequence_concatenation_exprt{ + std::move(cycle_delay), std::move(result)}; + } + + return result; +} diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index c56bf9961..a26e353b3 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1155,4 +1155,30 @@ inline sva_case_exprt &to_sva_case_expr(exprt &expr) return static_cast(expr); } +class sva_sequence_consecutive_repetition_exprt : public binary_predicate_exprt +{ +public: + exprt lower() const; + +protected: + using binary_predicate_exprt::op0; + using binary_predicate_exprt::op1; +}; + +inline const sva_sequence_consecutive_repetition_exprt & +to_sva_sequence_consecutive_repetition_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition); + sva_sequence_consecutive_repetition_exprt::check(expr); + return static_cast(expr); +} + +inline sva_sequence_consecutive_repetition_exprt & +to_sva_sequence_consecutive_repetition_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition); + sva_sequence_consecutive_repetition_exprt::check(expr); + return static_cast(expr); +} + #endif diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 43e1f1982..6009d076a 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1716,6 +1716,35 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression_check(exprt expr) /*******************************************************************\ +Function: verilog_typecheck_exprt::elaborate_constant_integer_expression + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +mp_integer +verilog_typecheck_exprt::elaborate_constant_integer_expression(exprt expr) +{ + source_locationt source_location = expr.find_source_location(); + + exprt tmp = elaborate_constant_expression(std::move(expr)); + + if(!tmp.is_constant()) + { + throw errort().with_location(source_location) + << "expected constant integer expression, but got `" << to_string(tmp) + << '\''; + } + + return numeric_cast_v(to_constant_expr(tmp)); +} + +/*******************************************************************\ + Function: verilog_typecheck_exprt::elaborate_constant_system_function_call Inputs: @@ -2969,17 +2998,37 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) else if( expr.id() == ID_sva_sequence_intersect || expr.id() == ID_sva_sequence_throughout || - expr.id() == ID_sva_sequence_within || - expr.id() == ID_sva_sequence_non_consecutive_repetition || + expr.id() == ID_sva_sequence_within) + { + auto &binary_expr = to_binary_expr(expr); + + convert_expr(binary_expr.lhs()); + make_boolean(binary_expr.lhs()); + convert_expr(binary_expr.rhs()); + make_boolean(binary_expr.rhs()); + + expr.type() = bool_typet(); + + return std::move(expr); + } + else if( expr.id() == ID_sva_sequence_consecutive_repetition || + expr.id() == ID_sva_sequence_non_consecutive_repetition || expr.id() == ID_sva_sequence_goto_repetition) { auto &binary_expr = to_binary_expr(expr); convert_expr(binary_expr.lhs()); make_boolean(binary_expr.lhs()); + convert_expr(binary_expr.rhs()); - make_boolean(binary_expr.rhs()); + + mp_integer n = elaborate_constant_integer_expression(binary_expr.rhs()); + if(n < 0) + throw errort().with_location(binary_expr.rhs().source_location()) + << "number of repetitions must not be negative"; + + binary_expr.rhs() = from_integer(n, integer_typet{}); expr.type() = bool_typet(); diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 7d60155f8..201a8500d 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -156,6 +156,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset std::optional is_constant_integer_post_convert(const exprt &); exprt elaborate_constant_expression(exprt); exprt elaborate_constant_expression_check(exprt); + mp_integer elaborate_constant_integer_expression(exprt); // To be overridden, requires a Verilog interpreter. virtual exprt elaborate_constant_function_call(const function_call_exprt &)