From 0225b8155f3db509af9ccd38e3c9b42b6bdd7e9e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 20 Apr 2025 13:36:57 -0700 Subject: [PATCH] BMC: SVA sequence within This implements the SVA sequence within operator in the word-level BMC backend. --- CHANGELOG | 1 + regression/verilog/SVA/sequence_within1.desc | 8 +++-- regression/verilog/SVA/sequence_within1.sv | 15 ++++++++- src/trans-word-level/property.cpp | 4 --- src/trans-word-level/sequence.cpp | 32 +++++++++++++++++++- src/verilog/sva_expr.h | 29 ++++++++++++++++++ src/verilog/verilog_typecheck_sva.cpp | 1 - 7 files changed, 81 insertions(+), 9 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 54ce984f7..a4b0b35d0 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -6,6 +6,7 @@ * SystemVerilog: unbased unsigned literals '0, '1, 'x, 'z * SystemVerilog: first_match * SystemVerilog: [->n] and [=n] +* SystemVerilog: within * SystemVerilog: bugfix for |-> and |=> * SystemVerilog: bugfix for SVA sequence and * Verilog: 'dx, 'dz diff --git a/regression/verilog/SVA/sequence_within1.desc b/regression/verilog/SVA/sequence_within1.desc index 60b676baa..06ba44868 100644 --- a/regression/verilog/SVA/sequence_within1.desc +++ b/regression/verilog/SVA/sequence_within1.desc @@ -1,7 +1,11 @@ CORE sequence_within1.sv ---bound 5 -^\[.*\] main\.x == 0 within main\.x == 1: FAILURE: property not supported by BMC engine$ +--bound 20 +^\[main\.p0\] main\.x == 0 within main\.x == 1: REFUTED$ +^\[main\.p1\] main\.x == 0 within \(##10 1\): PROVED up to bound 20$ +^\[main\.p2\] main\.x == 5 within \(##10 1\): PROVED up to bound 20$ +^\[main\.p3\] main\.x == 10 within \(##10 1\): PROVED up to bound 20$ +^\[main\.p4\] main\.x == 11 within \(##10 1\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/sequence_within1.sv b/regression/verilog/SVA/sequence_within1.sv index 259bef54a..710eb1258 100644 --- a/regression/verilog/SVA/sequence_within1.sv +++ b/regression/verilog/SVA/sequence_within1.sv @@ -1,10 +1,23 @@ module main(input clk); - reg [31:0] x = 0; + reg [7:0] x = 0; always @(posedge clk) x<=x+1; + // fails, no rhs match initial p0: assert property (x == 0 within x == 1); + // passes, lhs match at beginning of rhs match + initial p1: assert property (x == 0 within ##10 1); + + // passes, lhs match in the middle of rhs match + initial p2: assert property (x == 5 within ##10 1); + + // passes, lhs match at the end of rhs match + initial p3: assert property (x == 10 within ##10 1); + + // fails, lhs match just beyond the rhs match + initial p4: assert property (x == 11 within ##10 1); + endmodule diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp index 604a4d338..889004a6c 100644 --- a/src/trans-word-level/property.cpp +++ b/src/trans-word-level/property.cpp @@ -111,10 +111,6 @@ Function: bmc_supports_SVA_property bool bmc_supports_SVA_property(const exprt &expr) { - // sva_sequence_within is not supported yet - if(has_subexpr(expr, ID_sva_sequence_within)) - return false; - return true; } diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 6047bdc73..fead3b91f 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -205,7 +205,37 @@ sequence_matchest instantiate_sequence( } else if(expr.id() == ID_sva_sequence_within) { - PRECONDITION(false); + // If the lhs match is contained anywhere within the rhs match, + // then return the rhs match. + + auto &within_expr = to_sva_sequence_within_expr(expr); + const auto matches_rhs = + instantiate_sequence(within_expr.rhs(), t, no_timeframes); + + sequence_matchest result; + + for(auto &match_rhs : matches_rhs) + { + for(auto start_lhs = t; start_lhs <= match_rhs.end_time; ++start_lhs) + { + auto matches_lhs = + instantiate_sequence(within_expr.lhs(), start_lhs, no_timeframes); + + for(auto &match_lhs : matches_lhs) + { + // The end_time of the lhs match must be no later than the + // end_time of the rhs match. + if(match_lhs.end_time <= match_rhs.end_time) + { + // return the rhs end_time + auto cond = and_exprt{match_lhs.condition, match_rhs.condition}; + result.emplace_back(match_rhs.end_time, std::move(cond)); + } + } + } + } + + return result; } else if(expr.id() == ID_sva_and) { diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h index f3279871c..219789518 100644 --- a/src/verilog/sva_expr.h +++ b/src/verilog/sva_expr.h @@ -1500,6 +1500,35 @@ to_sva_sequence_intersect_expr(exprt &expr) return static_cast(expr); } +class sva_sequence_within_exprt : public binary_exprt +{ +public: + sva_sequence_within_exprt(exprt op0, exprt op1) + : binary_exprt( + std::move(op0), + ID_sva_sequence_within, + std::move(op1), + verilog_sva_sequence_typet{}) + { + } +}; + +static inline const sva_sequence_within_exprt & +to_sva_sequence_within_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_within); + sva_sequence_within_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + +static inline sva_sequence_within_exprt & +to_sva_sequence_within_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_sva_sequence_within); + sva_sequence_within_exprt::check(expr, validation_modet::INVARIANT); + return static_cast(expr); +} + class sva_sequence_throughout_exprt : public binary_exprt { public: diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 3ed7ef6bc..b85fb3e23 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -239,7 +239,6 @@ exprt verilog_typecheck_exprt::convert_binary_sva(binary_exprt expr) convert_sva(expr.rhs()); require_sva_sequence(expr.rhs()); - expr.type() = bool_typet{}; expr.type() = verilog_sva_sequence_typet{};