luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Compile intersect with no common length as never-matching

This commit is contained in:
Yilou Wang 2026-06-24 13:57:47 +02:00
parent 944735fc05
commit d13e18cffd
8 changed files with 78 additions and 88 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
src/V3AssertNfa.cpp
View File

@ -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());
}

6
test_regress/t/t_sequence_intersect_disjoint_bad.out
View File

@ -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

18
test_regress/t/t_sequence_intersect_disjoint_bad.v
View File

@ -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

10
test_regress/t/t_sequence_intersect_len_warn.out
View File

@ -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

18
test_regress/t/t_sequence_intersect_len_warn.py
View File

@ -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()

22
test_regress/t/t_sequence_intersect_len_warn.v
View File

@ -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

8
test_regress/t/t_sequence_intersect_disjoint_bad.py → test_regress/t/t_sequence_intersect_nevermatch.py
View File

@ -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()

57
test_regress/t/t_sequence_intersect_nevermatch.v Normal file
View File

@ -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