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

Support sequence intersect operator (#7374)

This commit is contained in:
Yilou Wang 2026-04-08 09:31:54 +02:00 committed by GitHub
parent 2736262b98
commit 141fe8bdad
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
17 changed files with 306 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/V3AssertPre.cpp
View File

@ -745,7 +745,7 @@ private:
AstSenTree* const senTreep = newSenTree(nodep);
AstAlways* const alwaysp = new AstAlways{flp, VAlwaysKwd::ALWAYS, senTreep, ifp};
cntVarp->addNextHere(alwaysp);
// Match when N-1 previous cycles were true and current cycle is true
// Match: cnt >= N-1 (previous cycles via NBA) && expr (current cycle)
AstNodeExpr* const cntCheckp = new AstGte{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
new AstConst{flp, static_cast<uint32_t>(n - 1)}};
cntCheckp->dtypeSetBit();
@ -852,6 +852,7 @@ private:
AstVar* const cntVarp = new AstVar{flp, VVarType::BLOCKTEMP, name + "__counter",
exprp->findBasicDType(VBasicDTypeKwd::UINT32)};
cntVarp->lifetime(VLifetime::AUTOMATIC_EXPLICIT);
cntVarp->noSample(true);
AstBegin* const beginp = new AstBegin{flp, name + "__block", cntVarp, true};
beginp->addStmtsp(

80
src/V3AssertProp.cpp
View File

@ -136,8 +136,9 @@ static std::vector<SeqStep> extractTimeline(AstNodeExpr* nodep) {
if (AstConst* const constp = VN_CAST(dlyp->lhsp(), Const)) {
cycles = constp->toSInt();
} else {
dlyp->lhsp()->v3warn(E_UNSUPPORTED,
"Unsupported: non-constant cycle delay in sequence and/or");
dlyp->lhsp()->v3warn(
E_UNSUPPORTED,
"Unsupported: non-constant cycle delay in sequence and/or/intersect");
}
}
// The expression after the delay
@ -158,6 +159,18 @@ static std::vector<SeqStep> extractTimeline(AstNodeExpr* nodep) {
return timeline;
}
// True if any AstSExpr in the subtree has a range delay (##[m:n]).
// Uses forall(): predicate returns false when a range delay is found,
// so !forall(...) means "at least one range delay exists".
static bool subtreeHasRangeDelay(const AstNode* nodep) {
return !nodep->forall([](const AstSExpr* sexprp) {
if (const AstDelay* const dlyp = VN_CAST(sexprp->delayp(), Delay)) {
if (dlyp->isRangeDelay()) return false;
}
return true;
});
}
// Lower sequence and/or to AST
class AssertPropLowerVisitor final : public VNVisitor {
// STATE
@ -396,6 +409,47 @@ class AssertPropLowerVisitor final : public VNVisitor {
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
// Lower a multi-cycle sequence 'intersect' (IEEE 1800-2023 16.9.6).
// intersect = and + equal-length constraint: both operands must match with the same duration.
// When total delays are equal constants, this is identical to 'and'; otherwise constant-false.
void lowerSeqIntersect(AstNodeBiop* nodep) {
const std::vector<SeqStep> lhsTimeline = extractTimeline(nodep->lhsp());
const std::vector<SeqStep> rhsTimeline = extractTimeline(nodep->rhsp());
int lhsTotal = 0;
for (const auto& step : lhsTimeline) lhsTotal += step.delayCycles;
int rhsTotal = 0;
for (const auto& step : rhsTimeline) rhsTotal += step.delayCycles;
if (lhsTotal != rhsTotal) {
// Lengths differ: per IEEE 16.9.6, the match set is empty -- constant-false.
// Warn the user; mismatched lengths are almost always a mistake.
// Skip when either operand had a range delay: RangeDelayExpander already
// replaced it with an FSM expression (containsSExpr returns false) and
// issued UNSUPPORTED, so no second diagnostic is needed.
if (containsSExpr(nodep->lhsp()) && containsSExpr(nodep->rhsp())) {
if (lhsTotal > rhsTotal) {
nodep->v3warn(WIDTHEXPAND, "Intersect sequence length mismatch"
" (left "
<< lhsTotal << " cycles, right " << rhsTotal
<< " cycles) -- intersection is always empty");
} else {
nodep->v3warn(WIDTHTRUNC, "Intersect sequence length mismatch"
" (left "
<< lhsTotal << " cycles, right " << rhsTotal
<< " cycles) -- intersection is always empty");
}
}
FileLine* const flp = nodep->fileline();
AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true};
bodyp->addStmtsp(new AstPExprClause{flp, false});
AstPExpr* const pexprp = new AstPExpr{flp, bodyp, nodep->dtypep()};
nodep->replaceWith(pexprp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
return;
}
// Same length: length restriction is trivially satisfied, lower as 'and'.
lowerSeqAnd(nodep);
}
void visit(AstSAnd* nodep) override {
iterateChildren(nodep);
if (containsSExpr(nodep->lhsp()) || containsSExpr(nodep->rhsp())) {
@ -409,6 +463,19 @@ class AssertPropLowerVisitor final : public VNVisitor {
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
}
void visit(AstSIntersect* nodep) override {
iterateChildren(nodep);
if (containsSExpr(nodep->lhsp()) || containsSExpr(nodep->rhsp())) {
lowerSeqIntersect(nodep);
} else {
// Pure boolean operands: length is always 0, lower to LogAnd
AstLogAnd* const newp = new AstLogAnd{nodep->fileline(), nodep->lhsp()->unlinkFrBack(),
nodep->rhsp()->unlinkFrBack()};
newp->dtypeFrom(nodep);
nodep->replaceWith(newp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
}
void visit(AstSOr* nodep) override {
iterateChildren(nodep);
if (containsSExpr(nodep->lhsp()) || containsSExpr(nodep->rhsp())) {
@ -1099,6 +1166,15 @@ class RangeDelayExpander final : public VNVisitor {
}
}
void visit(AstSIntersect* nodep) override {
// intersect with a range-delay operand cannot be lowered: the length-pairing
// logic requires knowing each operand's concrete length, which is dynamic.
if (subtreeHasRangeDelay(nodep->lhsp()) || subtreeHasRangeDelay(nodep->rhsp())) {
nodep->v3warn(E_UNSUPPORTED, "Unsupported: intersect with ranged cycle-delay operand");
}
iterateChildren(nodep);
}
void visit(AstSThroughout* nodep) override {
// Reject throughout with range-delay sequences before FSM expansion
// would silently lose per-tick enforcement (IEEE 1800-2023 16.9.9)

24
src/V3AstNodeExpr.h
View File

@ -3670,6 +3670,30 @@ public:
bool sizeMattersRhs() const override { return false; }
int instrCount() const override { return widthInstrs() + INSTR_COUNT_BRANCH; }
};
class AstSIntersect final : public AstNodeBiop {
// Sequence 'intersect' (IEEE 1800-2023 16.9.6): both operands match with equal length.
// AND with a length restriction. For boolean operands, lowered to AstLogAnd.
public:
AstSIntersect(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp)
: ASTGEN_SUPER_SIntersect(fl, lhsp, rhsp) {
dtypeSetBit();
}
ASTGEN_MEMBERS_AstSIntersect;
// LCOV_EXCL_START // Lowered before these are ever called
void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override {
out.opLogAnd(lhs, rhs);
}
string emitVerilog() override { return "%k(%l %fintersect %r)"; }
string emitC() override { V3ERROR_NA_RETURN(""); }
string emitSimpleOperator() override { V3ERROR_NA_RETURN(""); }
bool cleanOut() const override { return true; }
bool cleanLhs() const override { return true; }
bool cleanRhs() const override { return true; }
bool sizeMattersLhs() const override { return false; }
bool sizeMattersRhs() const override { return false; }
int instrCount() const override { return widthInstrs() + INSTR_COUNT_BRANCH; }
// LCOV_EXCL_STOP
};
class AstSOr final : public AstNodeBiop {
// Sequence 'or' (IEEE 1800-2023 16.9.7): at least one operand sequence must match.
// Operates on match sets, not values. For boolean operands, lowered to AstLogOr.

8
src/V3Dfg.cpp
View File

@ -781,11 +781,13 @@ void DfgVertex::typeCheck(const DfgGraph& dfg) const {
}
case VDfgType::SAnd:
case VDfgType::SIntersect:
case VDfgType::SOr:
case VDfgType::SThroughout: {
UASSERT_OBJ(false, this,
"SAnd/SOr/SThroughout should be removed before DFG"); // LCOV_EXCL_LINE
return; // LCOV_EXCL_LINE
// LCOV_EXCL_START // Lowered before DFG
UASSERT_OBJ(false, this, "SAnd/SIntersect/SOr/SThroughout should be removed before DFG");
return;
// LCOV_EXCL_STOP
}
case VDfgType::LogAnd:

2
src/V3DfgCse.cpp
View File

@ -126,6 +126,7 @@ class V3DfgCse final {
case VDfgType::StreamL:
case VDfgType::StreamR:
case VDfgType::SAnd:
case VDfgType::SIntersect:
case VDfgType::SOr:
case VDfgType::SThroughout:
case VDfgType::Sub:
@ -251,6 +252,7 @@ class V3DfgCse final {
case VDfgType::ShiftRS:
case VDfgType::StreamL:
case VDfgType::SAnd:
case VDfgType::SIntersect:
case VDfgType::SOr:
case VDfgType::SThroughout:
case VDfgType::StreamR:

3
src/V3Width.cpp
View File

@ -294,8 +294,9 @@ class WidthVisitor final : public VNVisitor {
// Widths: 1 bit out, lhs 1 bit, rhs 1 bit; Real: converts via compare with 0
void visit(AstLogAnd* nodep) override { visit_log_and_or(nodep); }
void visit(AstLogOr* nodep) override { visit_log_and_or(nodep); }
// Sequence and/or (IEEE 1800-2023 16.9.2), same width rules as LogAnd/LogOr
// Sequence and/or/intersect (IEEE 1800-2023 16.9.2), same width rules as LogAnd/LogOr
void visit(AstSAnd* nodep) override { visit_log_and_or(nodep); }
void visit(AstSIntersect* nodep) override { visit_log_and_or(nodep); }
void visit(AstSOr* nodep) override { visit_log_and_or(nodep); }
void visit(AstLogEq* nodep) override {
// Conversion from real not in IEEE, but a fallout

2
src/verilog.y
View File

@ -6849,7 +6849,7 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
{ $$ = new AstSOr{$2, $1, $3}; }
// // Intersect always has an sexpr rhs
| ~p~sexpr yINTERSECT sexpr
{ $$ = $1; BBUNSUP($2, "Unsupported: intersect (in sequence expression)"); DEL($3); }
{ $$ = new AstSIntersect{$2, $1, $3}; }
//
| yFIRST_MATCH '(' sexpr ')'
{ $$ = $3; BBUNSUP($1, "Unsupported: first_match (in sequence expression)"); }

18
test_regress/t/t_sequence_intersect.py Executable file
View File

@ -0,0 +1,18 @@
#!/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('simulator')
test.compile(verilator_flags2=['--assert --timing'])
test.execute()
test.passes()

82
test_regress/t/t_sequence_intersect.v Normal file
View File

@ -0,0 +1,82 @@
// 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 stop $stop
`define checkh(gotv, expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got='h%x exp='h%x\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
// verilog_format: on
module t (
input clk
);
integer cyc = 0;
reg [63:0] crc = '0;
reg [63:0] sum = '0;
// Derive test signals from CRC
wire a = crc[0];
wire b = crc[1];
wire c = crc[2];
wire d = crc[3];
wire [63:0] result = {60'h0, d, c, b, a};
always_ff @(posedge clk) begin
`ifdef TEST_VERBOSE
$write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b d=%b\n",
$time, cyc, crc, a, b, c, d);
`endif
cyc <= cyc + 1;
crc <= {crc[62:0], crc[63] ^ crc[2] ^ crc[0]};
sum <= result ^ {sum[62:0], sum[63] ^ sum[2] ^ sum[0]};
if (cyc == 0) begin
crc <= 64'h5aef0c8d_d70a4497;
sum <= '0;
end else if (cyc < 10) begin
sum <= '0;
end else if (cyc == 99) begin
`checkh(crc, 64'hc77bb9b3784ea091);
`checkh(sum, 64'hdb7bc8bfe61f987e);
$write("*-* All Finished *-*\n");
$finish;
end
end
// =========================================================================
// Boolean intersect (length-0): equivalent to boolean AND (IEEE 16.9.6)
// =========================================================================
// Boolean intersect: when a & b, intersect succeeds (equivalent to AND)
assert property (@(posedge clk) disable iff (cyc < 2)
(a & b) |-> (a intersect b));
// Boolean intersect with constant true -- reduces to just 'a'
assert property (@(posedge clk) disable iff (cyc < 2)
a |-> (a intersect 1'b1));
// =========================================================================
// Multi-cycle sequence intersect (IEEE 1800-2023 16.9.6)
// Same-length sequences: intersect succeeds when both arms complete
// =========================================================================
// Both arms have length 1; 1'b1 guarantees completion on both sides
assert property (@(posedge clk)
(a & b) |-> (a ##1 1'b1) intersect (b ##1 1'b1));
// Both arms have length 2
assert property (@(posedge clk)
(a & b) |-> (a ##2 1'b1) intersect (b ##2 1'b1));
// Different internal structure, same total length (2 cycles each)
assert property (@(posedge clk)
(a & b) |-> (a ##1 1'b1 ##1 1'b1) intersect (b ##2 1'b1));
// Standalone constant intersect (always passes)
assert property (@(posedge clk)
(1'b1 ##1 1'b1) intersect (1'b1 ##1 1'b1));
endmodule

13
test_regress/t/t_sequence_intersect_len_warn.out Normal file
View File

@ -0,0 +1,13 @@
%Warning-WIDTHTRUNC: t/t_sequence_intersect_len_warn.v:16:17: Intersect sequence length mismatch (left 1 cycles, right 3 cycles) -- intersection is always empty
: ... note: In instance 't'
16 | (a ##1 b) intersect (c ##3 d));
| ^~~~~~~~~
... For warning description see https://verilator.org/warn/WIDTHTRUNC?v=latest
... Use "/* verilator lint_off WIDTHTRUNC */" and lint_on around source to disable this message.
%Warning-WIDTHEXPAND: t/t_sequence_intersect_len_warn.v:20:17: Intersect sequence length mismatch (left 3 cycles, right 1 cycles) -- intersection is always empty
: ... note: In instance 't'
20 | (a ##3 b) intersect (c ##1 d));
| ^~~~~~~~~
... For warning description see https://verilator.org/warn/WIDTHEXPAND?v=latest
... Use "/* verilator lint_off WIDTHEXPAND */" and lint_on around source to disable this message.
%Error: Exiting due to

18
test_regress/t/t_sequence_intersect_len_warn.py Executable file
View File

@ -0,0 +1,18 @@
#!/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 Normal file
View File

@ -0,0 +1,22 @@
// 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

6
test_regress/t/t_sequence_intersect_range_unsup.out Normal file
View File

@ -0,0 +1,6 @@
%Error-UNSUPPORTED: t/t_sequence_intersect_range_unsup.v:12:21: Unsupported: intersect with ranged cycle-delay operand
: ... note: In instance 't'
12 | (a ##[1:5] b) intersect (c ##2 d));
| ^~~~~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

18
test_regress/t/t_sequence_intersect_range_unsup.py Executable file
View File

@ -0,0 +1,18 @@
#!/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('linter')
test.compile(verilator_flags2=['--assert --timing'],
fails=True,
expect_filename=test.golden_filename)
test.passes()

14
test_regress/t/t_sequence_intersect_range_unsup.v Normal file
View File

@ -0,0 +1,14 @@
// 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;
// Range delay in intersect operand is unsupported
assert property (@(posedge clk)
(a ##[1:5] b) intersect (c ##2 d));
endmodule

2
test_regress/t/t_sequence_nonconst_delay_unsup.out
View File

@ -1,4 +1,4 @@
%Error-UNSUPPORTED: t/t_sequence_nonconst_delay_unsup.v:14:40: Unsupported: non-constant cycle delay in sequence and/or
%Error-UNSUPPORTED: t/t_sequence_nonconst_delay_unsup.v:14:40: Unsupported: non-constant cycle delay in sequence and/or/intersect
: ... note: In instance 't'
14 | assert property (@(posedge clk) (a ##delay b) and (c ##1 d));
| ^~~~~

3
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -2,9 +2,6 @@
34 | a within(b);
| ^~~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:50:7: Unsupported: intersect (in sequence expression)
50 | a intersect b;
| ^~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:89:7: Unsupported: [*] boolean abbrev expression
89 | a [*];
| ^~