From 0b2bf991a6d8b0b98c6a4f2e87d02c9192bda93a Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Tue, 24 Mar 2026 13:56:14 +0100 Subject: [PATCH] Support boolean and/or in sequence expressions (#7285) --- src/V3AssertPre.cpp | 2 + src/V3AssertProp.cpp | 335 ++++++++++++++++++ src/V3AstNodeExpr.h | 44 +++ src/V3Dfg.cpp | 3 + src/V3DfgCse.cpp | 4 + src/V3Width.cpp | 3 + src/verilog.y | 11 +- test_regress/t/t_property_unsup.out | 6 - test_regress/t/t_sequence_bool_ops.py | 18 + test_regress/t/t_sequence_bool_ops.v | 104 ++++++ .../t/t_sequence_first_match_unsup.out | 14 +- .../t/t_sequence_nonconst_delay_unsup.out | 6 + .../t/t_sequence_nonconst_delay_unsup.py | 16 + .../t/t_sequence_nonconst_delay_unsup.v | 16 + test_regress/t/t_sequence_sexpr_unsup.out | 6 - 15 files changed, 558 insertions(+), 30 deletions(-) create mode 100755 test_regress/t/t_sequence_bool_ops.py create mode 100644 test_regress/t/t_sequence_bool_ops.v create mode 100644 test_regress/t/t_sequence_nonconst_delay_unsup.out create mode 100755 test_regress/t/t_sequence_nonconst_delay_unsup.py create mode 100644 test_regress/t/t_sequence_nonconst_delay_unsup.v diff --git a/src/V3AssertPre.cpp b/src/V3AssertPre.cpp index 6bc153135..13287998f 100644 --- a/src/V3AssertPre.cpp +++ b/src/V3AssertPre.cpp @@ -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 { diff --git a/src/V3AssertProp.cpp b/src/V3AssertProp.cpp index 6cc674c9f..30ca88fb2 100644 --- a/src/V3AssertProp.cpp +++ b/src/V3AssertProp.cpp @@ -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 extractTimeline(AstNodeExpr* nodep) { + std::vector 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 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 lhsTimeline = extractTimeline(nodep->lhsp()); + const std::vector 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 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> 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(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 lhsTimeline = extractTimeline(nodep->lhsp()); + const std::vector 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 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> 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(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}; } diff --git a/src/V3AstNodeExpr.h b/src/V3AstNodeExpr.h index c469fad3d..9f5323679 100644 --- a/src/V3AstNodeExpr.h +++ b/src/V3AstNodeExpr.h @@ -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 diff --git a/src/V3Dfg.cpp b/src/V3Dfg.cpp index 12c2bc6b1..05172e348 100644 --- a/src/V3Dfg.cpp +++ b/src/V3Dfg.cpp @@ -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: diff --git a/src/V3DfgCse.cpp b/src/V3DfgCse.cpp index b1f9241e5..d1831b752 100644 --- a/src/V3DfgCse.cpp +++ b/src/V3DfgCse.cpp @@ -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; diff --git a/src/V3Width.cpp b/src/V3Width.cpp index 3e58a3481..eec39fe8a 100644 --- a/src/V3Width.cpp +++ b/src/V3Width.cpp @@ -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); diff --git a/src/verilog.y b/src/verilog.y index ba3fc230d..68193b70c 100644 --- a/src/verilog.y +++ b/src/verilog.y @@ -6815,13 +6815,14 @@ sexpr: // ==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); } diff --git a/test_regress/t/t_property_unsup.out b/test_regress/t/t_property_unsup.out index 0f5bb8cdc..0be572e64 100644 --- a/test_regress/t/t_property_unsup.out +++ b/test_regress/t/t_property_unsup.out @@ -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)); | ^~~~~~~~~~ diff --git a/test_regress/t/t_sequence_bool_ops.py b/test_regress/t/t_sequence_bool_ops.py new file mode 100755 index 000000000..35e44000c --- /dev/null +++ b/test_regress/t/t_sequence_bool_ops.py @@ -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() diff --git a/test_regress/t/t_sequence_bool_ops.v b/test_regress/t/t_sequence_bool_ops.v new file mode 100644 index 000000000..55e00987d --- /dev/null +++ b/test_regress/t/t_sequence_bool_ops.v @@ -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 diff --git a/test_regress/t/t_sequence_first_match_unsup.out b/test_regress/t/t_sequence_first_match_unsup.out index a64703292..a7541ad3a 100644 --- a/test_regress/t/t_sequence_first_match_unsup.out +++ b/test_regress/t/t_sequence_first_match_unsup.out @@ -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); | ^~~~~~~~~~~ diff --git a/test_regress/t/t_sequence_nonconst_delay_unsup.out b/test_regress/t/t_sequence_nonconst_delay_unsup.out new file mode 100644 index 000000000..8d1555846 --- /dev/null +++ b/test_regress/t/t_sequence_nonconst_delay_unsup.out @@ -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 diff --git a/test_regress/t/t_sequence_nonconst_delay_unsup.py b/test_regress/t/t_sequence_nonconst_delay_unsup.py new file mode 100755 index 000000000..63487ba49 --- /dev/null +++ b/test_regress/t/t_sequence_nonconst_delay_unsup.py @@ -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() diff --git a/test_regress/t/t_sequence_nonconst_delay_unsup.v b/test_regress/t/t_sequence_nonconst_delay_unsup.v new file mode 100644 index 000000000..27d941f2c --- /dev/null +++ b/test_regress/t/t_sequence_nonconst_delay_unsup.v @@ -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 diff --git a/test_regress/t/t_sequence_sexpr_unsup.out b/test_regress/t/t_sequence_sexpr_unsup.out index ae547a2d0..33cf25b94 100644 --- a/test_regress/t/t_sequence_sexpr_unsup.out +++ b/test_regress/t/t_sequence_sexpr_unsup.out @@ -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; | ^~~~~~~~~~