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/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/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) 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); + } +}