From 94e4f4d6f2bb63d0094d4892910272a940633fbe Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 19 Apr 2025 10:42:12 -0700 Subject: [PATCH 1/2] SVA: default sequence semantics SVA sequences can have weak or strong semantics. 1800-2017 16.12.2 Sequence property requires that sequences in properties that are not explicitly marked as strong or weak are interpreted as weak when used in assert property or assume property, and strong otherwise. The Verilog type checker now emits corresponding expressions sva_implict_weak and sva_implicit_strong for uses of SVA sequences in properties. --- src/hw_cbmc_irep_ids.h | 2 ++ src/temporal-logic/trivial_sva.cpp | 6 +++-- src/trans-word-level/property.cpp | 28 +++++++++++++++++++---- src/verilog/expr2verilog.cpp | 17 ++++++++++---- src/verilog/sva_expr.h | 27 ++++++++++++++-------- src/verilog/verilog_typecheck.cpp | 12 ++++++++++ src/verilog/verilog_typecheck_expr.h | 3 +++ src/verilog/verilog_typecheck_sva.cpp | 32 +++++++++++++++++++++++++++ 8 files changed, 108 insertions(+), 19 deletions(-) diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 9b3f09bb2..18d9bb9f2 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -49,6 +49,8 @@ IREP_ID_ONE(sva_accept_on) IREP_ID_ONE(sva_reject_on) IREP_ID_ONE(sva_sync_accept_on) IREP_ID_ONE(sva_sync_reject_on) +IREP_ID_ONE(sva_implicit_strong) +IREP_ID_ONE(sva_implicit_weak) IREP_ID_ONE(sva_strong) IREP_ID_ONE(sva_weak) IREP_ID_ONE(sva_if) diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp index 13aca48aa..ba1d164de 100644 --- a/src/temporal-logic/trivial_sva.cpp +++ b/src/temporal-logic/trivial_sva.cpp @@ -107,11 +107,13 @@ exprt trivial_sva(exprt expr) op = trivial_sva(op); // post-traversal - if(expr.id() == ID_sva_sequence_property) + if( + expr.id() == ID_sva_weak || expr.id() == ID_sva_strong || + expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong) { // We simplify sequences to boolean expressions, and hence can drop // the sva_sequence_property converter - auto &op = to_sva_sequence_property_expr(expr).sequence(); + auto &op = to_sva_sequence_property_expr_base(expr).sequence(); if(op.type().id() == ID_bool) return op; } diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index d2f2f61f4..604a4d338 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -527,10 +527,24 @@ static obligationst property_obligations_rec( return property_obligations_rec( op_negated_opt.value(), current, no_timeframes); } - else if(is_SVA_sequence_operator(op)) + else if( + op.id() == ID_sva_strong || op.id() == ID_sva_weak || + op.id() == ID_sva_implicit_strong || op.id() == ID_sva_implicit_weak) { - return obligationst{ - instantiate_property(property_expr, current, no_timeframes)}; + // The sequence must not match. + auto &sequence = to_sva_sequence_property_expr_base(op).sequence(); + + const auto matches = + instantiate_sequence(sequence, current, no_timeframes); + + obligationst obligations; + + for(auto &match : matches) + { + obligations.add(match.end_time, not_exprt{match.condition}); + } + + return obligations; } else if(is_temporal_operator(op)) { @@ -647,7 +661,8 @@ static obligationst property_obligations_rec( } else if( property_expr.id() == ID_sva_strong || property_expr.id() == ID_sva_weak || - property_expr.id() == ID_sva_sequence_property) + property_expr.id() == ID_sva_implicit_strong || + property_expr.id() == ID_sva_implicit_weak) { auto &sequence = to_sva_sequence_property_expr_base(property_expr).sequence(); @@ -667,6 +682,11 @@ static obligationst property_obligations_rec( return obligationst{max, disjunction(disjuncts)}; } + else if(property_expr.id() == ID_sva_sequence_property) + { + // Should have been turned into sva_implict_weak or sva_implict_strong in the type checker. + PRECONDITION(false); + } else { return obligationst{ diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 2ccb0b151..e050ff21e 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -536,9 +536,14 @@ expr2verilogt::resultt expr2verilogt::convert_sva_unary( if(op.id() == ID_typecast) op_operands = to_typecast_expr(op).op().operands().size(); - else if(src.op().id() == ID_sva_sequence_property) + else if( + src.op().id() == ID_sva_sequence_property || + src.op().id() == ID_sva_implicit_weak || + src.op().id() == ID_sva_implicit_strong) + { op_operands = - to_sva_sequence_property_expr(op).sequence().operands().size(); + to_sva_sequence_property_expr_base(op).sequence().operands().size(); + } else op_operands = op.operands().size(); @@ -1816,8 +1821,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src) else if(src.id() == ID_sva_weak) return convert_function("weak", src); - else if(src.id() == ID_sva_sequence_property) - return convert_rec(to_sva_sequence_property_expr(src).sequence()); + else if( + src.id() == ID_sva_sequence_property || + src.id() == ID_sva_implicit_strong || src.id() == ID_sva_implicit_weak) + { + return convert_rec(to_sva_sequence_property_expr_base(src).sequence()); + } else if(src.id()==ID_sva_sequence_concatenation) return convert_sva_sequence_concatenation( diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index c8bb9186a..f3279871c 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1143,7 +1143,7 @@ to_sva_sequence_property_expr_base(const exprt &expr) } inline sva_sequence_property_expr_baset & -to_sva_sequence_property_base_expr(exprt &expr) +to_sva_sequence_property_expr_base(exprt &expr) { sva_sequence_property_expr_baset::check(expr); return static_cast(expr); @@ -1152,22 +1152,24 @@ to_sva_sequence_property_base_expr(exprt &expr) class sva_strong_exprt : public sva_sequence_property_expr_baset { public: - sva_strong_exprt(exprt __op) - : sva_sequence_property_expr_baset(ID_sva_strong, std::move(__op)) + sva_strong_exprt(irep_idt __id, exprt __op) + : sva_sequence_property_expr_baset(__id, std::move(__op)) { } }; inline const sva_strong_exprt &to_sva_strong_expr(const exprt &expr) { - PRECONDITION(expr.id() == ID_sva_strong); + PRECONDITION( + expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong); sva_strong_exprt::check(expr); return static_cast(expr); } inline sva_strong_exprt &to_sva_strong_expr(exprt &expr) { - PRECONDITION(expr.id() == ID_sva_strong); + PRECONDITION( + expr.id() == ID_sva_strong || expr.id() == ID_sva_implicit_strong); sva_strong_exprt::check(expr); return static_cast(expr); } @@ -1175,22 +1177,22 @@ inline sva_strong_exprt &to_sva_strong_expr(exprt &expr) class sva_weak_exprt : public sva_sequence_property_expr_baset { public: - sva_weak_exprt(exprt __op) - : sva_sequence_property_expr_baset(ID_sva_weak, std::move(__op)) + sva_weak_exprt(irep_idt __id, exprt __op) + : sva_sequence_property_expr_baset(__id, std::move(__op)) { } }; inline const sva_weak_exprt &to_sva_weak_expr(const exprt &expr) { - PRECONDITION(expr.id() == ID_sva_weak); + PRECONDITION(expr.id() == ID_sva_weak || expr.id() == ID_sva_implicit_weak); sva_weak_exprt::check(expr); return static_cast(expr); } inline sva_weak_exprt &to_sva_weak_expr(exprt &expr) { - PRECONDITION(expr.id() == ID_sva_weak); + PRECONDITION(expr.id() == ID_sva_weak || expr.id() == ID_sva_implicit_weak); sva_weak_exprt::check(expr); return static_cast(expr); } @@ -1584,4 +1586,11 @@ to_sva_sequence_property_expr(exprt &expr) return static_cast(expr); } +/// SVA sequences can be interpreted as weak or strong +enum class sva_sequence_semanticst +{ + WEAK, + STRONG +}; + #endif diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 7df6d1bc9..493dd1008 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1060,6 +1060,12 @@ void verilog_typecheckt::convert_assert_assume_cover( convert_sva(cond); require_sva_property(cond); + // 1800-2017 16.12.2 Sequence property + if(module_item.id() == ID_verilog_cover_property) + set_default_sequence_semantics(cond, sva_sequence_semanticst::STRONG); + else + set_default_sequence_semantics(cond, sva_sequence_semanticst::WEAK); + // We create a symbol for the property. // The 'value' of the symbol is set by synthesis. const irep_idt &identifier = module_item.identifier(); @@ -1125,6 +1131,12 @@ void verilog_typecheckt::convert_assert_assume_cover( convert_sva(cond); require_sva_property(cond); + // 1800-2017 16.12.2 Sequence property + if(statement.id() == ID_verilog_cover_property) + set_default_sequence_semantics(cond, sva_sequence_semanticst::STRONG); + else + set_default_sequence_semantics(cond, sva_sequence_semanticst::WEAK); + // We create a symbol for the property. // The 'value' is set by synthesis. const irep_idt &identifier = statement.identifier(); diff --git a/src/verilog/verilog_typecheck_expr.h b/src/verilog/verilog_typecheck_expr.h index 365ef69a4..f1d9f7a73 100644 --- a/src/verilog/verilog_typecheck_expr.h +++ b/src/verilog/verilog_typecheck_expr.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "sva_expr.h" #include "verilog_typecheck_base.h" #include @@ -207,6 +208,8 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset [[nodiscard]] exprt convert_binary_sva(binary_exprt); [[nodiscard]] exprt convert_ternary_sva(ternary_exprt); + static void set_default_sequence_semantics(exprt &, sva_sequence_semanticst); + // system functions exprt bits(const exprt &); std::optional bits_rec(const typet &) const; diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index a99d12d40..3ed7ef6bc 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -430,3 +430,35 @@ exprt verilog_typecheck_exprt::convert_sva_rec(exprt expr) return convert_expr_rec(expr); } } + +// 1800-2017 16.12.2 Sequence property +// Sequences are by default _weak_ when used in assert property +// or assume property, and are _strong_ when used in cover property. +// This flips when below the SVA not operator. +void verilog_typecheck_exprt::set_default_sequence_semantics( + exprt &expr, + sva_sequence_semanticst semantics) +{ + if(expr.id() == ID_sva_sequence_property) + { + // apply + if(semantics == sva_sequence_semanticst::WEAK) + expr.id(ID_sva_implicit_weak); + else + expr.id(ID_sva_implicit_strong); + } + else if(expr.id() == ID_sva_not) + { + // flip + semantics = semantics == sva_sequence_semanticst::WEAK + ? sva_sequence_semanticst::STRONG + : sva_sequence_semanticst::WEAK; + + set_default_sequence_semantics(to_sva_not_expr(expr).op(), semantics); + } + else + { + for(auto &op : expr.operands()) + set_default_sequence_semantics(op, semantics); + } +} From 6cb2428bde23e530376f2039888d507fe684aea3 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 16 Apr 2025 23:33:42 -0700 Subject: [PATCH 2/2] weak, strong and implicit SVA sequence properties are SVA operators is_SVA_operator(...) now recognizes weak, strong and implicit SVA sequence properties. --- src/ebmc/completeness_threshold.cpp | 14 ++++++++++++++ src/temporal-logic/temporal_logic.cpp | 5 ++++- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/ebmc/completeness_threshold.cpp b/src/ebmc/completeness_threshold.cpp index 1f73141ca..0238dd68f 100644 --- a/src/ebmc/completeness_threshold.cpp +++ b/src/ebmc/completeness_threshold.cpp @@ -63,6 +63,20 @@ bool has_low_completeness_threshold(const exprt &expr) upper_int <= 1; } } + else if( + expr.id() == ID_sva_strong || expr.id() == ID_sva_weak || + expr.id() == ID_sva_implicit_strong || expr.id() == ID_sva_implicit_weak) + { + auto &sequence = to_sva_sequence_property_expr_base(expr).sequence(); + if(!is_SVA_sequence_operator(sequence)) + return true; + else + return false; + } + else if(expr.id() == ID_sva_sequence_property) + { + PRECONDITION(false); // should have been turned into implicit weak/strong + } else return false; } diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp index d73a3e7b4..d92c49549 100644 --- a/src/temporal-logic/temporal_logic.cpp +++ b/src/temporal-logic/temporal_logic.cpp @@ -132,7 +132,10 @@ bool is_SVA_operator(const exprt &expr) id == ID_sva_overlapped_implication || id == ID_sva_non_overlapped_implication || id == ID_sva_overlapped_followed_by || - id == ID_sva_nonoverlapped_followed_by; + id == ID_sva_nonoverlapped_followed_by || + id == ID_sva_sequence_property || id == ID_sva_weak || + id == ID_sva_strong || id == ID_sva_implicit_weak || + id == ID_sva_implicit_strong; } bool is_SVA(const exprt &expr)