diff --git a/regression/verilog/SVA/disable_iff1.desc b/regression/verilog/SVA/disable_iff1.desc new file mode 100644 index 000000000..3fe739084 --- /dev/null +++ b/regression/verilog/SVA/disable_iff1.desc @@ -0,0 +1,12 @@ +CORE +disable_iff1.sv +--module main --bound 10 --numbered-trace +^\[main\.p0\] always \(disable iff \(main.counter == 0\) main\.counter != 0\): PROVED up to bound 10$ +^\[main\.p1\] always \(disable iff \(1\) 0\): PROVED up to bound 10$ +^\[main\.p2\] always \(disable iff \(main\.counter == 1\) main\.counter == 0\): REFUTED$ +^Counterexample with 3 states:$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/verilog/SVA/disable_iff1.sv b/regression/verilog/SVA/disable_iff1.sv new file mode 100644 index 000000000..e397fb5a8 --- /dev/null +++ b/regression/verilog/SVA/disable_iff1.sv @@ -0,0 +1,18 @@ +module main(input clk); + + // count up + reg [7:0] counter = 0; + + always_ff @(posedge clk) + counter++; + + // expected to pass + p0: assert property (@(posedge clk) disable iff (counter == 0) counter != 0); + + // expected to pass vacuously + p1: assert property (@(posedge clk) disable iff (1) 0); + + // expected to fail when counter reaches 2 + p2: assert property (@(posedge clk) disable iff (counter == 1) counter == 0); + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index a3dcf2e30..2066f3514 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -22,6 +22,7 @@ IREP_ID_ONE(sva_case) IREP_ID_ONE(sva_cycle_delay) IREP_ID_ONE(sva_cycle_delay_star) IREP_ID_ONE(sva_cycle_delay_plus) +IREP_ID_ONE(sva_disable_iff) IREP_ID_ONE(sva_sequence_concatenation) IREP_ID_ONE(sva_sequence_consecutive_repetition) IREP_ID_ONE(sva_sequence_first_match) diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index 83dc50e30..de0f6c56d 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -115,6 +115,11 @@ exprt normalize_property(exprt expr) : sva_if_expr.false_case(); expr = if_exprt{sva_if_expr.cond(), sva_if_expr.true_case(), false_case}; } + else if(expr.id() == ID_sva_disable_iff) + { + auto &disable_iff_expr = to_sva_disable_iff_expr(expr); + expr = or_exprt{disable_iff_expr.lhs(), disable_iff_expr.rhs()}; + } else if(expr.id() == ID_sva_strong) { expr = to_sva_strong_expr(expr).op(); diff --git a/src/temporal-logic/normalize_property.h b/src/temporal-logic/normalize_property.h index c33e7be8d..e7d2212ce 100644 --- a/src/temporal-logic/normalize_property.h +++ b/src/temporal-logic/normalize_property.h @@ -19,6 +19,7 @@ Author: Daniel Kroening, dkr@amazon.com /// sva_nexttime φ --> Xφ /// sva_s_nexttime φ --> Xφ /// sva_if --> ? : +/// a sva_disable_iff b --> a ∨ b /// ¬Xφ --> X¬φ /// ¬¬φ --> φ /// ¬Gφ --> F¬φ diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 3f9171915..29ae53ea7 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -14,12 +14,13 @@ bool is_temporal_operator(const exprt &expr) { return is_CTL_operator(expr) || is_LTL_operator(expr) || is_SVA_sequence(expr) || expr.id() == ID_A || expr.id() == ID_E || - expr.id() == ID_sva_always || 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 || + expr.id() == ID_sva_disable_iff || expr.id() == ID_sva_always || + 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 || expr.id() == ID_sva_overlapped_followed_by || expr.id() == ID_sva_nonoverlapped_followed_by; } diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 2fca48c7e..a67b0dc5b 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -475,6 +475,30 @@ std::string expr2verilogt::convert_sva_binary( /*******************************************************************\ +Function: expr2verilogt::convert_sva_disable_iff + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::string +expr2verilogt::convert_sva_disable_iff(const sva_disable_iff_exprt &expr) +{ + verilog_precedencet p0; + auto s0 = convert(expr.condition(), p0); + + verilog_precedencet p1; + auto s1 = convert(expr.rhs(), p1); + + return "disable iff (" + s0 + ") " + s1; +} + +/*******************************************************************\ + Function: expr2verilogt::convert_sva_indexed_binary Inputs: @@ -1408,6 +1432,10 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence) return precedence = verilog_precedencet::MIN, convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src)); + else if(src.id() == ID_sva_disable_iff) + return precedence = verilog_precedencet::MIN, + convert_sva_disable_iff(to_sva_disable_iff_expr(src)); + else if(src.id()==ID_sva_s_nexttime) return precedence = verilog_precedencet::MIN, convert_sva_indexed_binary( diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 2cdd7a093..996ee0de4 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include class sva_case_exprt; +class sva_disable_iff_exprt; class sva_if_exprt; class sva_ranged_predicate_exprt; @@ -122,6 +123,8 @@ class expr2verilogt std::string convert_sva_indexed_binary(const std::string &name, const binary_exprt &); + std::string convert_sva_disable_iff(const sva_disable_iff_exprt &); + virtual std::string convert_replication(const replication_exprt &, verilog_precedencet); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 68c0acda9..606489303 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -531,7 +531,7 @@ int yyverilogerror(const char *error) // whereas the table gives them in decreasing order. // The precendence of the assertion operators is lower than // those in Table 11-2. -%nonassoc "property_expr_event_control" // @(...) property_expr +%nonassoc "property_expr_clocking_event" // @(...) property_expr %nonassoc "always" "s_always" "eventually" "s_eventually" %nonassoc "accept_on" "reject_on" %nonassoc "sync_accept_on" "sync_reject_on" @@ -2081,8 +2081,10 @@ property_formal_type: ; property_spec: - TOK_DISABLE TOK_IFF '(' expression ')' property_expr - { $$=$6; } + clocking_event TOK_DISABLE TOK_IFF '(' expression ')' property_expr + { init($$, ID_sva_disable_iff); mto($$, $5); mto($$, $7); } + | TOK_DISABLE TOK_IFF '(' expression ')' property_expr + { init($$, ID_sva_disable_iff); mto($$, $4); mto($$, $6); } | property_expr ; @@ -2163,7 +2165,7 @@ property_expr_proper: { init($$, "sva_sync_accept_on"); mto($$, $3); } | "sync_reject_on" '(' expression_or_dist ')' { init($$, "sva_sync_reject_on"); mto($$, $3); } - | event_control property_expr { $$=$2; } %prec "property_expr_event_control" + | clocking_event property_expr { $$=$2; } %prec "property_expr_clocking_event" ; property_case_item_brace: diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index f14fdb988..3d644fa8f 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -11,6 +11,57 @@ Author: Daniel Kroening, kroening@kroening.com #include +class sva_disable_iff_exprt : public binary_predicate_exprt +{ +public: + explicit sva_disable_iff_exprt(exprt condition, exprt property) + : binary_predicate_exprt( + std::move(condition), + ID_sva_disable_iff, + std::move(property)) + { + } + + const exprt &condition() const + { + return op0(); + } + + exprt &condition() + { + return op0(); + } + + const exprt &property() const + { + return op1(); + } + + exprt &property() + { + return op1(); + } + +protected: + using binary_predicate_exprt::op0; + using binary_predicate_exprt::op1; +}; + +static inline const sva_disable_iff_exprt & +to_sva_disable_iff_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_disable_iff); + sva_disable_iff_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_disable_iff); + sva_disable_iff_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class sva_nexttime_exprt : public binary_predicate_exprt { public: diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 22ec82e08..28618db5b 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -2527,6 +2527,15 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) return std::move(expr); } + else if(expr.id() == ID_sva_disable_iff) + { + convert_expr(to_sva_disable_iff_expr(expr).condition()); + make_boolean(to_sva_disable_iff_expr(expr).condition()); + convert_expr(to_sva_disable_iff_expr(expr).property()); + make_boolean(to_sva_disable_iff_expr(expr).property()); + expr.type() = bool_typet(); + return std::move(expr); + } else if(expr.id() == ID_sva_nexttime) { if(to_sva_nexttime_expr(expr).is_indexed())