diff --git a/regression/verilog/SVA/always_with_range1.desc b/regression/verilog/SVA/always_with_range1.desc new file mode 100644 index 000000000..6f3d73896 --- /dev/null +++ b/regression/verilog/SVA/always_with_range1.desc @@ -0,0 +1,11 @@ +CORE +always_with_range1.sv +--bound 20 +^\[main\.property\.1\] always \[0:9\] main\.x < 10: PROVED up to bound 20$ +^\[main\.property\.2\] always \[0:\$\] main\.x < 10: REFUTED$ +^\[main\.property\.3\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/always_with_range1.sv b/regression/verilog/SVA/always_with_range1.sv new file mode 100644 index 000000000..7f806401e --- /dev/null +++ b/regression/verilog/SVA/always_with_range1.sv @@ -0,0 +1,20 @@ +module main; + + reg [31:0] x; + wire clk; + + initial x=0; + + always @(posedge clk) + x<=x+1; + + // holds owing to the range + initial p0: assert property (always [0:9] x<10); + + // unbounded, fails + initial p1: assert property (always [0:$] x<10); + + // strong variant + initial p2: assert property (s_always [0:9] x<10); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index a92d9dd1c..00e979018 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -16,6 +16,8 @@ IREP_ID_ONE(sva_sequence_throughout) IREP_ID_ONE(sva_sequence_concatenation) IREP_ID_ONE(sva_sequence_first_match) IREP_ID_ONE(sva_always) +IREP_ID_ONE(sva_ranged_always) +IREP_ID_ONE(sva_s_always) IREP_ID_ONE(sva_cover) IREP_ID_ONE(sva_nexttime) IREP_ID_ONE(sva_s_nexttime) diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 77d7fae14..0216ef3ba 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -17,11 +17,12 @@ bool is_temporal_operator(const exprt &expr) expr.id() == ID_A || expr.id() == ID_E || expr.id() == ID_U || expr.id() == ID_R || expr.id() == ID_G || expr.id() == ID_F || expr.id() == ID_X || expr.id() == ID_sva_always || - expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime || - expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until || - expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with || - expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually || - expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay; + expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always || + expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime || + expr.id() == ID_sva_until || expr.id() == ID_sva_s_until || + expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with || + expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually || + expr.id() == ID_sva_cycle_delay; } bool has_temporal_operator(const exprt &expr) diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 06d1c46d6..6061b10cd 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -8,11 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "property.h" +#include #include #include #include #include +#include #include #include #include @@ -56,6 +58,8 @@ bool bmc_supports_property(const exprt &expr) return bmc_supports_property(to_X_expr(expr).op()); else if(expr.id() == ID_sva_always) return true; + else if(expr.id() == ID_sva_ranged_always) + return true; else return false; } @@ -75,12 +79,12 @@ Function: property_obligations_rec static void property_obligations_rec( const exprt &property_expr, decision_proceduret &solver, - std::size_t current, - std::size_t no_timeframes, + const mp_integer ¤t, + const mp_integer &no_timeframes, const namespacet &ns, - std::map &obligations) + std::map &obligations) { - PRECONDITION(current < no_timeframes); + PRECONDITION(current >= 0 && current < no_timeframes); if(property_expr.id() == ID_X) { @@ -108,7 +112,43 @@ static void property_obligations_rec( PRECONDITION(false); }(property_expr); - for(std::size_t c = current; c < no_timeframes; c++) + for(mp_integer c = current; c < no_timeframes; ++c) + { + property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations); + } + } + else if( + property_expr.id() == ID_sva_ranged_always || + property_expr.id() == ID_sva_s_always) + { + auto &phi = property_expr.id() == ID_sva_ranged_always + ? to_sva_ranged_always_expr(property_expr).op() + : to_sva_s_always_expr(property_expr).op(); + auto &range = property_expr.id() == ID_sva_ranged_always + ? to_sva_ranged_always_expr(property_expr).range() + : to_sva_s_always_expr(property_expr).range(); + + auto from_opt = numeric_cast(range.op0()); + if(!from_opt.has_value()) + throw ebmc_errort() << "failed to convert SVA always from index"; + + auto from = std::max(mp_integer{0}, *from_opt); + + mp_integer to; + + if(range.op1().id() == ID_infinity) + { + to = no_timeframes - 1; + } + else + { + auto to_opt = numeric_cast(range.op1()); + if(!to_opt.has_value()) + throw ebmc_errort() << "failed to convert SVA always to index"; + to = std::min(*to_opt, no_timeframes - 1); + } + + for(mp_integer c = from; c <= to; ++c) { property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations); } @@ -133,13 +173,13 @@ Function: property_obligations \*******************************************************************/ -static std::map property_obligations( +static std::map property_obligations( const exprt &property_expr, decision_proceduret &solver, - std::size_t no_timeframes, + const mp_integer &no_timeframes, const namespacet &ns) { - std::map obligations; + std::map obligations; property_obligations_rec( property_expr, solver, 0, no_timeframes, ns, obligations); @@ -178,8 +218,10 @@ void property( for(auto &obligation_it : obligations) { auto t = obligation_it.first; - DATA_INVARIANT(t < no_timeframes, "obligation must have valid timeframe"); - prop_handles[t] = conjunction(obligation_it.second); + DATA_INVARIANT( + t >= 0 && t < no_timeframes, "obligation must have valid timeframe"); + auto t_int = numeric_cast_v(t); + prop_handles[t_int] = conjunction(obligation_it.second); } } diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index bb967f162..c47860929 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -394,8 +394,12 @@ std::string expr2verilogt::convert_sva( if(range.has_value()) { auto &range_binary = to_binary_expr(range.value()); - range_str = "[" + convert(range_binary.lhs()) + ':' + - convert(range_binary.rhs()) + "] "; + range_str = "[" + convert(range_binary.lhs()) + ':'; + if(range_binary.rhs().id() == ID_infinity) + range_str += "$"; + else + range_str += convert(range_binary.rhs()); + range_str += "] "; } unsigned p; @@ -1088,6 +1092,22 @@ std::string expr2verilogt::convert( else if(src.id()==ID_sva_always) return precedence = 0, convert_sva("always", to_sva_always_expr(src).op()); + else if(src.id() == ID_sva_ranged_always) + { + return precedence = 0, convert_sva( + "always", + to_sva_ranged_always_expr(src).range(), + to_sva_ranged_always_expr(src).op()); + } + + else if(src.id() == ID_sva_s_always) + { + return precedence = 0, convert_sva( + "s_always", + to_sva_s_always_expr(src).range(), + to_sva_s_always_expr(src).op()); + } + else if(src.id() == ID_sva_cover) return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op()); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 10b113297..e27dab48a 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -1946,8 +1946,11 @@ property_expr_proper: | property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); } | "nexttime" property_expr { init($$, "sva_nexttime"); mto($$, $2); } | "s_nexttime" property_expr { init($$, "sva_s_nexttime"); mto($$, $2); } + | "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always" + { init($$, ID_sva_ranged_always); mto($$, $3); mto($$, $5); } | "always" property_expr { init($$, "sva_always"); mto($$, $2); } - | "s_always" property_expr { init($$, "sva_s_always"); mto($$, $2); } + | "s_always" '[' constant_range ']' property_expr %prec "s_always" + { init($$, ID_sva_s_always); mto($$, $3); mto($$, $5); } | "s_eventually" property_expr { init($$, "sva_s_eventually"); mto($$, $2); } | "eventually" '[' constant_range ']' property_expr %prec "eventually" @@ -1989,8 +1992,10 @@ cycle_delay_range: ; cycle_delay_const_range_expression: - constant_expression ':' constant_expression - | constant_expression ':' '$' + constant_expression TOK_COLON constant_expression + { init($$, ID_sva_cycle_delay); mto($$, $1); mto($$, $3); } + | constant_expression TOK_COLON '$' + { init($$, ID_sva_cycle_delay); mto($$, $1); stack_expr($$).add_to_operands(exprt(ID_infinity)); } ; expression_or_dist: diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 7f7942219..776683078 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -170,6 +170,129 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr) return static_cast(expr); } +class sva_ranged_always_exprt : public binary_predicate_exprt +{ +public: + sva_ranged_always_exprt(binary_exprt range, exprt op) + : binary_predicate_exprt(std::move(range), ID_sva_always, std::move(op)) + { + } + + // These come with a range, which is binary + const binary_exprt &range() const + { + return static_cast(op0()); + } + + binary_exprt &range() + { + return static_cast(op0()); + } + + const exprt &op() const + { + return op1(); + } + + exprt &op() + { + return op1(); + } + + const exprt &lhs() const = delete; + exprt &lhs() = delete; + const exprt &rhs() const = delete; + exprt &rhs() = delete; + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_exprt::check(expr, vm); + binary_exprt::check(to_binary_expr(expr).op0(), vm); + } + +protected: + using binary_predicate_exprt::op0; + using binary_predicate_exprt::op1; +}; + +static inline const sva_ranged_always_exprt & +to_sva_ranged_always_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_ranged_always); + sva_ranged_always_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_ranged_always_exprt &to_sva_ranged_always_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_ranged_always); + sva_ranged_always_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +class sva_s_always_exprt : public binary_predicate_exprt +{ +public: + sva_s_always_exprt(binary_exprt range, exprt op) + : binary_predicate_exprt(std::move(range), ID_sva_s_always, std::move(op)) + { + } + + // These come with a range, which is binary + const binary_exprt &range() const + { + return static_cast(op0()); + } + + binary_exprt &range() + { + return static_cast(op0()); + } + + const exprt &op() const + { + return op1(); + } + + exprt &op() + { + return op1(); + } + + const exprt &lhs() const = delete; + exprt &lhs() = delete; + const exprt &rhs() const = delete; + exprt &rhs() = delete; + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + binary_exprt::check(expr, vm); + binary_exprt::check(to_binary_expr(expr).op0(), vm); + } + +protected: + using binary_predicate_exprt::op0; + using binary_predicate_exprt::op1; +}; + +static inline const sva_s_always_exprt &to_sva_s_always_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_s_always); + sva_s_always_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_s_always_exprt &to_sva_s_always_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_s_always); + sva_s_always_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class sva_cover_exprt : public unary_predicate_exprt { public: diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 5ae9c3c59..5b5bf5958 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -1592,6 +1592,16 @@ void verilog_typecheck_exprt::implicit_typecast( return; } } +#if 0 + else if(src_type.id() == ID_natural) + { + if(dest_type.id()==ID_integer) + { + expr = typecast_exprt{expr, dest_type}; + return; + } + } +#endif else if( src_type.id() == ID_bool || src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv || src_type.id() == ID_verilog_unsignedbv || @@ -2240,21 +2250,32 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) return std::move(expr); } - else if(expr.id() == ID_sva_eventually) + else if( + expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_always || + expr.id() == ID_sva_s_always) { auto &range = to_binary_expr(expr.op0()); + auto lower = convert_integer_constant_expression(range.op0()); - auto upper = convert_integer_constant_expression(range.op1()); - if(lower > upper) - { - throw errort().with_location(expr.source_location()) - << "range must be lower <= upper"; - } range.op0() = from_integer(lower, natural_typet()) .with_source_location(range.op0()); - range.op1() = from_integer(upper, natural_typet()) - .with_source_location(range.op1()); + + if(range.op1().id() == ID_infinity) + { + } + else + { + auto upper = convert_integer_constant_expression(range.op1()); + if(lower > upper) + { + throw errort().with_location(expr.source_location()) + << "range must be lower <= upper"; + } + + range.op1() = from_integer(upper, natural_typet()) + .with_source_location(range.op1()); + } convert_expr(expr.op1()); make_boolean(expr.op1());