From 63c34367f0b5e6e6ba197a534aaf22025e7cf0e9 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 19 Oct 2025 17:00:11 -0700 Subject: [PATCH] SVA: add cover sequence 1800-2012 has introduced the cover sequence statement, in addition to the cover property statement. --- CHANGELOG | 2 + regression/verilog/SVA/cover_sequence1.sv | 4 +- regression/verilog/SVA/cover_sequence2.sv | 8 ++-- regression/verilog/SVA/cover_sequence3.sv | 6 +-- regression/verilog/SVA/cover_sequence4.sv | 6 +-- src/hw_cbmc_irep_ids.h | 2 + src/temporal-logic/temporal_logic.cpp | 3 +- src/temporal-logic/trivial_sva.cpp | 8 ++++ src/verilog/expr2verilog.cpp | 11 +++-- src/verilog/expr2verilog_class.h | 3 +- src/verilog/parser.y | 10 +++++ src/verilog/sva_expr.h | 52 +++++++++++++++++++++++ src/verilog/verilog_elaborate.cpp | 4 +- src/verilog/verilog_expr.cpp | 3 +- src/verilog/verilog_expr.h | 12 ++++-- src/verilog/verilog_interfaces.cpp | 3 +- src/verilog/verilog_synthesis.cpp | 44 ++++++++++++++++--- src/verilog/verilog_typecheck.cpp | 24 ++++++++--- src/verilog/verilog_typecheck_sva.cpp | 15 +++++++ 19 files changed, 181 insertions(+), 39 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 687ac144f..f4e1d66b9 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -1,5 +1,7 @@ # EBMC 5.8 +* SystemVerilog: cover sequence + # EBMC 5.7 * Verilog: --initial-zero changes the default value from nondet to zero diff --git a/regression/verilog/SVA/cover_sequence1.sv b/regression/verilog/SVA/cover_sequence1.sv index 5fcbc9384..fcc2207f1 100644 --- a/regression/verilog/SVA/cover_sequence1.sv +++ b/regression/verilog/SVA/cover_sequence1.sv @@ -7,9 +7,9 @@ module main(input clk); x++; // expected to pass - p0: cover property (x==2 ##1 x==3 ##1 x==4); + p0: cover sequence (x==2 ##1 x==3 ##1 x==4); // expected to fail - p1: cover property (x==2 ##1 x==3 ##1 x==5); + p1: cover sequence (x==2 ##1 x==3 ##1 x==5); endmodule diff --git a/regression/verilog/SVA/cover_sequence2.sv b/regression/verilog/SVA/cover_sequence2.sv index 117316945..473572c2f 100644 --- a/regression/verilog/SVA/cover_sequence2.sv +++ b/regression/verilog/SVA/cover_sequence2.sv @@ -7,15 +7,15 @@ module main(input clk); x++; // expected to fail - p0: cover property (x==2 ##1 x==3 ##1 x==100); + p0: cover sequence (x==2 ##1 x==3 ##1 x==100); // expected to fail until x reaches 100 - p1: cover property (x==98 ##1 x==99 ##1 x==100); + p1: cover sequence (x==98 ##1 x==99 ##1 x==100); // expected to pass once x reaches 5 - p2: cover property (x==3 ##1 x==4 ##1 x==5); + p2: cover sequence (x==3 ##1 x==4 ##1 x==5); // expected to pass once x reaches 6 - p3: cover property (x==4 ##1 x==5 ##1 x==6); + p3: cover sequence (x==4 ##1 x==5 ##1 x==6); endmodule diff --git a/regression/verilog/SVA/cover_sequence3.sv b/regression/verilog/SVA/cover_sequence3.sv index 091240018..b0037fb2a 100644 --- a/regression/verilog/SVA/cover_sequence3.sv +++ b/regression/verilog/SVA/cover_sequence3.sv @@ -7,12 +7,12 @@ module main(input clk); x++; // passes with bound >=9 - p0: cover property (1[*10]); + p0: cover sequence (1[*10]); // passes with bound >=3 - p1: cover property (1[*4:10]); + p1: cover sequence (1[*4:10]); // passes with bound >=4 - p2: cover property (1[*5:10]); + p2: cover sequence (1[*5:10]); endmodule diff --git a/regression/verilog/SVA/cover_sequence4.sv b/regression/verilog/SVA/cover_sequence4.sv index 9c08ffb5a..24fa91fc4 100644 --- a/regression/verilog/SVA/cover_sequence4.sv +++ b/regression/verilog/SVA/cover_sequence4.sv @@ -7,12 +7,12 @@ module main(input clk); x++; // passes with bound >=9 - p0: cover property (1[=10]); + p0: cover sequence (1[=10]); // passes with bound >=3 - p1: cover property (1[=4:10]); + p1: cover sequence (1[=4:10]); // passes with bound >=4 - p2: cover property (1[=5:10]); + p2: cover sequence (1[=5:10]); endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index b1e5f0a41..912591f66 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -69,6 +69,7 @@ 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_disable_iff) IREP_ID_ONE(sva_sequence_first_match) IREP_ID_ONE(sva_sequence_goto_repetition) IREP_ID_ONE(sva_sequence_intersect) @@ -210,6 +211,7 @@ IREP_ID_ONE(verilog_immediate_cover) IREP_ID_ONE(verilog_assert_property) IREP_ID_ONE(verilog_assume_property) IREP_ID_ONE(verilog_cover_property) +IREP_ID_ONE(verilog_cover_sequence) IREP_ID_ONE(verilog_covergroup) IREP_ID_ONE(verilog_restrict_property) IREP_ID_ONE(verilog_expect_property) diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index 2ae4155f1..bdb3ddf1d 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -112,7 +112,8 @@ bool is_SVA_sequence_operator(const exprt &expr) id == ID_sva_sequence_goto_repetition || id == ID_sva_sequence_non_consecutive_repetition || id == ID_sva_sequence_repetition_star || - id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean; + id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean || + id == ID_sva_sequence_disable_iff; } bool is_SVA_operator(const exprt &expr) diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp index 6eadfdc17..be055bc1a 100644 --- a/src/temporal-logic/trivial_sva.cpp +++ b/src/temporal-logic/trivial_sva.cpp @@ -110,6 +110,14 @@ exprt trivial_sva(exprt expr) 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_sequence_disable_iff) + { + auto &disable_iff_expr = to_sva_sequence_disable_iff_expr(expr); + expr = sva_or_exprt{ + sva_boolean_exprt{disable_iff_expr.lhs(), verilog_sva_sequence_typet{}}, + disable_iff_expr.rhs(), + verilog_sva_sequence_typet{}}; + } else if(expr.id() == ID_sva_accept_on || expr.id() == ID_sva_sync_accept_on) { auto &sva_abort_expr = to_sva_abort_expr(expr); diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 216c8c9d4..7bacf2ed0 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -680,10 +680,10 @@ Function: expr2verilogt::convert_sva_abort expr2verilogt::resultt expr2verilogt::convert_sva_abort( const std::string &text, - const sva_abort_exprt &expr) + const binary_exprt &expr) { - auto op0 = convert_rec(expr.condition()); - auto op1 = convert_rec(expr.property()); + auto op0 = convert_rec(expr.op0()); + auto op1 = convert_rec(expr.op1()); return {verilog_precedencet::MIN, text + " (" + op0.s + ") " + op1.s}; } @@ -1937,6 +1937,11 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) return precedence = verilog_precedencet::MIN, convert_sva_abort("disable iff", to_sva_abort_expr(src)); + else if(src.id() == ID_sva_sequence_disable_iff) + return precedence = verilog_precedencet::MIN, + convert_sva_abort( + "disable iff", to_sva_sequence_disable_iff_expr(src)); + else if(src.id()==ID_sva_eventually) { return precedence = verilog_precedencet::MIN, diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 1a1a96693..77ad41adb 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class sva_abort_exprt; class sva_case_exprt; class sva_if_exprt; class sva_ranged_predicate_exprt; @@ -145,7 +144,7 @@ class expr2verilogt const std::string &name, const sva_sequence_repetition_exprt &); - resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &); + resultt convert_sva_abort(const std::string &name, const binary_exprt &); resultt convert_sva_indexed_binary(const std::string &name, const binary_exprt &); diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 583fb82d8..61e5b98d9 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -2408,6 +2408,7 @@ concurrent_assertion_statement: assert_property_statement | assume_property_statement | cover_property_statement + | cover_sequence_statement | restrict_property_statement ; @@ -2470,6 +2471,15 @@ cover_property_statement: TOK_COVER TOK_PROPERTY '(' property_spec ')' action_bl { init($$, ID_verilog_cover_property); mto($$, $4); mto($$, $6); } ; +cover_sequence_statement: + TOK_COVER TOK_SEQUENCE '(' sequence_expr ')' action_block + { init($$, ID_verilog_cover_sequence); mto2($$, $4, $6); } + | TOK_COVER TOK_SEQUENCE '(' clocking_event TOK_DISABLE TOK_IFF '(' expression ')' sequence_expr ')' action_block + { init($5, ID_sva_sequence_disable_iff); mto2($5, $8, $10); init($$, ID_verilog_cover_sequence); mto2($$, $5, $12); } + | TOK_COVER TOK_SEQUENCE '(' TOK_DISABLE TOK_IFF '(' expression ')' sequence_expr ')' action_block + { init($4, ID_sva_sequence_disable_iff); mto2($4, $7, $9); init($$, ID_verilog_cover_sequence); mto2($$, $4, $11); } + ; + restrict_property_statement: TOK_RESTRICT TOK_PROPERTY '(' property_spec ')' ';' { init($$, ID_verilog_restrict_property); mto($$, $4); mto($$, $6); } ; diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 6282c7804..8e3baa35b 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -36,6 +36,58 @@ static inline sva_boolean_exprt &to_sva_boolean_expr(exprt &expr) return static_cast(expr); } +/// disable_iff for cover sequence +class sva_sequence_disable_iff_exprt : public binary_exprt +{ +public: + sva_sequence_disable_iff_exprt(exprt condition, exprt sequence) + : binary_exprt( + std::move(condition), + ID_sva_sequence_disable_iff, + std::move(sequence), + verilog_sva_sequence_typet{}) + { + } + + const exprt &condition() const + { + return op0(); + } + + exprt &condition() + { + return op0(); + } + + const exprt &sequence() const + { + return op1(); + } + + exprt &sequence() + { + return op1(); + } + +protected: + using binary_exprt::op0; + using binary_exprt::op1; +}; + +static inline const sva_sequence_disable_iff_exprt & +to_sva_sequence_disable_iff_expr(const exprt &expr) +{ + sva_sequence_disable_iff_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_sequence_disable_iff_exprt & +to_sva_sequence_disable_iff_expr(exprt &expr) +{ + sva_sequence_disable_iff_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_exprt { diff --git a/src/verilog/verilog_elaborate.cpp b/src/verilog/verilog_elaborate.cpp index fa17ed612..41633f528 100644 --- a/src/verilog/verilog_elaborate.cpp +++ b/src/verilog/verilog_elaborate.cpp @@ -671,6 +671,7 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement) statement.id() == ID_verilog_assume_property || statement.id() == ID_verilog_restrict_property || statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence || statement.id() == ID_verilog_expect_property) { } @@ -850,7 +851,8 @@ void verilog_typecheckt::collect_symbols( module_item.id() == ID_verilog_assert_property || module_item.id() == ID_verilog_assume_property || module_item.id() == ID_verilog_restrict_property || - module_item.id() == ID_verilog_cover_property) + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) { } else if(module_item.id() == ID_verilog_assertion_item) diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 3a359986a..f1ca0e9d3 100644 --- a/src/verilog/verilog_expr.cpp +++ b/src/verilog/verilog_expr.cpp @@ -201,7 +201,8 @@ static void dependencies_rec( module_item.id() == ID_verilog_assert_property || module_item.id() == ID_verilog_assume_property || module_item.id() == ID_verilog_restrict_property || - module_item.id() == ID_verilog_cover_property) + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) { } else if(module_item.id() == ID_verilog_assertion_item) diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 9f7b197c3..0ce9ecca2 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2061,7 +2061,8 @@ to_verilog_assert_assume_cover_module_item( module_item.id() == ID_verilog_assert_property || module_item.id() == ID_verilog_assume_property || module_item.id() == ID_verilog_restrict_property || - module_item.id() == ID_verilog_cover_property); + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence); binary_exprt::check(module_item); return static_cast( module_item); @@ -2074,7 +2075,8 @@ to_verilog_assert_assume_cover_module_item(verilog_module_itemt &module_item) module_item.id() == ID_verilog_assert_property || module_item.id() == ID_verilog_assume_property || module_item.id() == ID_verilog_restrict_property || - module_item.id() == ID_verilog_cover_property); + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence); binary_exprt::check(module_item); return static_cast(module_item); } @@ -2124,7 +2126,8 @@ to_verilog_assert_assume_cover_statement(const verilog_statementt &statement) statement.id() == ID_verilog_restrict_property || statement.id() == ID_verilog_smv_assume || statement.id() == ID_verilog_immediate_cover || - statement.id() == ID_verilog_cover_property); + statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence); binary_exprt::check(statement); return static_cast(statement); } @@ -2141,7 +2144,8 @@ to_verilog_assert_assume_cover_statement(verilog_statementt &statement) statement.id() == ID_verilog_restrict_property || statement.id() == ID_verilog_smv_assume || statement.id() == ID_verilog_immediate_cover || - statement.id() == ID_verilog_cover_property); + statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence); binary_exprt::check(statement); return static_cast(statement); } diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp index a1d1e9358..e9ff6f54b 100644 --- a/src/verilog/verilog_interfaces.cpp +++ b/src/verilog/verilog_interfaces.cpp @@ -285,7 +285,8 @@ void verilog_typecheckt::interface_module_item( module_item.id() == ID_verilog_assert_property || module_item.id() == ID_verilog_assume_property || module_item.id() == ID_verilog_restrict_property || - module_item.id() == ID_verilog_cover_property) + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) { // done later } diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 06325b559..e8ccf9be9 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -2299,6 +2299,7 @@ void verilog_synthesist::synth_assert_assume_cover( // one of the 'always' variants -- assertions and assumptions have an implicit 'always' if( statement.id() != ID_verilog_cover_property && + statement.id() != ID_verilog_cover_sequence && statement.id() != ID_verilog_immediate_cover) { if(cond_for_comment.id() != ID_sva_always) @@ -2315,7 +2316,9 @@ void verilog_synthesist::synth_assert_assume_cover( { cond_for_comment = sva_assume_exprt(cond_for_comment); } - else if(statement.id() == ID_verilog_cover_property) + else if( + statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence) { // 'cover' properties are existential cond_for_comment = sva_cover_exprt(cond_for_comment); @@ -2355,6 +2358,7 @@ void verilog_synthesist::synth_assert_assume_cover( // assertions and assumptions have an implicit 'always' if( statement.id() != ID_verilog_cover_property && + statement.id() != ID_verilog_cover_sequence && statement.id() != ID_verilog_immediate_cover) { if(cond.id() != ID_sva_always) @@ -2374,14 +2378,25 @@ void verilog_synthesist::synth_assert_assume_cover( else if(statement.id() == ID_verilog_cover_property) { // 'cover' properties are existential - cond = sva_cover_exprt(cond); + cond = sva_cover_exprt{cond}; + } + else if(statement.id() == ID_verilog_cover_sequence) + { + // 'cover' properties are existential + cond = sva_cover_exprt{sva_sequence_property_exprt{cond}}; } // 1800-2017 16.12.2 Sequence property - if(statement.id() == ID_verilog_cover_property) + if( + statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence) + { set_default_sequence_semantics(cond, sva_sequence_semanticst::STRONG); + } else + { set_default_sequence_semantics(cond, sva_sequence_semanticst::WEAK); + } symbol.value = std::move(cond); } @@ -2418,7 +2433,9 @@ void verilog_synthesist::synth_assert_assume_cover( if(cond_for_comment.id() != ID_sva_always) cond_for_comment = sva_always_exprt{cond_for_comment}; } - else if(module_item.id() == ID_verilog_cover_property) + else if( + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) { // 'cover' requirements are existential. cond_for_comment = sva_cover_exprt{cond_for_comment}; @@ -2455,14 +2472,25 @@ void verilog_synthesist::synth_assert_assume_cover( // 'cover' requirements are existential. cond = sva_cover_exprt{cond}; } + else if(module_item.id() == ID_verilog_cover_sequence) + { + // 'cover' requirements are existential. + cond = sva_cover_exprt{sva_sequence_property_exprt{cond}}; + } else PRECONDITION(false); // 1800-2017 16.12.2 Sequence property - if(module_item.id() == ID_verilog_cover_property) + if( + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) + { set_default_sequence_semantics(cond, sva_sequence_semanticst::STRONG); + } else + { set_default_sequence_semantics(cond, sva_sequence_semanticst::WEAK); + } symbol.value = std::move(cond); } @@ -3195,7 +3223,8 @@ void verilog_synthesist::synth_statement( statement.id() == ID_verilog_immediate_assert || statement.id() == ID_verilog_assert_property || statement.id() == ID_verilog_smv_assert || - statement.id() == ID_verilog_cover_property) + statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence) { synth_assert_assume_cover( to_verilog_assert_assume_cover_statement(statement)); @@ -3331,7 +3360,8 @@ void verilog_synthesist::synth_module_item( } else if( module_item.id() == ID_verilog_assert_property || - module_item.id() == ID_verilog_cover_property) + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) { synth_assert_assume_cover( to_verilog_assert_assume_cover_module_item(module_item)); diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 0c9a845d5..3784a9b10 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1041,7 +1041,11 @@ void verilog_typecheckt::convert_assert_assume_cover( exprt &cond = module_item.condition(); convert_sva(cond); - require_sva_property(cond); + + if(module_item.id() == ID_verilog_cover_sequence) + require_sva_sequence(cond); + else + require_sva_property(cond); // We create a symbol for the property. // The 'value' of the symbol is set by synthesis. @@ -1056,6 +1060,7 @@ void verilog_typecheckt::convert_assert_assume_cover( : module_item.id() == ID_verilog_assume_property ? "assume" : module_item.id() == ID_verilog_cover_property ? "cover" + : module_item.id() == ID_verilog_cover_sequence ? "cover" : ""; assertion_counter++; @@ -1106,7 +1111,11 @@ void verilog_typecheckt::convert_assert_assume_cover( exprt &cond = statement.condition(); convert_sva(cond); - require_sva_property(cond); + + if(statement.id() == ID_verilog_cover_sequence) + require_sva_sequence(cond); + else + require_sva_property(cond); // We create a symbol for the property. // The 'value' is set by synthesis. @@ -1120,6 +1129,7 @@ void verilog_typecheckt::convert_assert_assume_cover( : statement.id() == ID_verilog_assert_property ? "assert" : statement.id() == ID_verilog_smv_assert ? "assert" : statement.id() == ID_verilog_cover_property ? "cover" + : statement.id() == ID_verilog_cover_sequence ? "cover" : statement.id() == ID_verilog_immediate_assume ? "assume" : statement.id() == ID_verilog_assume_property ? "assume" @@ -1525,7 +1535,8 @@ void verilog_typecheckt::convert_statement( statement.id() == ID_verilog_immediate_assert || statement.id() == ID_verilog_assert_property || statement.id() == ID_verilog_smv_assert || - statement.id() == ID_verilog_cover_property) + statement.id() == ID_verilog_cover_property || + statement.id() == ID_verilog_cover_sequence) { convert_assert_assume_cover( to_verilog_assert_assume_cover_statement(statement)); @@ -1541,9 +1552,6 @@ void verilog_typecheckt::convert_statement( { convert_assert_assume_cover(to_verilog_assume_statement(statement)); } - else if(statement.id() == ID_verilog_cover_property) - { - } else if(statement.id() == ID_verilog_non_blocking_assign) convert_assign(to_verilog_assign(statement), false); else if(statement.id()==ID_if) @@ -1585,6 +1593,7 @@ void verilog_typecheckt::convert_statement( sub_statement.id() == ID_verilog_assert_property || sub_statement.id() == ID_verilog_assume_property || sub_statement.id() == ID_verilog_restrict_property || + sub_statement.id() == ID_verilog_cover_sequence || sub_statement.id() == ID_verilog_cover_property) { sub_statement.set(ID_identifier, label_statement.label()); @@ -1664,7 +1673,8 @@ void verilog_typecheckt::convert_module_item( module_item.id() == ID_verilog_assert_property || module_item.id() == ID_verilog_assume_property || module_item.id() == ID_verilog_restrict_property || - module_item.id() == ID_verilog_cover_property) + module_item.id() == ID_verilog_cover_property || + module_item.id() == ID_verilog_cover_sequence) { convert_assert_assume_cover( to_verilog_assert_assume_cover_module_item(module_item)); diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 747ccf60f..777cf445c 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -167,6 +167,21 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) return std::move(expr); } + else if(expr.id() == ID_sva_sequence_disable_iff) + { + auto &disable_iff = to_sva_sequence_disable_iff_expr(expr); + + // The condition of these is special: They are not sampled, + // but evaluated directly (1800-2017 16.6). + convert_expr(disable_iff.condition()); + make_boolean(disable_iff.condition()); + + convert_sva(disable_iff.sequence()); + require_sva_sequence(disable_iff.sequence()); + expr.type() = verilog_sva_sequence_typet{}; + + return std::move(expr); + } else if( expr.id() == ID_sva_cycle_delay_plus || // ##[+] expr.id() == ID_sva_cycle_delay_star) // ##[*]