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

Support boolean and/or in sequence expressions (#7285)

This commit is contained in:
Yilou Wang 2026-03-24 13:56:14 +01:00 committed by GitHub
parent 6873dc2f63
commit 0b2bf991a6
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
15 changed files with 558 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/V3AssertPre.cpp
View File

@ -823,6 +823,8 @@ private:
AstIf* const guardp = new AstIf{flp, condp, origStmtsp};
bodyp->addStmtsp(guardp);
nodep->replaceWith(pexprp);
// Don't iterate pexprp here -- it was already iterated when created
// (in visit(AstSExpr*)), so delays and disable iff are already processed.
} else if (nodep->isOverlapped()) {
nodep->replaceWith(new AstLogOr{flp, new AstLogNot{flp, lhsp}, rhsp});
} else {

335
src/V3AssertProp.cpp
View File

@ -39,6 +39,7 @@
#include "V3AssertProp.h"
#include "V3Graph.h"
#include "V3UniqueNames.h"
VL_DEFINE_DEBUG_FUNCTIONS;
@ -101,6 +102,338 @@ public:
string dotColor() const override { return m_ifBranch ? "green" : "red"; }
};
// Check whether a subtree contains any AstSExpr (multi-cycle sequence)
static bool containsSExpr(const AstNode* nodep) {
return !nodep->forall([](const AstSExpr*) { return false; });
}
// A single step in a sequence timeline: delay cycles followed by an expression check
struct SeqStep final {
int delayCycles; // Cycle delay before this check (0 for first step)
AstNodeExpr* exprp; // Expression to evaluate at this step
};
// Extract a timeline of (delay, expression) pairs from a sequence expression.
// For a plain expression, returns a single step with delay 0.
// For AstSExpr chains like `a ##1 b ##2 c`, returns [{0,a}, {1,b}, {2,c}].
static std::vector<SeqStep> extractTimeline(AstNodeExpr* nodep) {
std::vector<SeqStep> timeline;
if (AstSExpr* const sexprp = VN_CAST(nodep, SExpr)) {
// Recursively extract from the inner (preExprp) chain first
if (sexprp->preExprp()) {
if (AstSExpr* const preSExprp = VN_CAST(sexprp->preExprp(), SExpr)) {
// preExprp is itself a sequence -- extract its timeline
timeline = extractTimeline(preSExprp);
} else {
// preExprp is a plain expression -- first step at cycle 0
timeline.push_back({0, sexprp->preExprp()});
}
}
// Get cycle delay from delayp
int cycles = 0;
if (AstDelay* const dlyp = VN_CAST(sexprp->delayp(), Delay)) {
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");
}
}
// The expression after the delay
if (AstSExpr* const innerSExprp = VN_CAST(sexprp->exprp(), SExpr)) {
// Nested SExpr: extract its timeline and offset by current delay
std::vector<SeqStep> inner = extractTimeline(innerSExprp);
if (!inner.empty()) {
inner[0].delayCycles += cycles;
for (auto& step : inner) timeline.push_back(step);
}
} else {
timeline.push_back({cycles, sexprp->exprp()});
}
} else {
// Plain boolean expression -- single step, no delay
timeline.push_back({0, nodep});
}
return timeline;
}
// Lower sequence and/or to AST
class AssertPropLowerVisitor final : public VNVisitor {
// STATE
AstNodeModule* m_modp = nullptr; // Current module
V3UniqueNames m_seqBrNames{"__VseqBr"}; // Sequence branch dead-tracking name generator
// Lower a multi-cycle sequence 'and' to an AstPExpr with interleaved if/delay AST.
void lowerSeqAnd(AstNodeBiop* nodep) {
FileLine* const flp = nodep->fileline();
// Extract timelines from both operands
const std::vector<SeqStep> lhsTimeline = extractTimeline(nodep->lhsp());
const std::vector<SeqStep> rhsTimeline = extractTimeline(nodep->rhsp());
// Compute absolute cycle for each step
struct AbsStep final {
int cycle;
AstNodeExpr* exprp;
int branchId; // 0=lhs, 1=rhs
};
std::vector<AbsStep> allSteps;
int absCycle = 0;
for (const auto& step : lhsTimeline) {
absCycle += step.delayCycles;
allSteps.push_back({absCycle, step.exprp, 0});
}
const int lhsMaxCycle = absCycle;
absCycle = 0;
for (const auto& step : rhsTimeline) {
absCycle += step.delayCycles;
allSteps.push_back({absCycle, step.exprp, 1});
}
const int rhsMaxCycle = absCycle;
const int maxCycle = std::max(lhsMaxCycle, rhsMaxCycle);
// Sort by absolute cycle, then by branch id
std::stable_sort(allSteps.begin(), allSteps.end(), [](const AbsStep& a, const AbsStep& b) {
if (a.cycle != b.cycle) return a.cycle < b.cycle;
return a.branchId < b.branchId;
});
// Build AstPExprClause terminals
auto makePass = [&]() -> AstPExprClause* { return new AstPExprClause{flp, true}; };
auto makeFail = [&]() -> AstPExprClause* { return new AstPExprClause{flp, false}; };
{
// AND: all checks must pass. Generate nested if/delay chain.
// Group steps by cycle, combine same-cycle checks with LogAnd.
// Build from innermost (last cycle) outward.
// Group steps by cycle
std::map<int, std::vector<AstNodeExpr*>> cycleChecks;
for (const auto& step : allSteps) {
cycleChecks[step.cycle].push_back(step.exprp->cloneTree(false));
}
// Build from the last cycle inward
AstNode* innerp = makePass();
int prevCycle = maxCycle;
for (auto it = cycleChecks.rbegin(); it != cycleChecks.rend(); ++it) {
const int cycle = it->first;
auto& exprs = it->second;
// Combine all expressions at this cycle with LogAnd
AstNodeExpr* condp = new AstSampled{flp, exprs[0]};
condp->dtypeSetBit();
for (size_t i = 1; i < exprs.size(); ++i) {
AstNodeExpr* const rp = new AstSampled{flp, exprs[i]};
rp->dtypeSetBit();
condp = new AstLogAnd{flp, condp, rp};
condp->dtypeSetBit();
}
// Wrap in if: if (cond) { delay + inner } else { fail }
AstBegin* const thenp = new AstBegin{flp, "", nullptr, true};
// Add delay if needed (from this cycle to previous inner cycle)
if (prevCycle > cycle) {
const int delayCycles = prevCycle - cycle;
AstDelay* const dlyp = new AstDelay{
flp, new AstConst{flp, static_cast<uint32_t>(delayCycles)}, true};
thenp->addStmtsp(dlyp);
dlyp->addStmtsp(innerp);
} else {
thenp->addStmtsp(innerp);
}
AstIf* const ifp = new AstIf{flp, condp, thenp, makeFail()};
innerp = ifp;
prevCycle = cycle;
}
// Wrap in AstPExpr
AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true};
bodyp->addStmtsp(innerp);
AstPExpr* const pexprp = new AstPExpr{flp, bodyp, nodep->dtypep()};
nodep->replaceWith(pexprp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
}
// Lower a multi-cycle sequence 'or' to an AstPExpr with dead-tracking variables.
// IEEE 1800-2023 16.9.7: composite matches if at least one operand sequence matches.
// Both branches are evaluated independently from the same start cycle.
void lowerSeqOr(AstNodeBiop* nodep) {
UASSERT_OBJ(m_modp, nodep, "SOr not under a module");
FileLine* const flp = nodep->fileline();
// Extract timelines from both operands
const std::vector<SeqStep> lhsTimeline = extractTimeline(nodep->lhsp());
const std::vector<SeqStep> rhsTimeline = extractTimeline(nodep->rhsp());
// Compute absolute cycle for each step, mark which is last per branch
struct AbsStep final {
int cycle;
AstNodeExpr* exprp;
int branchId;
};
std::vector<AbsStep> allSteps;
int absCycle = 0;
for (const auto& step : lhsTimeline) {
absCycle += step.delayCycles;
allSteps.push_back({absCycle, step.exprp, 0});
}
const int br0MaxCycle = absCycle;
absCycle = 0;
for (const auto& step : rhsTimeline) {
absCycle += step.delayCycles;
allSteps.push_back({absCycle, step.exprp, 1});
}
const int br1MaxCycle = absCycle;
// Group by cycle, preserving branch info
struct CycleEntry final {
int branchId;
AstNodeExpr* exprp;
};
std::map<int, std::vector<CycleEntry>> cycleChecks;
for (const auto& step : allSteps) {
cycleChecks[step.cycle].push_back({step.branchId, step.exprp});
}
// Create dead-tracking variables at module level
AstVar* const br0Deadp = new AstVar{flp, VVarType::MODULETEMP, m_seqBrNames.get("0_dead"),
VFlagBitPacked{}, 1};
br0Deadp->lifetime(VLifetime::STATIC_EXPLICIT);
AstVar* const br1Deadp = new AstVar{flp, VVarType::MODULETEMP, m_seqBrNames.get("1_dead"),
VFlagBitPacked{}, 1};
br1Deadp->lifetime(VLifetime::STATIC_EXPLICIT);
m_modp->addStmtsp(br0Deadp);
m_modp->addStmtsp(br1Deadp);
auto makePass = [&]() -> AstPExprClause* { return new AstPExprClause{flp, true}; };
auto makeFail = [&]() -> AstPExprClause* { return new AstPExprClause{flp, false}; };
// Build from innermost (last cycle) outward, same nesting pattern as and
AstNode* innerp = nullptr;
int nextCycle = -1;
for (auto rit = cycleChecks.rbegin(); rit != cycleChecks.rend(); ++rit) {
const int cycle = rit->first;
AstBegin* const cycleBlock = new AstBegin{flp, "", nullptr, true};
// For each branch's check at this cycle
for (const auto& entry : rit->second) {
AstVar* const deadVarp = (entry.branchId == 0) ? br0Deadp : br1Deadp;
const int brMaxCycle = (entry.branchId == 0) ? br0MaxCycle : br1MaxCycle;
const bool isLast = (cycle == brMaxCycle);
AstNodeExpr* const sampledp = new AstSampled{flp, entry.exprp->cloneTree(false)};
sampledp->dtypeSetBit();
AstNodeExpr* const alivep
= new AstLogNot{flp, new AstVarRef{flp, deadVarp, VAccess::READ}};
alivep->dtypeSetBit();
if (isLast) {
// Last check: alive && passes -> pass
AstNodeExpr* const passCond = new AstLogAnd{flp, alivep, sampledp};
passCond->dtypeSetBit();
cycleBlock->addStmtsp(new AstIf{flp, passCond, makePass()});
// alive && fails -> dead
AstNodeExpr* const alive2p
= new AstLogNot{flp, new AstVarRef{flp, deadVarp, VAccess::READ}};
alive2p->dtypeSetBit();
AstNodeExpr* const failCond = new AstLogAnd{
flp, alive2p, new AstLogNot{flp, sampledp->cloneTree(false)}};
failCond->dtypeSetBit();
cycleBlock->addStmtsp(
new AstIf{flp, failCond,
new AstAssign{flp, new AstVarRef{flp, deadVarp, VAccess::WRITE},
new AstConst{flp, AstConst::BitTrue{}}}});
} else {
// Non-last: alive && fails -> dead
AstNodeExpr* const failCond
= new AstLogAnd{flp, alivep, new AstLogNot{flp, sampledp}};
failCond->dtypeSetBit();
cycleBlock->addStmtsp(
new AstIf{flp, failCond,
new AstAssign{flp, new AstVarRef{flp, deadVarp, VAccess::WRITE},
new AstConst{flp, AstConst::BitTrue{}}}});
}
}
// Both dead -> fail
AstNodeExpr* const allDeadp
= new AstLogAnd{flp, new AstVarRef{flp, br0Deadp, VAccess::READ},
new AstVarRef{flp, br1Deadp, VAccess::READ}};
allDeadp->dtypeSetBit();
cycleBlock->addStmtsp(new AstIf{flp, allDeadp, makeFail()});
// Nest delay + inner from later cycles
if (nextCycle > cycle && innerp) {
AstDelay* const dlyp = new AstDelay{
flp, new AstConst{flp, static_cast<uint32_t>(nextCycle - cycle)}, true};
cycleBlock->addStmtsp(dlyp);
dlyp->addStmtsp(innerp);
}
innerp = cycleBlock;
nextCycle = cycle;
}
// Wrap in AstPExpr with initialization
AstBegin* const bodyp = new AstBegin{flp, "", nullptr, true};
bodyp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, br0Deadp, VAccess::WRITE},
new AstConst{flp, AstConst::BitFalse{}}});
bodyp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, br1Deadp, VAccess::WRITE},
new AstConst{flp, AstConst::BitFalse{}}});
bodyp->addStmtsp(innerp);
AstPExpr* const pexprp = new AstPExpr{flp, bodyp, nodep->dtypep()};
nodep->replaceWith(pexprp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
void visit(AstSAnd* nodep) override {
iterateChildren(nodep);
if (containsSExpr(nodep->lhsp()) || containsSExpr(nodep->rhsp())) {
lowerSeqAnd(nodep);
} else {
// Pure boolean operands: 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())) {
lowerSeqOr(nodep);
} else {
// Pure boolean operands: lower to LogOr
AstLogOr* const newp = new AstLogOr{nodep->fileline(), nodep->lhsp()->unlinkFrBack(),
nodep->rhsp()->unlinkFrBack()};
newp->dtypeFrom(nodep);
nodep->replaceWith(newp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
}
}
void visit(AstNodeModule* nodep) override {
VL_RESTORER(m_modp);
m_modp = nodep;
iterateChildren(nodep);
}
void visit(AstNode* nodep) override { iterateChildren(nodep); }
void visit(AstConstPool* nodep) override {}
public:
explicit AssertPropLowerVisitor(AstNetlist* nodep) { iterate(nodep); }
~AssertPropLowerVisitor() override = default;
};
// Parse properties and ensemble a property tree graph
class AssertPropBuildVisitor final : public VNVisitorConst {
// STATE
@ -172,6 +505,7 @@ class AssertPropBuildVisitor final : public VNVisitorConst {
m_lastVtxp = dlyVtxp;
}
}
void visit(AstSOr* nodep) override {} // All SOr lowered by AssertPropLowerVisitor
void visit(AstNode* nodep) override { iterateChildrenConst(nodep); }
void visit(AstConstPool* nodep) override {}
@ -255,6 +589,7 @@ public:
void V3AssertProp::assertPropAll(AstNetlist* nodep) {
UINFO(2, __FUNCTION__ << ":");
{ AssertPropLowerVisitor{nodep}; }
{
V3Graph graph;
{ AssertPropBuildVisitor{nodep, graph}; }

44
src/V3AstNodeExpr.h
View File

@ -3617,6 +3617,50 @@ public:
int instrCount() const override { return widthInstrs() * 2; }
bool stringFlavor() const override { return true; }
};
class AstSAnd final : public AstNodeBiop {
// Sequence 'and' (IEEE 1800-2023 16.9.5): both operand sequences must match.
// Operates on match sets, not values. For boolean operands, lowered to AstLogAnd.
public:
AstSAnd(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp)
: ASTGEN_SUPER_SAnd(fl, lhsp, rhsp) {
dtypeSetBit();
}
ASTGEN_MEMBERS_AstSAnd;
void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override {
out.opLogAnd(lhs, rhs);
}
string emitVerilog() override { return "%k(%l %fand %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; }
};
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.
public:
AstSOr(FileLine* fl, AstNodeExpr* lhsp, AstNodeExpr* rhsp)
: ASTGEN_SUPER_SOr(fl, lhsp, rhsp) {
dtypeSetBit();
}
ASTGEN_MEMBERS_AstSOr;
void numberOperate(V3Number& out, const V3Number& lhs, const V3Number& rhs) override {
out.opLogOr(lhs, rhs);
}
string emitVerilog() override { return "%k(%l %for %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; }
};
class AstSel final : public AstNodeBiop {
// *Resolved* (tyep checked) multiple bit range extraction. Always const width
// @astgen alias op1 := fromp

3
src/V3Dfg.cpp
View File

@ -691,6 +691,9 @@ void DfgVertex::typeCheck(const DfgGraph& dfg) const {
return;
}
case VDfgType::SAnd:
case VDfgType::SOr: UASSERT_OBJ(false, this, "SAnd/SOr should be removed before DFG"); return;
case VDfgType::LogAnd:
case VDfgType::LogEq:
case VDfgType::LogIf:

4
src/V3DfgCse.cpp
View File

@ -123,6 +123,8 @@ class V3DfgCse final {
case VDfgType::ShiftRS:
case VDfgType::StreamL:
case VDfgType::StreamR:
case VDfgType::SAnd:
case VDfgType::SOr:
case VDfgType::Sub:
case VDfgType::Xor: return V3Hash{};
}
@ -240,6 +242,8 @@ class V3DfgCse final {
case VDfgType::ShiftR:
case VDfgType::ShiftRS:
case VDfgType::StreamL:
case VDfgType::SAnd:
case VDfgType::SOr:
case VDfgType::StreamR:
case VDfgType::Sub:
case VDfgType::Xor: return true;

3
src/V3Width.cpp
View File

@ -293,6 +293,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
void visit(AstSAnd* 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
visit_log_and_or(nodep);

11
src/verilog.y
View File

@ -6815,13 +6815,14 @@ sexpr<nodeExprp>: // ==IEEE: sequence_expr (The name sexpr is important as reg
| '(' ~p~sexpr ',' sequence_match_itemList ')'
{ $$ = new AstExprStmt{$3, $4, $2}; }
//
// // AND/OR are between pexprs OR sexprs
// // AND/OR are between pexprs OR sexprs (IEEE 1800-2023 16.9.2, 16.11.2)
// // For expression-level (boolean) operands, AstLogAnd/AstLogOr is correct.
// // For temporal sequence operands (containing ##), the downstream
// // V3Width "Implication with sequence expression" check will catch them.
| ~p~sexpr yAND ~p~sexpr
{ $$ = new AstLogAnd{$2, $1, $3};
BBUNSUP($2, "Unsupported: and (in sequence expression)"); }
{ $$ = new AstSAnd{$2, $1, $3}; }
| ~p~sexpr yOR ~p~sexpr
{ $$ = new AstLogOr{$2, $1, $3};
BBUNSUP($2, "Unsupported: or (in sequence expression)"); }
{ $$ = 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); }

6
test_regress/t/t_property_unsup.out
View File

@ -14,15 +14,9 @@
%Error-UNSUPPORTED: t/t_property_unsup.v:92:26: Unsupported: always (in property expression)
92 | assert property ((a or(always b)) implies (a or(always b)));
| ^~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:92:23: Unsupported: or (in sequence expression)
92 | assert property ((a or(always b)) implies (a or(always b)));
| ^~
%Error-UNSUPPORTED: t/t_property_unsup.v:92:51: Unsupported: always (in property expression)
92 | assert property ((a or(always b)) implies (a or(always b)));
| ^~~~~~
%Error-UNSUPPORTED: t/t_property_unsup.v:92:48: Unsupported: or (in sequence expression)
92 | assert property ((a or(always b)) implies (a or(always b)));
| ^~
%Error-UNSUPPORTED: t/t_property_unsup.v:94:21: Unsupported: eventually[] (in property expression)
94 | assert property ((eventually[0: 1] a) implies (eventually[0: 1] a));
| ^~~~~~~~~~

18
test_regress/t/t_sequence_bool_ops.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(timing_loop=True, verilator_flags2=['--assert', '--timing'])
test.execute()
test.passes()

104
test_regress/t/t_sequence_bool_ops.v Normal file
View File

@ -0,0 +1,104 @@
// 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];
// Aggregate outputs into a single result vector
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 and/or (single-cycle, CRC-driven antecedent)
// =========================================================================
// Boolean 'and': (a and b) true iff a && b
assert property (@(posedge clk) disable iff (cyc < 2)
(a and b) |-> (a & b));
// Boolean 'or': (a or b) true iff a || b
assert property (@(posedge clk) disable iff (cyc < 2)
(a or b) |-> (a | b));
// 'and' with constant true -- reduces to just 'a'
assert property (@(posedge clk) disable iff (cyc < 2)
(a and 1'b1) |-> a);
// 'or' with constant false -- reduces to just 'a'
assert property (@(posedge clk) disable iff (cyc < 2)
(a or 1'b0) |-> a);
// =========================================================================
// Multi-cycle sequence and (IEEE 1800-2023 16.9.5)
// CRC-driven: antecedent gates when sequence starts, consequent guaranteed
// =========================================================================
// Sequence 'and': both branches must complete, same length
assert property (@(posedge clk)
(a & b) |-> (a ##1 1'b1) and (b ##1 1'b1));
// Sequence 'and': different lengths, end at later branch
assert property (@(posedge clk)
(a & b) |-> (a ##1 1'b1) and (b ##2 1'b1));
// Sequence 'and': standalone (constant, always passes)
assert property (@(posedge clk)
(1'b1 ##1 1'b1) and (1'b1 ##2 1'b1));
// =========================================================================
// Multi-cycle sequence or (IEEE 1800-2023 16.9.7)
// CRC-driven: at least one branch must complete
// =========================================================================
// Sequence 'or': same length, CRC-driven
assert property (@(posedge clk)
(a | b) |-> (a ##1 1'b1) or (b ##1 1'b1));
// Sequence 'or': different lengths, CRC-driven
assert property (@(posedge clk)
(a | b) |-> (a ##1 1'b1) or (b ##2 1'b1));
// Sequence 'or': standalone (constant, always passes)
assert property (@(posedge clk)
(1'b1 ##1 1'b1) or (1'b1 ##2 1'b1));
endmodule

14
test_regress/t/t_sequence_first_match_unsup.out
View File

@ -1,19 +1,7 @@
%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:51:41: Unsupported: or (in sequence expression)
51 | initial p0 : assert property ((##1 1) or(##2 1) |-> x == 1);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:54: Unsupported: or (in sequence expression)
54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1);
| ^~
%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:54:33: Unsupported: first_match (in sequence expression)
54 | initial p1 : assert property (first_match ((##1 1) or(##2 1)) |-> x == 1);
| ^~~~~~~~~~~
%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:57:35: Unsupported: or (in sequence expression)
57 | initial p2 : assert property (1 or ##1 1 |-> x == 0);
| ^~
%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:48: Unsupported: or (in sequence expression)
60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0);
| ^~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error-UNSUPPORTED: t/t_sequence_first_match_unsup.v:60:33: Unsupported: first_match (in sequence expression)
60 | initial p3 : assert property (first_match (1 or ##1 1) |-> x == 0);
| ^~~~~~~~~~~

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

@ -0,0 +1,6 @@
%Error-UNSUPPORTED: t/t_sequence_nonconst_delay_unsup.v:14:40: Unsupported: non-constant cycle delay in sequence and/or
: ... note: In instance 't'
14 | assert property (@(posedge clk) (a ##delay b) and (c ##1 d));
| ^~~~~
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
%Error: Exiting due to

16
test_regress/t/t_sequence_nonconst_delay_unsup.py Executable file
View File

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

16
test_regress/t/t_sequence_nonconst_delay_unsup.v Normal file
View File

@ -0,0 +1,16 @@
// 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;
int delay = 1;
// Non-constant cycle delay in sequence and/or is unsupported
assert property (@(posedge clk) (a ##delay b) and (c ##1 d));
endmodule

6
test_regress/t/t_sequence_sexpr_unsup.out
View File

@ -2,12 +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:38:7: Unsupported: and (in sequence expression)
38 | a and b;
| ^~~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:42:7: Unsupported: or (in sequence expression)
42 | a or b;
| ^~
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:46:7: Unsupported: throughout (in sequence expression)
46 | a throughout b;
| ^~~~~~~~~~