From d13e18cffd4bc2138cbca223e1a521fec436531b Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Wed, 24 Jun 2026 13:57:47 +0200 Subject: [PATCH] Compile intersect with no common length as never-matching --- src/V3AssertNfa.cpp | 27 +++++---- .../t/t_sequence_intersect_disjoint_bad.out | 6 -- .../t/t_sequence_intersect_disjoint_bad.v | 18 ------ .../t/t_sequence_intersect_len_warn.out | 10 ---- .../t/t_sequence_intersect_len_warn.py | 18 ------ .../t/t_sequence_intersect_len_warn.v | 22 ------- ....py => t_sequence_intersect_nevermatch.py} | 8 +-- .../t/t_sequence_intersect_nevermatch.v | 57 +++++++++++++++++++ 8 files changed, 78 insertions(+), 88 deletions(-) delete mode 100644 test_regress/t/t_sequence_intersect_disjoint_bad.out delete mode 100644 test_regress/t/t_sequence_intersect_disjoint_bad.v delete mode 100644 test_regress/t/t_sequence_intersect_len_warn.out delete mode 100755 test_regress/t/t_sequence_intersect_len_warn.py delete mode 100644 test_regress/t/t_sequence_intersect_len_warn.v rename test_regress/t/{t_sequence_intersect_disjoint_bad.py => t_sequence_intersect_nevermatch.py} (73%) create mode 100644 test_regress/t/t_sequence_intersect_nevermatch.v diff --git a/src/V3AssertNfa.cpp b/src/V3AssertNfa.cpp index 6761b7608..6fd12eee0 100644 --- a/src/V3AssertNfa.cpp +++ b/src/V3AssertNfa.cpp @@ -980,6 +980,19 @@ class SvaNfaBuilder final { return result; } + // Empty common-length intersection -- unequal fixed lengths, or disjoint + // ranged lengths. IEEE 1800-2023 16.9.6 requires both operands to match + // over a window of the same length, so with no common length the intersect + // simply never matches. This is legal (matching nothing), not an error, so + // lower to a constant false rather than rejecting legal code. Mirrors + // commercial simulators: compiles clean, the assertion never matches and a + // cover yields zero hits. + BuildResult buildNeverMatchIntersect(AstNodeExpr* nodep, SvaStateVertex* entryVtxp, + bool isTopLevelStep) { + AstNodeExpr* const falsep = new AstConst{nodep->fileline(), AstConst::BitFalse{}}; + return buildFromLoweringTree(falsep, entryVtxp, isTopLevelStep); + } + // Lower `seq1 intersect seq2` when an operand's match length varies // (IEEE 1800-2023 16.9.6: both match over one window, equal start and end). // The common length range is [lo,hi] = intersection of the two operands' @@ -1005,12 +1018,8 @@ class SvaNfaBuilder final { const int lo = std::max(lhsRange.first, rhsRange.first); const int hi = std::min(lhsRange.second, rhsRange.second); if (lo > hi) { - nodep->v3error("Intersect sequence lengths share no common value: left " - + std::to_string(lhsRange.first) + ".." - + std::to_string(lhsRange.second) + " cycles, right " - + std::to_string(rhsRange.first) + ".." - + std::to_string(rhsRange.second) + " cycles (IEEE 1800-2023 16.9.6)"); - return BuildResult::failWithError(); + // Disjoint length ranges share no common length -> never matches. + return buildNeverMatchIntersect(nodep, entryVtxp, isTopLevelStep); } FileLine* const flp = nodep->fileline(); if (lo == hi) { @@ -1261,10 +1270,8 @@ public: const int rhsLen = fixedLength(intp->rhsp()); if (lhsLen >= 0 && rhsLen >= 0) { if (lhsLen != rhsLen) { - intp->v3error("Intersect sequence length mismatch: left " - + std::to_string(lhsLen) + " cycles, right " - + std::to_string(rhsLen) + " cycles (IEEE 1800-2023 16.9.6)"); - return BuildResult::failWithError(); + // Unequal fixed lengths share no common length -> never matches. + return buildNeverMatchIntersect(intp, entryVtxp, isTopLevelStep); } return buildAndCombiner(intp->lhsp(), intp->rhsp(), entryVtxp, intp->fileline()); } diff --git a/test_regress/t/t_sequence_intersect_disjoint_bad.out b/test_regress/t/t_sequence_intersect_disjoint_bad.out deleted file mode 100644 index c5a131724..000000000 --- a/test_regress/t/t_sequence_intersect_disjoint_bad.out +++ /dev/null @@ -1,6 +0,0 @@ -%Error: t/t_sequence_intersect_disjoint_bad.v:16:34: Intersect sequence lengths share no common value: left 1..2 cycles, right 4..5 cycles (IEEE 1800-2023 16.9.6) - : ... note: In instance 't' - 16 | assert property ((a ##[1:2] b) intersect (c ##[4:5] d)); - | ^~~~~~~~~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: Exiting due to diff --git a/test_regress/t/t_sequence_intersect_disjoint_bad.v b/test_regress/t/t_sequence_intersect_disjoint_bad.v deleted file mode 100644 index 321a592d5..000000000 --- a/test_regress/t/t_sequence_intersect_disjoint_bad.v +++ /dev/null @@ -1,18 +0,0 @@ -// DESCRIPTION: Verilator: Verilog Test module -// -// This file ONLY is placed under the Creative Commons Public Domain. -// SPDX-FileCopyrightText: 2026 PlanV GmbH -// SPDX-License-Identifier: CC0-1.0 - -module t ( - input clk -); - logic a, b, c, d; - - default clocking @(posedge clk); - endclocking - - // LHS length in [1,2], RHS in [4,5]: no common length, can never match - assert property ((a ##[1:2] b) intersect (c ##[4:5] d)); - -endmodule diff --git a/test_regress/t/t_sequence_intersect_len_warn.out b/test_regress/t/t_sequence_intersect_len_warn.out deleted file mode 100644 index f8239fae1..000000000 --- a/test_regress/t/t_sequence_intersect_len_warn.out +++ /dev/null @@ -1,10 +0,0 @@ -%Error: t/t_sequence_intersect_len_warn.v:16:17: Intersect sequence length mismatch: left 1 cycles, right 3 cycles (IEEE 1800-2023 16.9.6) - : ... note: In instance 't' - 16 | (a ##1 b) intersect (c ##3 d)); - | ^~~~~~~~~ - ... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance. -%Error: t/t_sequence_intersect_len_warn.v:20:17: Intersect sequence length mismatch: left 3 cycles, right 1 cycles (IEEE 1800-2023 16.9.6) - : ... note: In instance 't' - 20 | (a ##3 b) intersect (c ##1 d)); - | ^~~~~~~~~ -%Error: Exiting due to diff --git a/test_regress/t/t_sequence_intersect_len_warn.py b/test_regress/t/t_sequence_intersect_len_warn.py deleted file mode 100755 index 58fc7aeba..000000000 --- a/test_regress/t/t_sequence_intersect_len_warn.py +++ /dev/null @@ -1,18 +0,0 @@ -#!/usr/bin/env python3 -# DESCRIPTION: Verilator: Verilog Test driver/expect definition -# -# This program is free software; you can redistribute it and/or modify it -# under the terms of either the GNU Lesser General Public License Version 3 -# or the Perl Artistic License Version 2.0. -# SPDX-FileCopyrightText: 2026 Wilson Snyder -# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 - -import vltest_bootstrap - -test.scenarios('vlt_all') - -test.compile(verilator_flags2=['--assert', '--timing', '--lint-only'], - fails=True, - expect_filename=test.golden_filename) - -test.passes() diff --git a/test_regress/t/t_sequence_intersect_len_warn.v b/test_regress/t/t_sequence_intersect_len_warn.v deleted file mode 100644 index e544c8926..000000000 --- a/test_regress/t/t_sequence_intersect_len_warn.v +++ /dev/null @@ -1,22 +0,0 @@ -// DESCRIPTION: Verilator: Verilog Test module -// -// This file ONLY is placed under the Creative Commons Public Domain. -// SPDX-FileCopyrightText: 2026 PlanV GmbH -// SPDX-License-Identifier: CC0-1.0 - -// verilog_format: off -// verilog_lint: off -// verilog_format: on - -module t (input clk); - logic a, b, c, d; - - // LHS length 2, RHS length 4 -- WIDTHTRUNC (left < right) - assert property (@(posedge clk) - (a ##1 b) intersect (c ##3 d)); - - // LHS length 4, RHS length 2 -- WIDTHEXPAND (left > right) - assert property (@(posedge clk) - (a ##3 b) intersect (c ##1 d)); - -endmodule diff --git a/test_regress/t/t_sequence_intersect_disjoint_bad.py b/test_regress/t/t_sequence_intersect_nevermatch.py similarity index 73% rename from test_regress/t/t_sequence_intersect_disjoint_bad.py rename to test_regress/t/t_sequence_intersect_nevermatch.py index f83bbb887..02f5fb0b6 100755 --- a/test_regress/t/t_sequence_intersect_disjoint_bad.py +++ b/test_regress/t/t_sequence_intersect_nevermatch.py @@ -9,10 +9,10 @@ import vltest_bootstrap -test.scenarios('linter') +test.scenarios('simulator') -test.compile(verilator_flags2=['--assert --timing'], - fails=True, - expect_filename=test.golden_filename) +test.compile(verilator_flags2=['--assert --timing --debug-check']) + +test.execute() test.passes() diff --git a/test_regress/t/t_sequence_intersect_nevermatch.v b/test_regress/t/t_sequence_intersect_nevermatch.v new file mode 100644 index 000000000..17887e184 --- /dev/null +++ b/test_regress/t/t_sequence_intersect_nevermatch.v @@ -0,0 +1,57 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define checkd(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); $stop; end while(0); +// verilog_format: on + +module t ( + input clk +); + integer cyc = 0; + reg [63:0] crc = 64'h5aef0c8d_d70a4497; + + wire a = crc[0]; + wire b = crc[1]; + wire c = crc[2]; + wire d = crc[3]; + + int f_fix = 0; + int f_dis = 0; + + always_ff @(posedge clk) begin + cyc <= cyc + 1; + crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]}; + if (cyc == 99) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end + + default clocking @(posedge clk); + endclocking + + // An intersect whose operands share no common length compiles and never + // matches (IEEE 1800-2023 16.9.6 requires a window of equal length). Each + // form is the antecedent of `|-> 1'b0`: it stays vacuous while it never + // matches, so the else fires once per match -- pinned to 0. A spurious match + // would both fail the assertion and bump the counter. + + // Unequal fixed lengths: {2} vs {3}. + ap_fix : + assert property (disable iff (cyc < 2) ((a ##2 b) intersect (c ##3 d)) |-> 1'b0) + else f_fix <= f_fix + 1; + + // Disjoint ranges: {1,2} vs {4,5}. + ap_dis : + assert property (disable iff (cyc < 2) ((a ##[1:2] b) intersect (c ##[4:5] d)) |-> 1'b0) + else f_dis <= f_dis + 1; + + final begin + `checkd(f_fix, 0); // Questa: 0 + `checkd(f_dis, 0); // Questa: 0 + end +endmodule