Support ##[M:N] range cycle delay in SVA sequences (#7312)
This commit is contained in:
Yilou Wang
GitHub
parent
afa071a822
commit
3ddf7ad6ec
|
|
@ -38,6 +38,7 @@
|
|||
|
||||
#include "V3AssertProp.h"
|
||||
|
||||
#include "V3Const.h"
|
||||
#include "V3Graph.h"
|
||||
#include "V3UniqueNames.h"
|
||||
|
||||
|
|
@ -584,11 +585,417 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
//######################################################################
|
||||
// Range delay expansion (runs before DFA builder)
|
||||
//
|
||||
// Replaces ##[M:N] range delays with a module-level FSM (always block
|
||||
// + state/counter vars). No coroutine overhead -- one state advance
|
||||
// per clock cycle. The SExpr becomes a !fail combinational check.
|
||||
|
||||
class RangeDelayExpander final : public VNVisitor {
|
||||
// STATE
|
||||
V3UniqueNames m_names{"__Vrangedly"};
|
||||
AstNodeModule* m_modp = nullptr; // Current module
|
||||
std::vector<AstNode*> m_toDelete; // Nodes to delete after traversal
|
||||
|
||||
struct SeqStep final {
|
||||
AstNodeExpr* exprp; // Expression to check (nullptr if unary leading delay)
|
||||
int delay; // Fixed delay after this expression (0 for tail)
|
||||
bool isRange; // Whether this step's delay is a range
|
||||
int rangeMin;
|
||||
int rangeMax;
|
||||
};
|
||||
|
||||
// Extract delay bounds from AstDelay. Clones and constifies (does not modify original AST).
|
||||
bool extractDelayBounds(AstDelay* dlyp, bool& isRange, int& minVal, int& maxVal) {
|
||||
isRange = dlyp->isRangeDelay();
|
||||
AstNodeExpr* const minExprp = V3Const::constifyEdit(dlyp->lhsp()->cloneTree(false));
|
||||
const AstConst* const minConstp = VN_CAST(minExprp, Const);
|
||||
if (isRange) {
|
||||
AstNodeExpr* const maxExprp = V3Const::constifyEdit(dlyp->rhsp()->cloneTree(false));
|
||||
const AstConst* const maxConstp = VN_CAST(maxExprp, Const);
|
||||
if (!minConstp || !maxConstp) {
|
||||
dlyp->v3error("Range delay bounds must be elaboration-time constants"
|
||||
" (IEEE 1800-2023 16.7)");
|
||||
VL_DO_DANGLING(minExprp->deleteTree(), minExprp);
|
||||
VL_DO_DANGLING(maxExprp->deleteTree(), maxExprp);
|
||||
return false;
|
||||
}
|
||||
minVal = minConstp->toSInt();
|
||||
maxVal = maxConstp->toSInt();
|
||||
VL_DO_DANGLING(minExprp->deleteTree(), minExprp);
|
||||
VL_DO_DANGLING(maxExprp->deleteTree(), maxExprp);
|
||||
if (minVal < 0 || maxVal < 0) {
|
||||
dlyp->v3error("Range delay bounds must be non-negative"
|
||||
" (IEEE 1800-2023 16.7)");
|
||||
return false;
|
||||
}
|
||||
if (maxVal < minVal) {
|
||||
dlyp->v3error("Range delay maximum must be >= minimum"
|
||||
" (IEEE 1800-2023 16.7)");
|
||||
return false;
|
||||
}
|
||||
if (minVal == 0) {
|
||||
dlyp->v3warn(E_UNSUPPORTED, "Unsupported: ##0 in range delays");
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
minVal = maxVal = minConstp ? minConstp->toSInt() : 0;
|
||||
VL_DO_DANGLING(minExprp->deleteTree(), minExprp);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
// Flatten a (possibly nested) SExpr tree into a linear vector of SeqSteps.
|
||||
// SExpr trees are left-recursive: (a ##[1:2] b) ##1 c becomes
|
||||
// SExpr(pre=SExpr(a, ##[1:2], b), ##1, c)
|
||||
// Output for that example: [{a, range[1:2]}, {b, delay=1}, {c, delay=0}]
|
||||
bool linearize(AstSExpr* rootp, std::vector<SeqStep>& steps) {
|
||||
bool hasRange = false;
|
||||
linearizeImpl(rootp, steps, hasRange /*ref*/);
|
||||
return hasRange;
|
||||
}
|
||||
|
||||
bool linearizeImpl(AstSExpr* curp, std::vector<SeqStep>& steps, bool& hasRange) {
|
||||
if (AstSExpr* const prep = VN_CAST(curp->preExprp(), SExpr)) {
|
||||
if (!linearizeImpl(prep, steps, hasRange)) return false;
|
||||
}
|
||||
AstDelay* const dlyp = VN_CAST(curp->delayp(), Delay);
|
||||
UASSERT_OBJ(dlyp, curp, "Expected AstDelay");
|
||||
bool isRange = false;
|
||||
int minVal = 0, maxVal = 0;
|
||||
if (!extractDelayBounds(dlyp, isRange, minVal, maxVal)) return false;
|
||||
if (isRange) hasRange = true;
|
||||
|
||||
if (curp->preExprp() && !VN_IS(curp->preExprp(), SExpr)) {
|
||||
steps.push_back({curp->preExprp(), minVal, isRange, minVal, maxVal});
|
||||
} else {
|
||||
steps.push_back({nullptr, minVal, isRange, minVal, maxVal});
|
||||
}
|
||||
|
||||
if (AstSExpr* const nextp = VN_CAST(curp->exprp(), SExpr)) {
|
||||
return linearizeImpl(nextp, steps, hasRange);
|
||||
}
|
||||
steps.push_back({curp->exprp(), 0, false, 0, 0});
|
||||
return true;
|
||||
}
|
||||
|
||||
// Build FSM body as if/else chain on state variable.
|
||||
// State 0 = IDLE. Each range delay adds 2 states (wait + check),
|
||||
// each fixed delay adds 1 (wait), each tail expr adds 1 (check).
|
||||
//
|
||||
// Example: a ##[M:N] b ##1 c
|
||||
// steps: [{a, range[M:N]}, {b, delay=1}, {c, delay=0}]
|
||||
// State 1: WAIT_MIN (count down M cycles)
|
||||
// State 2: CHECK_RANGE (check b each cycle, up to N-M retries)
|
||||
// State 3: WAIT_FIXED (count down 1 cycle for ##1)
|
||||
// State 4: CHECK_TAIL (check c, report pass/fail)
|
||||
AstNode* buildFsmBody(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, AstVar* failVarp,
|
||||
const std::vector<SeqStep>& steps, AstSenItem* sensesp,
|
||||
AstNodeExpr* antExprp) {
|
||||
|
||||
AstNode* fsmChainp = nullptr;
|
||||
int nextState = 1;
|
||||
|
||||
for (size_t i = 0; i < steps.size(); ++i) {
|
||||
const SeqStep& step = steps[i];
|
||||
|
||||
if (step.isRange) {
|
||||
// Range delay needs two states: WAIT_MIN and CHECK_RANGE
|
||||
UASSERT(i + 1 < steps.size(), "Range must have next step");
|
||||
const int waitState = nextState++;
|
||||
const int checkState = nextState++;
|
||||
const int rangeWidth = step.rangeMax - step.rangeMin;
|
||||
const SeqStep& nextStep = steps[i + 1];
|
||||
|
||||
const int afterMatchState = nextState;
|
||||
|
||||
// WAIT_MIN: count down rangeMin cycles
|
||||
{
|
||||
AstNode* const bodyp = new AstIf{
|
||||
flp,
|
||||
new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
|
||||
new AstConst{flp, 0}},
|
||||
makeStateTransition(flp, stateVarp, cntVarp, checkState, rangeWidth),
|
||||
new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE},
|
||||
new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
|
||||
new AstConst{flp, 1}}}};
|
||||
fsmChainp = chainState(flp, fsmChainp, stateVarp, waitState, bodyp);
|
||||
}
|
||||
|
||||
// CHECK_RANGE: check expr each cycle, fail on timeout
|
||||
{
|
||||
AstNode* matchActionp = nullptr;
|
||||
AstNode* const timeoutp = new AstBegin{flp, "", nullptr, true};
|
||||
VN_AS(timeoutp, Begin)
|
||||
->addStmtsp(new AstAssign{flp,
|
||||
new AstVarRef{flp, failVarp, VAccess::WRITE},
|
||||
new AstConst{flp, AstConst::BitTrue{}}});
|
||||
VN_AS(timeoutp, Begin)
|
||||
->addStmtsp(new AstAssign{flp,
|
||||
new AstVarRef{flp, stateVarp, VAccess::WRITE},
|
||||
new AstConst{flp, 0}});
|
||||
AstNode* const decrementp
|
||||
= new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE},
|
||||
new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
|
||||
new AstConst{flp, 1}}};
|
||||
|
||||
AstIf* const failOrRetryp
|
||||
= new AstIf{flp,
|
||||
new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
|
||||
new AstConst{flp, 0}},
|
||||
timeoutp, decrementp};
|
||||
|
||||
if (nextStep.delay > 0) {
|
||||
matchActionp = makeStateTransition(flp, stateVarp, cntVarp,
|
||||
afterMatchState, nextStep.delay - 1);
|
||||
} else {
|
||||
matchActionp
|
||||
= makeStateTransition(flp, stateVarp, cntVarp, afterMatchState, 0);
|
||||
}
|
||||
|
||||
AstIf* const checkp
|
||||
= new AstIf{flp, new AstSampled{flp, nextStep.exprp->cloneTree(false)},
|
||||
matchActionp, failOrRetryp};
|
||||
|
||||
fsmChainp = chainState(flp, fsmChainp, stateVarp, checkState, checkp);
|
||||
}
|
||||
|
||||
// Skip next step (already consumed as the range check target)
|
||||
++i;
|
||||
continue;
|
||||
|
||||
} else if (step.delay > 0) {
|
||||
// Fixed delay: count down then advance
|
||||
const int waitState = nextState++;
|
||||
AstNode* const bodyp = new AstIf{
|
||||
flp,
|
||||
new AstEq{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
|
||||
new AstConst{flp, 0}},
|
||||
new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE},
|
||||
new AstConst{flp, static_cast<uint32_t>(nextState)}},
|
||||
new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE},
|
||||
new AstSub{flp, new AstVarRef{flp, cntVarp, VAccess::READ},
|
||||
new AstConst{flp, 1}}}};
|
||||
|
||||
fsmChainp = chainState(flp, fsmChainp, stateVarp, waitState, bodyp);
|
||||
|
||||
} else if (i == steps.size() - 1 && step.exprp) {
|
||||
// Tail: check final expression, pass or fail
|
||||
const int checkState = nextState++;
|
||||
AstNode* const passp = new AstAssign{
|
||||
flp, new AstVarRef{flp, stateVarp, VAccess::WRITE}, new AstConst{flp, 0}};
|
||||
AstBegin* const failp = new AstBegin{flp, "", nullptr, true};
|
||||
failp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, failVarp, VAccess::WRITE},
|
||||
new AstConst{flp, AstConst::BitTrue{}}});
|
||||
failp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE},
|
||||
new AstConst{flp, 0}});
|
||||
|
||||
AstIf* const bodyp = new AstIf{
|
||||
flp, new AstSampled{flp, step.exprp->cloneTree(false)}, passp, failp};
|
||||
|
||||
fsmChainp = chainState(flp, fsmChainp, stateVarp, checkState, bodyp);
|
||||
}
|
||||
}
|
||||
|
||||
// Build IDLE state (state 0): check trigger and start
|
||||
AstNode* idleBodyp = nullptr;
|
||||
const SeqStep& firstStep = steps[0];
|
||||
int initCnt = 0;
|
||||
if (firstStep.isRange) {
|
||||
initCnt = firstStep.rangeMin - 1;
|
||||
} else {
|
||||
initCnt = firstStep.delay - 1;
|
||||
}
|
||||
AstNode* const startActionp
|
||||
= makeStateTransition(flp, stateVarp, cntVarp, 1, initCnt < 0 ? 0 : initCnt);
|
||||
|
||||
// Trigger = antecedent (from implication) AND/OR first step expression
|
||||
AstNodeExpr* triggerp = nullptr;
|
||||
if (antExprp && firstStep.exprp) {
|
||||
triggerp = new AstAnd{flp, new AstSampled{flp, antExprp->cloneTree(false)},
|
||||
new AstSampled{flp, firstStep.exprp->cloneTree(false)}};
|
||||
} else if (antExprp) {
|
||||
triggerp = new AstSampled{flp, antExprp->cloneTree(false)};
|
||||
} else if (firstStep.exprp) {
|
||||
triggerp = new AstSampled{flp, firstStep.exprp->cloneTree(false)};
|
||||
}
|
||||
|
||||
if (triggerp) {
|
||||
triggerp->dtypeSetBit();
|
||||
idleBodyp = new AstIf{flp, triggerp, startActionp, nullptr};
|
||||
} else {
|
||||
// Unary form with no antecedent: start unconditionally each cycle
|
||||
idleBodyp = startActionp;
|
||||
}
|
||||
|
||||
// Chain: if (state == 0) idle else if (state == 1) ... else ...
|
||||
AstIf* const idleIfp = new AstIf{
|
||||
flp,
|
||||
new AstEq{flp, new AstVarRef{flp, stateVarp, VAccess::READ}, new AstConst{flp, 0}},
|
||||
idleBodyp, fsmChainp};
|
||||
|
||||
// Reset fail flag at top of each cycle
|
||||
AstNode* const resetFailp
|
||||
= new AstAssign{flp, new AstVarRef{flp, failVarp, VAccess::WRITE},
|
||||
new AstConst{flp, AstConst::BitFalse{}}};
|
||||
resetFailp->addNext(idleIfp);
|
||||
return resetFailp;
|
||||
}
|
||||
|
||||
// Helper: generate state = newState; cnt = initCnt;
|
||||
AstNode* makeStateTransition(FileLine* flp, AstVar* stateVarp, AstVar* cntVarp, int newState,
|
||||
int initCnt) {
|
||||
AstBegin* const blockp = new AstBegin{flp, "", nullptr, true};
|
||||
blockp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, stateVarp, VAccess::WRITE},
|
||||
new AstConst{flp, static_cast<uint32_t>(newState)}});
|
||||
blockp->addStmtsp(new AstAssign{flp, new AstVarRef{flp, cntVarp, VAccess::WRITE},
|
||||
new AstConst{flp, static_cast<uint32_t>(initCnt)}});
|
||||
return blockp;
|
||||
}
|
||||
|
||||
// Helper: chain a state check into the if/else chain
|
||||
// Builds: if (state == stateNum) { body } else { existing chain }
|
||||
AstNode* chainState(FileLine* flp, AstNode* existingChainp, AstVar* stateVarp, int stateNum,
|
||||
AstNode* bodyp) {
|
||||
AstIf* const ifp = new AstIf{flp,
|
||||
new AstEq{flp, new AstVarRef{flp, stateVarp, VAccess::READ},
|
||||
new AstConst{flp, static_cast<uint32_t>(stateNum)}},
|
||||
bodyp, existingChainp};
|
||||
return ifp;
|
||||
}
|
||||
|
||||
// Recursively check if any delay in the SExpr tree is a range delay
|
||||
static bool containsRangeDelay(AstSExpr* nodep) {
|
||||
if (AstDelay* const dlyp = VN_CAST(nodep->delayp(), Delay)) {
|
||||
if (dlyp->isRangeDelay()) return true;
|
||||
}
|
||||
if (AstSExpr* const prep = VN_CAST(nodep->preExprp(), SExpr)) {
|
||||
if (containsRangeDelay(prep)) return true;
|
||||
}
|
||||
if (AstSExpr* const exprp = VN_CAST(nodep->exprp(), SExpr)) {
|
||||
if (containsRangeDelay(exprp)) return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
// Find the clock sensitivity for this SExpr by searching up the tree
|
||||
AstSenItem* findClock(AstNode* nodep) {
|
||||
for (AstNode* curp = nodep; curp; curp = curp->backp()) {
|
||||
if (AstPropSpec* const specp = VN_CAST(curp, PropSpec)) {
|
||||
if (specp->sensesp()) return specp->sensesp();
|
||||
}
|
||||
}
|
||||
nodep->v3fatalSrc("Range delay SExpr without clocking event");
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// Find implication antecedent if this SExpr is the RHS of |-> or |=>
|
||||
// The FSM absorbs the antecedent as its trigger so the implication node
|
||||
// can be removed -- otherwise fail timing wouldn't align with the trigger.
|
||||
std::pair<AstNodeExpr*, bool> findAntecedent(AstNode* nodep) {
|
||||
for (AstNode* curp = nodep; curp; curp = curp->backp()) {
|
||||
if (AstImplication* const implp = VN_CAST(curp, Implication)) {
|
||||
return {implp->lhsp(), implp->isOverlapped()};
|
||||
}
|
||||
}
|
||||
return {nullptr, false};
|
||||
}
|
||||
|
||||
// VISITORS
|
||||
void visit(AstNodeModule* nodep) override {
|
||||
VL_RESTORER(m_modp);
|
||||
m_modp = nodep;
|
||||
iterateChildren(nodep);
|
||||
}
|
||||
|
||||
void visit(AstSExpr* nodep) override {
|
||||
if (!containsRangeDelay(nodep)) {
|
||||
iterateChildren(nodep);
|
||||
return;
|
||||
}
|
||||
std::vector<SeqStep> steps;
|
||||
if (!linearize(nodep, steps)) {
|
||||
nodep->replaceWith(new AstConst{nodep->fileline(), AstConst::BitFalse{}});
|
||||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||
return;
|
||||
}
|
||||
|
||||
FileLine* const flp = nodep->fileline();
|
||||
|
||||
// Find clock for the FSM (unclocked assertions are caught by V3Assert)
|
||||
AstSenItem* const sensesp = findClock(nodep);
|
||||
UASSERT_OBJ(sensesp, nodep, "Range delay SExpr without clocking event");
|
||||
|
||||
UASSERT_OBJ(m_modp, nodep, "Range delay SExpr not under a module");
|
||||
|
||||
// Find antecedent (if inside implication)
|
||||
const std::pair<AstNodeExpr*, bool> antResult = findAntecedent(nodep);
|
||||
AstNodeExpr* const antExprp = antResult.first;
|
||||
// const bool isOverlapped = antResult.second; // Reserved for |=> support
|
||||
|
||||
// Create module-level state variables
|
||||
const std::string baseName = m_names.get(nodep);
|
||||
AstVar* const stateVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__state",
|
||||
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
|
||||
stateVarp->lifetime(VLifetime::STATIC_EXPLICIT);
|
||||
AstVar* const cntVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__cnt",
|
||||
nodep->findBasicDType(VBasicDTypeKwd::UINT32)};
|
||||
cntVarp->lifetime(VLifetime::STATIC_EXPLICIT);
|
||||
AstVar* const failVarp = new AstVar{flp, VVarType::MODULETEMP, baseName + "__fail",
|
||||
nodep->findBasicDType(VBasicDTypeKwd::BIT)};
|
||||
failVarp->lifetime(VLifetime::STATIC_EXPLICIT);
|
||||
|
||||
// Build FSM body
|
||||
AstNode* const fsmBodyp
|
||||
= buildFsmBody(flp, stateVarp, cntVarp, failVarp, steps, sensesp, antExprp);
|
||||
|
||||
// Create Always block for the FSM (same scheduling as assertion always blocks)
|
||||
AstAlways* const alwaysp = new AstAlways{
|
||||
flp, VAlwaysKwd::ALWAYS, new AstSenTree{flp, sensesp->cloneTree(false)}, fsmBodyp};
|
||||
|
||||
// Add state vars and always block to module
|
||||
m_modp->addStmtsp(stateVarp);
|
||||
m_modp->addStmtsp(cntVarp);
|
||||
m_modp->addStmtsp(failVarp);
|
||||
m_modp->addStmtsp(alwaysp);
|
||||
|
||||
// Replace with !fail expression (combinational check).
|
||||
// If inside an implication, replace the entire implication since
|
||||
// the FSM already handles the antecedent.
|
||||
AstNodeExpr* const checkp = new AstNot{flp, new AstVarRef{flp, failVarp, VAccess::READ}};
|
||||
checkp->dtypeSetBit();
|
||||
|
||||
if (antExprp) {
|
||||
// Find the implication, replace it with the check, defer deletion
|
||||
for (AstNode* curp = nodep->backp(); curp; curp = curp->backp()) {
|
||||
if (AstImplication* const implp = VN_CAST(curp, Implication)) {
|
||||
implp->replaceWith(checkp);
|
||||
m_toDelete.push_back(implp);
|
||||
break;
|
||||
}
|
||||
}
|
||||
} else {
|
||||
nodep->replaceWith(checkp);
|
||||
VL_DO_DANGLING(nodep->deleteTree(), nodep);
|
||||
}
|
||||
}
|
||||
|
||||
void visit(AstNode* nodep) override { iterateChildren(nodep); }
|
||||
|
||||
public:
|
||||
explicit RangeDelayExpander(AstNetlist* nodep) {
|
||||
iterate(nodep);
|
||||
for (AstNode* const np : m_toDelete) np->deleteTree();
|
||||
}
|
||||
};
|
||||
|
||||
//######################################################################
|
||||
// Top AssertProp class
|
||||
|
||||
void V3AssertProp::assertPropAll(AstNetlist* nodep) {
|
||||
UINFO(2, __FUNCTION__ << ":");
|
||||
{ RangeDelayExpander{nodep}; }
|
||||
{ AssertPropLowerVisitor{nodep}; }
|
||||
{
|
||||
V3Graph graph;
|
||||
|
|
|
|||
|
|
@ -541,8 +541,9 @@ public:
|
|||
};
|
||||
class AstDelay final : public AstNodeStmt {
|
||||
// Delay statement
|
||||
// @astgen op1 := lhsp : AstNodeExpr // Delay value
|
||||
// @astgen op1 := lhsp : AstNodeExpr // Delay value (or min for range)
|
||||
// @astgen op2 := stmtsp : List[AstNode] // Statements under delay
|
||||
// @astgen op3 := rhsp : Optional[AstNodeExpr] // Max delay value (range delay only)
|
||||
VTimescale m_timeunit; // Delay's time unit
|
||||
const bool m_isCycle; // True if it is a cycle delay
|
||||
|
||||
|
|
@ -560,6 +561,7 @@ public:
|
|||
void timeunit(const VTimescale& flag) { m_timeunit = flag; }
|
||||
VTimescale timeunit() const { return m_timeunit; }
|
||||
bool isCycleDelay() const { return m_isCycle; }
|
||||
bool isRangeDelay() const { return rhsp() != nullptr; }
|
||||
};
|
||||
class AstDisable final : public AstNodeStmt {
|
||||
// @astgen op1 := targetRefp : Optional[AstNodeExpr] // Reference to link in V3LinkDot
|
||||
|
|
|
|||
|
|
@ -6864,10 +6864,9 @@ cycle_delay_range<delayp>: // IEEE: ==cycle_delay_range
|
|||
// // UNSUP: This causes a big grammar ambiguity
|
||||
// // as ()'s mismatch between primary and the following statement
|
||||
// // the sv-ac committee has been asked to clarify (Mantis 1901)
|
||||
| yP_POUNDPOUND anyrange
|
||||
{ $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
|
||||
DEL($2);
|
||||
BBUNSUP($<fl>1, "Unsupported: ## range cycle delay range expression"); }
|
||||
| yP_POUNDPOUND '[' constExpr ':' constExpr ']'
|
||||
{ $$ = new AstDelay{$1, $3, true};
|
||||
$$->rhsp($5); }
|
||||
| yP_POUNDPOUND yP_BRASTAR ']'
|
||||
{ $$ = new AstDelay{$1, new AstConst{$1, AstConst::BitFalse{}}, true};
|
||||
BBUNSUP($<fl>1, "Unsupported: ## [*] cycle delay range expression"); }
|
||||
|
|
|
|||
|
|
@ -1,10 +1,7 @@
|
|||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:65:29: Unsupported: ## range cycle delay range expression
|
||||
65 | ($rose(a), l_b = b) |-> ##[3:10] q[l_b];
|
||||
| ^~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:51: Unsupported: [-> boolean abbrev expression
|
||||
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
| ^~~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_unsup.v:82:54: Unsupported: boolean abbrev (in sequence expression)
|
||||
82 | (count == 0, l_t = $realtime) ##1 (count == 7)[->1] |-> $realtime - l_t < 50.5;
|
||||
| ^
|
||||
|
|
|
|||
|
|
@ -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()
|
||||
|
|
@ -0,0 +1,88 @@
|
|||
// 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 [63:0] result = {61'h0, c, b, a};
|
||||
|
||||
always_ff @(posedge clk) begin
|
||||
`ifdef TEST_VERBOSE
|
||||
$write("[%0t] cyc==%0d crc=%x a=%b b=%b c=%b\n",
|
||||
$time, cyc, crc, a, b, c);
|
||||
`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'h38c614665c6b71ad);
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
end
|
||||
|
||||
// Basic ##[1:3] range delay (CRC-driven, always-true consequent)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> ##[1:3] 1'b1);
|
||||
|
||||
// ##[2:4] range delay
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
b |-> ##[2:4] 1'b1);
|
||||
|
||||
// Degenerate ##[2:2] (equivalent to ##2)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> ##[2:2] 1'b1);
|
||||
|
||||
// Multi-step: ##[1:2] then ##1 (both consequents always true)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> ##[1:2] 1'b1 ##1 1'b1);
|
||||
|
||||
// Large range ##[1:10000] (scalability, O(1) code size)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> ##[1:10000] 1'b1);
|
||||
|
||||
// Range with binary SExpr: nextStep has delay > 0 after range match
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> b ##[1:2] 1'b1 ##3 1'b1);
|
||||
|
||||
// Binary SExpr without implication (covers firstStep.exprp path without antecedent)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a ##[1:3] 1'b1);
|
||||
|
||||
// Implication with binary SExpr RHS (covers antExprp AND firstStep.exprp)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> b ##[1:2] 1'b1);
|
||||
|
||||
// Fixed delay before range (covers firstStep.delay path in IDLE)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
a |-> ##2 1'b1 ##[1:3] 1'b1);
|
||||
|
||||
// Unary range with no antecedent and no preExpr (covers unconditional start)
|
||||
assert property (@(posedge clk) disable iff (cyc < 2)
|
||||
##[1:3] 1'b1);
|
||||
|
||||
endmodule
|
||||
|
|
@ -0,0 +1,19 @@
|
|||
%Error: t/t_property_sexpr_range_delay_bad.v:18:45: Range delay bounds must be elaboration-time constants (IEEE 1800-2023 16.7)
|
||||
: ... note: In instance 't'
|
||||
18 | a1: assert property (@(posedge clk) a |-> ##[1:cyc] b);
|
||||
| ^~
|
||||
... See the manual at https://verilator.org/verilator_doc.html?v=latest for more assistance.
|
||||
%Error: t/t_property_sexpr_range_delay_bad.v:21:45: Range delay bounds must be non-negative (IEEE 1800-2023 16.7)
|
||||
: ... note: In instance 't'
|
||||
21 | a2: assert property (@(posedge clk) a |-> ##[-1:3] b);
|
||||
| ^~
|
||||
%Error: t/t_property_sexpr_range_delay_bad.v:24:45: Range delay maximum must be >= minimum (IEEE 1800-2023 16.7)
|
||||
: ... note: In instance 't'
|
||||
24 | a3: assert property (@(posedge clk) a |-> ##[5:2] b);
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_property_sexpr_range_delay_bad.v:27:45: Unsupported: ##0 in range delays
|
||||
: ... note: In instance 't'
|
||||
27 | a4: assert property (@(posedge clk) a |-> ##[0:3] b);
|
||||
| ^~
|
||||
... For error description see https://verilator.org/warn/UNSUPPORTED?v=latest
|
||||
%Error: Exiting due to
|
||||
|
|
@ -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')
|
||||
|
||||
test.lint(expect_filename=test.golden_filename,
|
||||
verilator_flags2=['--assert', '--timing', '--error-limit 1000'],
|
||||
fails=True)
|
||||
|
||||
test.passes()
|
||||
|
|
@ -0,0 +1,29 @@
|
|||
// 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;
|
||||
|
||||
logic clk = 0;
|
||||
always #5 clk = ~clk;
|
||||
|
||||
int cyc = 0;
|
||||
logic a, b;
|
||||
|
||||
always @(posedge clk) cyc <= cyc + 1;
|
||||
|
||||
// Non-constant bounds
|
||||
a1: assert property (@(posedge clk) a |-> ##[1:cyc] b);
|
||||
|
||||
// Negative bound
|
||||
a2: assert property (@(posedge clk) a |-> ##[-1:3] b);
|
||||
|
||||
// Max < min
|
||||
a3: assert property (@(posedge clk) a |-> ##[5:2] b);
|
||||
|
||||
// ##0 in range
|
||||
a4: assert property (@(posedge clk) a |-> ##[0:3] b);
|
||||
|
||||
endmodule
|
||||
|
|
@ -8,18 +8,12 @@
|
|||
%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:60:5: Unsupported: ## range cycle delay range expression
|
||||
60 | ## [1:2] b;
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:63:5: Unsupported: ## [*] cycle delay range expression
|
||||
63 | ## [*] b;
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:66:5: Unsupported: ## [+] cycle delay range expression
|
||||
66 | ## [+] b;
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:76:7: Unsupported: ## range cycle delay range expression
|
||||
76 | a ## [1:2] b;
|
||||
| ^~
|
||||
%Error-UNSUPPORTED: t/t_sequence_sexpr_unsup.v:79:7: Unsupported: ## [*] cycle delay range expression
|
||||
79 | a ## [*] b;
|
||||
| ^~
|
||||
|
|
|
|||
Loading…
Reference in New Issue