From ca996d15c098587c7300a3c2b76fc6668277106a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 23 Apr 2025 09:22:33 -0700 Subject: [PATCH] introduce verilog_sva_property_typet This introduces a type for Verilog SVA properties to distinguish properties from state predicates and sequences. --- regression/verilog/SVA/named_property1.desc | 8 + regression/verilog/SVA/named_property1.sv | 15 ++ src/hw_cbmc_irep_ids.h | 1 + src/temporal-logic/ltl_sva_to_string.cpp | 8 +- src/temporal-logic/normalize_property.cpp | 23 +- src/temporal-logic/sva_to_ltl.cpp | 32 +++ src/temporal-logic/trivial_sva.cpp | 4 + src/verilog/sva_expr.cpp | 6 + src/verilog/sva_expr.h | 261 +++++++++++++++----- src/verilog/verilog_typecheck.cpp | 3 +- src/verilog/verilog_typecheck_sva.cpp | 33 ++- src/verilog/verilog_types.h | 9 + 12 files changed, 313 insertions(+), 90 deletions(-) create mode 100644 regression/verilog/SVA/named_property1.desc create mode 100644 regression/verilog/SVA/named_property1.sv diff --git a/regression/verilog/SVA/named_property1.desc b/regression/verilog/SVA/named_property1.desc new file mode 100644 index 000000000..72673abb6 --- /dev/null +++ b/regression/verilog/SVA/named_property1.desc @@ -0,0 +1,8 @@ +CORE +named_property1.sv + +^file .* line 12: sequence required, but got property$ +^EXIT=2$ +^SIGNAL=0$ +-- +-- diff --git a/regression/verilog/SVA/named_property1.sv b/regression/verilog/SVA/named_property1.sv new file mode 100644 index 000000000..489055b30 --- /dev/null +++ b/regression/verilog/SVA/named_property1.sv @@ -0,0 +1,15 @@ +module main(input clk); + + wire [31:0] x = 10; + + property x_is_ten; + x == 10 + endproperty : x_is_ten + + // Cannot be used as a sequence, even when it syntactically + // qualifies as a sequence. + sequence some_sequence; + x_is_ten + endsequence + +endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index c2f4ddd0d..8d37e95fe 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -147,6 +147,7 @@ IREP_ID_ONE(verilog_null) IREP_ID_ONE(verilog_event) IREP_ID_ONE(verilog_event_trigger) IREP_ID_ONE(verilog_string) +IREP_ID_ONE(verilog_sva_property) IREP_ID_ONE(verilog_sva_sequence) IREP_ID_ONE(reg) IREP_ID_ONE(macromodule) diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp index 42f136708..f69b97352 100644 --- a/src/temporal-logic/ltl_sva_to_string.cpp +++ b/src/temporal-logic/ltl_sva_to_string.cpp @@ -250,8 +250,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) auto &followed_by = to_sva_followed_by_expr(expr); auto not_b = not_exprt{followed_by.consequent()}; return rec( - not_exprt{ - sva_overlapped_implication_exprt{followed_by.antecedent(), not_b}}, + not_exprt{sva_overlapped_implication_exprt{ + followed_by.antecedent(), not_b, bool_typet{}}}, mode); } else if(expr.id() == ID_sva_nonoverlapped_followed_by) @@ -262,8 +262,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode) auto &followed_by = to_sva_followed_by_expr(expr); auto not_b = not_exprt{followed_by.consequent()}; return rec( - not_exprt{ - sva_non_overlapped_implication_exprt{followed_by.antecedent(), not_b}}, + not_exprt{sva_non_overlapped_implication_exprt{ + followed_by.antecedent(), not_b, bool_typet{}}}, mode); } else if(expr.id() == ID_sva_sequence_property) diff --git a/src/temporal-logic/normalize_property.cpp b/src/temporal-logic/normalize_property.cpp index c55479ebb..0124b6203 100644 --- a/src/temporal-logic/normalize_property.cpp +++ b/src/temporal-logic/normalize_property.cpp @@ -27,8 +27,9 @@ exprt normalize_pre_sva_non_overlapped_implication( { const auto &lhs_cond = to_sva_boolean_expr(expr.lhs()).op(); auto one = natural_typet{}.one_expr(); - return or_exprt{ - not_exprt{lhs_cond}, sva_ranged_always_exprt{one, one, expr.rhs()}}; + auto ranged_always = sva_ranged_always_exprt{one, one, expr.rhs()}; + ranged_always.type() = bool_typet{}; + return or_exprt{not_exprt{lhs_cond}, ranged_always}; } else return std::move(expr); @@ -63,24 +64,32 @@ exprt normalize_property_rec(exprt expr) else if(expr.id() == ID_sva_nexttime) { auto one = natural_typet{}.one_expr(); - expr = sva_ranged_always_exprt{one, one, to_sva_nexttime_expr(expr).op()}; + expr = sva_ranged_always_exprt{ + one, one, to_sva_nexttime_expr(expr).op(), bool_typet{}}; } else if(expr.id() == ID_sva_s_nexttime) { auto one = natural_typet{}.one_expr(); - expr = sva_s_always_exprt{one, one, to_sva_s_nexttime_expr(expr).op()}; + expr = sva_s_always_exprt{ + one, one, to_sva_s_nexttime_expr(expr).op(), bool_typet{}}; } else if(expr.id() == ID_sva_indexed_nexttime) { auto &nexttime_expr = to_sva_indexed_nexttime_expr(expr); expr = sva_ranged_always_exprt{ - nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; + nexttime_expr.index(), + nexttime_expr.index(), + nexttime_expr.op(), + bool_typet{}}; } else if(expr.id() == ID_sva_indexed_s_nexttime) { auto &nexttime_expr = to_sva_indexed_s_nexttime_expr(expr); expr = sva_s_always_exprt{ - nexttime_expr.index(), nexttime_expr.index(), nexttime_expr.op()}; + nexttime_expr.index(), + nexttime_expr.index(), + nexttime_expr.op(), + bool_typet{}}; } // normalize the operands @@ -104,7 +113,7 @@ exprt normalize_property(exprt expr) { // top-level only if(expr.id() == ID_sva_cover) - expr = sva_always_exprt{not_exprt{to_sva_cover_expr(expr).op()}}; + expr = sva_always_exprt{sva_not_exprt{to_sva_cover_expr(expr).op()}}; expr = trivial_sva(expr); diff --git a/src/temporal-logic/sva_to_ltl.cpp b/src/temporal-logic/sva_to_ltl.cpp index 97341b712..00e4cbb9f 100644 --- a/src/temporal-logic/sva_to_ltl.cpp +++ b/src/temporal-logic/sva_to_ltl.cpp @@ -238,6 +238,38 @@ exprt SVA_to_LTL(exprt expr) { return expr; } + else if(expr.id() == ID_sva_implies) + { + // maps cleanly to 'implies' + auto &sva_implies = to_sva_implies_expr(expr); + auto rec_lhs = SVA_to_LTL(sva_implies.lhs()); + auto rec_rhs = SVA_to_LTL(sva_implies.rhs()); + return implies_exprt{rec_rhs, rec_lhs}; + } + else if(expr.id() == ID_sva_iff) + { + // maps cleanly to = + auto &sva_iff = to_sva_iff_expr(expr); + auto rec_lhs = SVA_to_LTL(sva_iff.lhs()); + auto rec_rhs = SVA_to_LTL(sva_iff.rhs()); + return equal_exprt{rec_rhs, rec_lhs}; + } + else if(expr.id() == ID_sva_and) + { + // maps cleanly to Boolean and + auto &sva_iff = to_sva_iff_expr(expr); + auto rec_lhs = SVA_to_LTL(sva_iff.lhs()); + auto rec_rhs = SVA_to_LTL(sva_iff.rhs()); + return and_exprt{rec_rhs, rec_lhs}; + } + else if(expr.id() == ID_sva_or) + { + // maps cleanly to Boolean or + auto &sva_iff = to_sva_iff_expr(expr); + auto rec_lhs = SVA_to_LTL(sva_iff.lhs()); + auto rec_rhs = SVA_to_LTL(sva_iff.rhs()); + return or_exprt{rec_rhs, rec_lhs}; + } else if( expr.id() == ID_and || expr.id() == ID_implies || expr.id() == ID_or || expr.id() == ID_not) diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp index 9aceba725..6eadfdc17 100644 --- a/src/temporal-logic/trivial_sva.cpp +++ b/src/temporal-logic/trivial_sva.cpp @@ -23,6 +23,10 @@ static std::optional is_state_predicate(const exprt &expr) exprt trivial_sva(exprt expr) { // pre-traversal + if(expr.type().id() == ID_verilog_sva_property) + { + expr.type() = bool_typet{}; + } // rewrite the operands, recursively for(auto &op : expr.operands()) diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp index 223ab386d..7b9b2d28a 100644 --- a/src/verilog/sva_expr.cpp +++ b/src/verilog/sva_expr.cpp @@ -11,6 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +exprt sva_iff_exprt::implications() const +{ + return sva_and_exprt{ + sva_implies_exprt{lhs(), rhs()}, sva_implies_exprt{rhs(), lhs()}, type()}; +} + exprt sva_cycle_delay_plus_exprt::lower() const { // same as ##[1:$] diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index 9b3f68a2e..d0ab309e9 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -37,11 +37,15 @@ static inline sva_boolean_exprt &to_sva_boolean_expr(exprt &expr) } /// accept_on, reject_on, sync_accept_on, sync_reject_on, disable_iff -class sva_abort_exprt : public binary_predicate_exprt +class sva_abort_exprt : public binary_exprt { public: sva_abort_exprt(irep_idt id, exprt condition, exprt property) - : binary_predicate_exprt(std::move(condition), id, std::move(property)) + : binary_exprt( + std::move(condition), + id, + std::move(property), + verilog_sva_property_typet{}) { } @@ -66,8 +70,8 @@ class sva_abort_exprt : public binary_predicate_exprt } protected: - using binary_predicate_exprt::op0; - using binary_predicate_exprt::op1; + using binary_exprt::op0; + using binary_exprt::op1; }; static inline const sva_abort_exprt &to_sva_abort_expr(const exprt &expr) @@ -110,11 +114,11 @@ static inline sva_disable_iff_exprt &to_sva_disable_iff_expr(exprt &expr) } /// nonindexed variant -class sva_nexttime_exprt : public unary_predicate_exprt +class sva_nexttime_exprt : public unary_exprt { public: explicit sva_nexttime_exprt(exprt op) - : unary_predicate_exprt(ID_sva_nexttime, std::move(op)) + : unary_exprt(ID_sva_nexttime, std::move(op), verilog_sva_property_typet{}) { } }; @@ -134,11 +138,14 @@ static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr) } /// nonindexed variant -class sva_s_nexttime_exprt : public unary_predicate_exprt +class sva_s_nexttime_exprt : public unary_exprt { public: explicit sva_s_nexttime_exprt(exprt op) - : unary_predicate_exprt(ID_sva_s_nexttime, std::move(op)) + : unary_exprt( + ID_sva_s_nexttime, + std::move(op), + verilog_sva_property_typet{}) { } }; @@ -159,14 +166,15 @@ static inline sva_s_nexttime_exprt &to_sva_s_nexttime_expr(exprt &expr) } /// indexed variant of sva_nexttime_exprt -class sva_indexed_nexttime_exprt : public binary_predicate_exprt +class sva_indexed_nexttime_exprt : public binary_exprt { public: sva_indexed_nexttime_exprt(constant_exprt index, exprt op) - : binary_predicate_exprt( + : binary_exprt( std::move(index), ID_sva_indexed_nexttime, - std::move(op)) + std::move(op), + verilog_sva_property_typet{}) { } @@ -191,8 +199,8 @@ class sva_indexed_nexttime_exprt : public binary_predicate_exprt } protected: - using binary_predicate_exprt::op0; - using binary_predicate_exprt::op1; + using binary_exprt::op0; + using binary_exprt::op1; }; static inline const sva_indexed_nexttime_exprt & @@ -212,14 +220,15 @@ to_sva_indexed_nexttime_expr(exprt &expr) } /// indexed variant of sva_s_nexttime_exprt -class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt +class sva_indexed_s_nexttime_exprt : public binary_exprt { public: sva_indexed_s_nexttime_exprt(constant_exprt index, exprt op) - : binary_predicate_exprt( + : binary_exprt( std::move(index), ID_sva_indexed_s_nexttime, - std::move(op)) + std::move(op), + verilog_sva_property_typet{}) { } @@ -244,8 +253,8 @@ class sva_indexed_s_nexttime_exprt : public binary_predicate_exprt } protected: - using binary_predicate_exprt::op0; - using binary_predicate_exprt::op1; + using binary_exprt::op0; + using binary_exprt::op1; }; static inline const sva_indexed_s_nexttime_exprt & @@ -280,7 +289,22 @@ class sva_ranged_predicate_exprt : public ternary_exprt std::move(__from), std::move(__to), std::move(__op), - bool_typet{}) + verilog_sva_property_typet{}) + { + } + + sva_ranged_predicate_exprt( + irep_idt __id, + constant_exprt __from, + exprt __to, + exprt __op, + typet __type) + : ternary_exprt( + __id, + std::move(__from), + std::move(__to), + std::move(__op), + std::move(__type)) { } @@ -362,6 +386,21 @@ class sva_bounded_range_predicate_exprt : public sva_ranged_predicate_exprt { } + sva_bounded_range_predicate_exprt( + irep_idt __id, + constant_exprt __from, + constant_exprt __to, + exprt __op, + typet __type) + : sva_ranged_predicate_exprt( + __id, + std::move(__from), + std::move(__to), + std::move(__op), + std::move(__type)) + { + } + const constant_exprt &to() const { return static_cast( @@ -402,11 +441,14 @@ static inline sva_eventually_exprt &to_sva_eventually_expr(exprt &expr) return static_cast(expr); } -class sva_s_eventually_exprt : public unary_predicate_exprt +class sva_s_eventually_exprt : public unary_exprt { public: explicit sva_s_eventually_exprt(exprt op) - : unary_predicate_exprt(ID_sva_s_eventually, std::move(op)) + : unary_exprt( + ID_sva_s_eventually, + std::move(op), + verilog_sva_property_typet{}) { } }; @@ -458,11 +500,11 @@ to_sva_ranged_s_eventually_expr(exprt &expr) return static_cast(expr); } -class sva_always_exprt : public unary_predicate_exprt +class sva_always_exprt : public unary_exprt { public: explicit sva_always_exprt(exprt op) - : unary_predicate_exprt(ID_sva_always, std::move(op)) + : unary_exprt(ID_sva_always, std::move(op), verilog_sva_property_typet{}) { } }; @@ -492,6 +534,16 @@ class sva_ranged_always_exprt : public sva_ranged_predicate_exprt std::move(op)) { } + + sva_ranged_always_exprt(constant_exprt from, exprt to, exprt op, typet __type) + : sva_ranged_predicate_exprt( + ID_sva_ranged_always, + std::move(from), + std::move(to), + std::move(op), + std::move(__type)) + { + } }; static inline const sva_ranged_always_exprt & @@ -520,6 +572,20 @@ class sva_s_always_exprt : public sva_bounded_range_predicate_exprt std::move(op)) { } + + sva_s_always_exprt( + constant_exprt from, + constant_exprt to, + exprt op, + typet __type) + : sva_bounded_range_predicate_exprt( + ID_sva_s_always, + std::move(from), + std::move(to), + std::move(op), + std::move(__type)) + { + } }; static inline const sva_s_always_exprt &to_sva_s_always_expr(const exprt &expr) @@ -536,11 +602,11 @@ static inline sva_s_always_exprt &to_sva_s_always_expr(exprt &expr) return static_cast(expr); } -class sva_cover_exprt : public unary_predicate_exprt +class sva_cover_exprt : public unary_exprt { public: explicit sva_cover_exprt(exprt op) - : unary_predicate_exprt(ID_sva_cover, std::move(op)) + : unary_exprt(ID_sva_cover, std::move(op), verilog_sva_property_typet{}) { } }; @@ -559,11 +625,11 @@ static inline sva_cover_exprt &to_sva_cover_expr(exprt &expr) return static_cast(expr); } -class sva_assume_exprt : public unary_predicate_exprt +class sva_assume_exprt : public unary_exprt { public: explicit sva_assume_exprt(exprt op) - : unary_predicate_exprt(ID_sva_assume, std::move(op)) + : unary_exprt(ID_sva_assume, std::move(op), verilog_sva_property_typet{}) { } }; @@ -582,11 +648,15 @@ static inline sva_assume_exprt &to_sva_assume_expr(exprt &expr) return static_cast(expr); } -class sva_until_exprt : public binary_predicate_exprt +class sva_until_exprt : public binary_exprt { public: explicit sva_until_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_until, std::move(op1)) + : binary_exprt( + std::move(op0), + ID_sva_until, + std::move(op1), + verilog_sva_property_typet{}) { } }; @@ -605,11 +675,15 @@ static inline sva_until_exprt &to_sva_until_expr(exprt &expr) return static_cast(expr); } -class sva_s_until_exprt : public binary_predicate_exprt +class sva_s_until_exprt : public binary_exprt { public: explicit sva_s_until_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_s_until, std::move(op1)) + : binary_exprt( + std::move(op0), + ID_sva_s_until, + std::move(op1), + verilog_sva_property_typet{}) { } }; @@ -629,11 +703,15 @@ static inline sva_s_until_exprt &to_sva_s_until_expr(exprt &expr) } /// SVA until_with operator -- like LTL (weak) R, but lhs/rhs swapped -class sva_until_with_exprt : public binary_predicate_exprt +class sva_until_with_exprt : public binary_exprt { public: explicit sva_until_with_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_until_with, std::move(op1)) + : binary_exprt( + std::move(op0), + ID_sva_until_with, + std::move(op1), + verilog_sva_property_typet{}) { } }; @@ -654,14 +732,15 @@ static inline sva_until_with_exprt &to_sva_until_with_expr(exprt &expr) } /// SVA s_until_with operator -- like LTL strong R, but lhs/rhs swapped -class sva_s_until_with_exprt : public binary_predicate_exprt +class sva_s_until_with_exprt : public binary_exprt { public: explicit sva_s_until_with_exprt(exprt op0, exprt op1) - : binary_predicate_exprt( + : binary_exprt( std::move(op0), ID_sva_s_until_with, - std::move(op1)) + std::move(op1), + verilog_sva_property_typet{}) { } }; @@ -682,17 +761,31 @@ static inline sva_s_until_with_exprt &to_sva_s_until_with_expr(exprt &expr) } /// base class for |->, |=>, #-#, #=# -class sva_implication_base_exprt : public binary_predicate_exprt +class sva_implication_base_exprt : public binary_exprt { public: - explicit sva_implication_base_exprt( + sva_implication_base_exprt( exprt __antecedent, irep_idt __id, exprt __consequent) - : binary_predicate_exprt( + : binary_exprt( std::move(__antecedent), __id, - std::move(__consequent)) + std::move(__consequent), + verilog_sva_property_typet{}) + { + } + + sva_implication_base_exprt( + exprt __antecedent, + irep_idt __id, + exprt __consequent, + typet __type) + : binary_exprt( + std::move(__antecedent), + __id, + std::move(__consequent), + std::move(__type)) { } @@ -757,15 +850,25 @@ to_sva_implication_base_expr(exprt &expr) class sva_overlapped_implication_exprt : public sva_implication_base_exprt { public: - explicit sva_overlapped_implication_exprt( - exprt __antecedent, - exprt __consequent) + sva_overlapped_implication_exprt(exprt __antecedent, exprt __consequent) : sva_implication_base_exprt( std::move(__antecedent), ID_sva_overlapped_implication, std::move(__consequent)) { } + + sva_overlapped_implication_exprt( + exprt __antecedent, + exprt __consequent, + typet __type) + : sva_implication_base_exprt( + std::move(__antecedent), + ID_sva_overlapped_implication, + std::move(__consequent), + std::move(__type)) + { + } }; static inline const sva_overlapped_implication_exprt & @@ -788,15 +891,25 @@ to_sva_overlapped_implication_expr(exprt &expr) class sva_non_overlapped_implication_exprt : public sva_implication_base_exprt { public: - explicit sva_non_overlapped_implication_exprt( - exprt __antecedent, - exprt __consequent) + sva_non_overlapped_implication_exprt(exprt __antecedent, exprt __consequent) : sva_implication_base_exprt( std::move(__antecedent), ID_sva_non_overlapped_implication, std::move(__consequent)) { } + + sva_non_overlapped_implication_exprt( + exprt __antecedent, + exprt __consequent, + typet __type) + : sva_implication_base_exprt( + std::move(__antecedent), + ID_sva_non_overlapped_implication, + std::move(__consequent), + std::move(__type)) + { + } }; static inline const sva_non_overlapped_implication_exprt & @@ -815,11 +928,11 @@ to_sva_non_overlapped_implication_expr(exprt &expr) return static_cast(expr); } -class sva_not_exprt : public unary_predicate_exprt +class sva_not_exprt : public unary_exprt { public: explicit sva_not_exprt(exprt op) - : unary_predicate_exprt(ID_sva_not, std::move(op)) + : unary_exprt(ID_sva_not, std::move(op), verilog_sva_property_typet{}) { } }; @@ -841,8 +954,13 @@ static inline sva_not_exprt &to_sva_not_expr(exprt &expr) class sva_and_exprt : public binary_exprt { public: - explicit sva_and_exprt(exprt op0, exprt op1, typet type) - : binary_exprt(std::move(op0), ID_sva_and, std::move(op1), std::move(type)) + // can be a sequence or property, depending on operands + explicit sva_and_exprt(exprt op0, exprt op1, typet __type) + : binary_exprt( + std::move(op0), + ID_sva_and, + std::move(op1), + std::move(__type)) { } }; @@ -861,13 +979,20 @@ static inline sva_and_exprt &to_sva_and_expr(exprt &expr) return static_cast(expr); } -class sva_iff_exprt : public binary_predicate_exprt +class sva_iff_exprt : public binary_exprt { public: explicit sva_iff_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_iff, std::move(op1)) + : binary_exprt( + std::move(op0), + ID_sva_iff, + std::move(op1), + verilog_sva_property_typet{}) { } + + // (lhs implies rhs) and (rhs implies lhs) + exprt implications() const; }; static inline const sva_iff_exprt &to_sva_iff_expr(const exprt &expr) @@ -884,11 +1009,15 @@ static inline sva_iff_exprt &to_sva_iff_expr(exprt &expr) return static_cast(expr); } -class sva_implies_exprt : public binary_predicate_exprt +class sva_implies_exprt : public binary_exprt { public: explicit sva_implies_exprt(exprt op0, exprt op1) - : binary_predicate_exprt(std::move(op0), ID_sva_implies, std::move(op1)) + : binary_exprt( + std::move(op0), + ID_sva_implies, + std::move(op1), + verilog_sva_property_typet{}) { } }; @@ -910,8 +1039,9 @@ static inline sva_implies_exprt &to_sva_implies_expr(exprt &expr) class sva_or_exprt : public binary_exprt { public: - explicit sva_or_exprt(exprt op0, exprt op1, typet type) - : binary_exprt(std::move(op0), ID_sva_or, std::move(op1), std::move(type)) + // These can be sequences or properties, depending on the operands + explicit sva_or_exprt(exprt op0, exprt op1, typet __type) + : binary_exprt(std::move(op0), ID_sva_or, std::move(op1), std::move(__type)) { } }; @@ -1143,7 +1273,7 @@ class sva_if_exprt : public ternary_exprt std::move(__cond), std::move(__true_case), std::move(__false_case), - bool_typet()) + verilog_sva_property_typet{}) { } @@ -1200,11 +1330,11 @@ static inline sva_if_exprt &to_sva_if_expr(exprt &expr) /// Base class for sequence property expressions. /// 1800-2017 16.12.2 Sequence property -class sva_sequence_property_expr_baset : public unary_predicate_exprt +class sva_sequence_property_expr_baset : public unary_exprt { public: sva_sequence_property_expr_baset(irep_idt __id, exprt __op) - : unary_predicate_exprt(__id, std::move(__op)) + : unary_exprt(__id, std::move(__op), verilog_sva_property_typet{}) { } @@ -1219,7 +1349,7 @@ class sva_sequence_property_expr_baset : public unary_predicate_exprt } protected: - using unary_predicate_exprt::op; + using unary_exprt::op; }; inline const sva_sequence_property_expr_baset & @@ -1284,14 +1414,15 @@ inline sva_weak_exprt &to_sva_weak_expr(exprt &expr) return static_cast(expr); } -class sva_case_exprt : public binary_predicate_exprt +class sva_case_exprt : public binary_exprt { public: explicit sva_case_exprt(exprt __case_op, exprt __cases) - : binary_predicate_exprt( + : binary_exprt( std::move(__case_op), ID_sva_case, - std::move(__cases)) + std::move(__cases), + verilog_sva_property_typet{}) { } @@ -1348,8 +1479,8 @@ class sva_case_exprt : public binary_predicate_exprt exprt lower() const; protected: - using binary_predicate_exprt::op0; - using binary_predicate_exprt::op1; + using binary_exprt::op0; + using binary_exprt::op1; }; inline const sva_case_exprt &to_sva_case_expr(const exprt &expr) diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 493dd1008..9df7d9c4c 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1806,8 +1806,7 @@ void verilog_typecheckt::convert_property_declaration( convert_sva(declaration.cond()); require_sva_property(declaration.cond()); - auto type = bool_typet{}; - type.set(ID_C_verilog_type, ID_verilog_property_declaration); + auto type = verilog_sva_property_typet{}; symbolt symbol{full_identifier, type, mode}; symbol.module = module_identifier; diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 29e21bde9..4efb9f99b 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -42,6 +42,11 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &expr) expr = sva_boolean_exprt{std::move(expr), verilog_sva_sequence_typet{}}; } } + else if(type.id() == ID_verilog_sva_property) + { + throw errort().with_location(expr.source_location()) + << "sequence required, but got property"; + } else { throw errort().with_location(expr.source_location()) @@ -61,6 +66,10 @@ void verilog_typecheck_exprt::require_sva_property(exprt &expr) // or cover. expr = sva_sequence_property_exprt{std::move(expr)}; } + else if(type.id() == ID_verilog_sva_property) + { + // good as is + } else if( type.id() == ID_bool || type.id() == ID_unsignedbv || type.id() == ID_signedbv || type.id() == ID_verilog_unsignedbv || @@ -85,14 +94,14 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr) { convert_sva(expr.op()); require_sva_property(expr.op()); - expr.type() = bool_typet{}; // always boolean, never x + expr.type() = verilog_sva_property_typet{}; // always boolean, never x return std::move(expr); } else if(expr.id() == ID_sva_weak || expr.id() == ID_sva_strong) { convert_sva(expr.op()); require_sva_sequence(expr.op()); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } else @@ -126,7 +135,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) require_sva_property(expr.lhs()); require_sva_property(expr.rhs()); // always boolean, never x - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; } return std::move(expr); @@ -140,7 +149,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) require_sva_property(expr.rhs()); // always boolean, never x - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } @@ -156,7 +165,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) convert_sva(to_sva_abort_expr(expr).property()); require_sva_property(to_sva_abort_expr(expr).property()); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } @@ -185,7 +194,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) auto &op = to_sva_indexed_nexttime_expr(expr).op(); convert_sva(op); require_sva_property(op); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } @@ -196,7 +205,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) auto &op = to_sva_indexed_s_nexttime_expr(expr).op(); convert_sva(op); require_sva_property(op); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } @@ -215,7 +224,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) convert_sva(expr.rhs()); require_sva_property(expr.rhs()); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } else if( @@ -228,7 +237,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) convert_sva(expr.rhs()); require_sva_property(expr.rhs()); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } @@ -295,7 +304,7 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) require_sva_property(case_item.result()); } - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } else @@ -387,7 +396,7 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr) convert_sva(expr.op2()); require_sva_property(expr.op2()); - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } @@ -406,7 +415,7 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr) } // These are always property expressions - expr.type() = bool_typet{}; + expr.type() = verilog_sva_property_typet{}; return std::move(expr); } diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h index b3d8aec77..5c5916d77 100644 --- a/src/verilog/verilog_types.h +++ b/src/verilog/verilog_types.h @@ -739,6 +739,15 @@ inline verilog_package_scope_typet &to_verilog_package_scope_type(typet &type) return static_cast(type); } +/// SVA properties +class verilog_sva_property_typet : public typet +{ +public: + verilog_sva_property_typet() : typet(ID_verilog_sva_property) + { + } +}; + /// SVA sequences class verilog_sva_sequence_typet : public typet {