diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 18d9bb9f..359fd4a3 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -45,6 +45,7 @@ IREP_ID_ONE(smv_EBG) IREP_ID_ONE(smv_ABG) IREP_ID_ONE(smv_ABU) IREP_ID_ONE(smv_EBU) +IREP_ID_ONE(sva_boolean) IREP_ID_ONE(sva_accept_on) IREP_ID_ONE(sva_reject_on) IREP_ID_ONE(sva_sync_accept_on) diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 4d972345..8ef4b463 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -23,12 +23,13 @@ Author: Daniel Kroening, dkr@amazon.com exprt normalize_pre_sva_non_overlapped_implication( sva_non_overlapped_implication_exprt expr) { - // Same as a->always[1:1] b if lhs is not a sequence. - if(!is_SVA_sequence_operator(expr.lhs())) + // Same as a->always[1:1] b if lhs is not a proper sequence. + if(expr.lhs().id() == ID_sva_boolean) { + const auto &lhs_cond = to_sva_boolean_expr(expr.lhs()).op(); auto one = natural_typet{}.one_expr(); return or_exprt{ - not_exprt{expr.lhs()}, sva_ranged_always_exprt{one, one, expr.rhs()}}; + not_exprt{lhs_cond}, sva_ranged_always_exprt{one, one, expr.rhs()}}; } else return std::move(expr); diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 7d1c6fce..7495cbce 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -105,9 +105,9 @@ bool is_SVA_sequence_operator(const exprt &expr) // ID_sva_non_overlapped_implication and ID_sva_overlapped_implication // are property expressions, not sequence expressions. // Note that ID_sva_not does not yield a sequence expression. - return id == ID_sva_and || id == ID_sva_or || id == ID_sva_cycle_delay || - id == ID_sva_cycle_delay_plus || id == ID_sva_cycle_delay_star || - id == ID_sva_sequence_concatenation || + return id == ID_sva_boolean || id == ID_sva_and || id == ID_sva_or || + id == ID_sva_cycle_delay || id == ID_sva_cycle_delay_plus || + id == ID_sva_cycle_delay_star || id == ID_sva_sequence_concatenation || id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match || id == ID_sva_sequence_throughout || id == ID_sva_sequence_within || id == ID_sva_sequence_goto_repetition || @@ -120,7 +120,9 @@ bool is_SVA_sequence_operator(const exprt &expr) bool is_SVA_operator(const exprt &expr) { auto id = expr.id(); - return is_SVA_sequence_operator(expr) || id == ID_sva_disable_iff || + return is_SVA_sequence_operator(expr) || id == ID_sva_implies || + id == ID_sva_iff || id == ID_sva_not || id == ID_sva_case || + id == ID_sva_if || id == ID_sva_disable_iff || id == ID_sva_accept_on || id == ID_sva_reject_on || id == ID_sva_sync_accept_on || id == ID_sva_sync_reject_on || id == ID_sva_always || id == ID_sva_s_always || @@ -245,10 +247,11 @@ struct ltl_sequence_matcht std::vector LTL_sequence_matches(const exprt &sequence) { - if(!is_SVA_sequence_operator(sequence)) + if(sequence.id() == ID_sva_boolean) { // atomic proposition - return {{sequence, 1}}; + auto &p = to_sva_boolean_expr(sequence).op(); + return {{p, 1}}; } else if(sequence.id() == ID_sva_sequence_concatenation) { diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index b9341a7d..d3e2ab6c 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -411,10 +411,19 @@ sequence_matchest instantiate_sequence( return result; } - else + else if(expr.id() == ID_sva_boolean) { - // not a sequence, evaluate as state predicate - auto instantiated = instantiate_property(expr, t, no_timeframes); + // a state predicate + auto &predicate = to_sva_boolean_expr(expr).op(); + auto instantiated = instantiate_property(predicate, t, no_timeframes); return {{instantiated.first, instantiated.second}}; } + else + { + DATA_CHECK_WITH_DIAGNOSTICS( + validation_modet::INVARIANT, + false, + "unexpected sequence expression", + expr.pretty()); + } } diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index ba93e737..b31fdbae 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1810,6 +1810,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return convert_rec(to_sva_sequence_property_expr_base(src).sequence()); } + else if(src.id() == ID_sva_boolean) + { + // These are invisible + return convert_rec(to_sva_boolean_expr(src).op()); + } + else if(src.id()==ID_sva_sequence_concatenation) return convert_sva_sequence_concatenation( to_binary_expr(src), precedence = verilog_precedencet::MIN); diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 455cb5bc..d6763932 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -13,6 +13,29 @@ Author: Daniel Kroening, kroening@kroening.com #include "verilog_types.h" +/// 1800-2017 16.6 Boolean expressions +/// Conversion of a Boolean expression into a sequence or property +class sva_boolean_exprt : public unary_exprt +{ +public: + sva_boolean_exprt(exprt condition, typet __type) + : unary_exprt(ID_sva_boolean, std::move(condition), std::move(__type)) + { + } +}; + +static inline const sva_boolean_exprt &to_sva_boolean_expr(const exprt &expr) +{ + sva_boolean_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_boolean_exprt &to_sva_boolean_expr(exprt &expr) +{ + sva_boolean_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + /// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff class sva_abort_exprt : public binary_predicate_exprt { diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 4abe8adf..34723582 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -35,8 +35,9 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &expr) } else { - // state formula, can cast to sequence + // state formula, can convert to sequence make_boolean(expr); + expr = sva_boolean_exprt{std::move(expr), verilog_sva_sequence_typet{}}; } } else @@ -86,10 +87,8 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr) return std::move(expr); } else if( - expr.id() == ID_sva_cycle_delay_plus || // ##[+] - expr.id() == ID_sva_cycle_delay_star || // ##[*] - expr.id() == ID_sva_sequence_repetition_plus || // x[+] - expr.id() == ID_sva_sequence_repetition_star) // x[*} + expr.id() == ID_sva_cycle_delay_plus || // ##[+] + expr.id() == ID_sva_cycle_delay_star) // ##[*] { // These take a sequence as argument. // For some, the grammar allows properties to implement and/or over @@ -99,6 +98,16 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr) expr.type() = verilog_sva_sequence_typet{}; return std::move(expr); } + else if( + expr.id() == ID_sva_sequence_repetition_plus || // x[+] + expr.id() == ID_sva_sequence_repetition_star) // x[*] + { + // These take a Boolean as argument, and yield a sequence. + convert_expr(expr.op()); + make_boolean(expr.op()); + expr.type() = verilog_sva_sequence_typet{}; + return std::move(expr); + } else if(expr.id() == ID_sva_weak || expr.id() == ID_sva_strong) { convert_sva(expr.op()); @@ -109,7 +118,11 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr) else { // not SVA - return convert_expr_rec(std::move(expr)); + DATA_CHECK_WITH_DIAGNOSTICS( + validation_modet::INVARIANT, + false, + "unexpected unary SVA expression", + expr.pretty()); } } @@ -123,14 +136,12 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) // These yield sequences when both operands are sequences, and // properties otherwise. if( - (expr.lhs().type().id() == ID_verilog_sva_sequence || - !has_temporal_operator(expr.lhs())) && - (expr.rhs().type().id() == ID_verilog_sva_sequence || - !has_temporal_operator(expr.rhs()))) + expr.lhs().type().id() == ID_verilog_sva_sequence && + expr.rhs().type().id() == ID_verilog_sva_sequence) { - expr.type() = verilog_sva_sequence_typet{}; require_sva_sequence(expr.lhs()); require_sva_sequence(expr.rhs()); + expr.type() = verilog_sva_sequence_typet{}; } else { @@ -294,8 +305,12 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) } else { - // not SVA - return convert_expr_rec(std::move(expr)); + // unexpected SVA expression + DATA_CHECK_WITH_DIAGNOSTICS( + validation_modet::INVARIANT, + false, + "unexpected binary SVA expression", + expr.pretty()); } } @@ -409,22 +424,38 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr) else { // not SVA - return convert_expr_rec(std::move(expr)); + DATA_CHECK_WITH_DIAGNOSTICS( + validation_modet::INVARIANT, + false, + "unexpected ternary SVA expression", + expr.pretty()); } } exprt verilog_typecheck_exprt::convert_sva_rec(exprt expr) { - switch(expr.operands().size()) - { - case 1: - return convert_unary_sva(to_unary_expr(expr)); - case 2: - return convert_binary_sva(to_binary_expr(expr)); - case 3: - return convert_ternary_sva(to_ternary_expr(expr)); - default: - return convert_expr_rec(expr); + if(is_SVA_operator(expr)) + { + switch(expr.operands().size()) + { + case 1: + return convert_unary_sva(to_unary_expr(expr)); + case 2: + return convert_binary_sva(to_binary_expr(expr)); + case 3: + return convert_ternary_sva(to_ternary_expr(expr)); + default: + DATA_CHECK_WITH_DIAGNOSTICS( + validation_modet::INVARIANT, + false, + "unexpected SVA expression", + expr.pretty()); + } + } + else + { + // not SVA, but an expression that gets sampled. + return convert_expr_rec(std::move(expr)); } }