Fix range delays with parameter bounds (#7882)

Signed-off-by: Artur Bieniek <abieniek@antmicro.com>
This commit is contained in:
Artur Bieniek 2026-07-06 19:13:11 +02:00 committed by GitHub
parent 8ed0acf1ec
commit a5f4d40901
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 20 additions and 2 deletions

View File

@ -472,8 +472,8 @@ class SvaNfaBuilder final {
AstVar* tryHoistSampled(AstNodeExpr* exprp, FileLine* flp, int cloneCount) {
constexpr int kHoistThreshold = 2;
if (cloneCount < kHoistThreshold) return nullptr;
AstVar* const tempVarp = new AstVar{flp, VVarType::MODULETEMP, m_propTempNames.get(exprp),
m_modp->findBitDType()};
AstVar* const tempVarp
= new AstVar{flp, VVarType::MODULETEMP, m_propTempNames.get(exprp), exprp->dtypep()};
m_modp->addStmtsp(tempVarp);
AstAssign* const assignp = new AstAssign{flp, new AstVarRef{flp, tempVarp, VAccess::WRITE},
sampled(exprp->cloneTreePure(false))};

View File

@ -731,6 +731,17 @@ class WidthVisitor final : public VNVisitor {
iterateCheckBool(nodep, "default disable iff condition", nodep->condp(), BOTH);
}
void visit(AstDelay* nodep) override {
if (nodep->isCycleDelay() && m_underSExpr) {
// Fold parameterized SVA cycle-delay bounds
userIterateAndNext(nodep->lhsp(), WidthVP{SELF, BOTH}.p());
V3Const::constifyParamsNoWarnEdit(nodep->lhsp());
if (nodep->rhsp() && !nodep->isUnbounded()) {
// Fold parametrized SVA cycle-delay max bound
userIterateAndNext(nodep->rhsp(), WidthVP{SELF, BOTH}.p());
V3Const::constifyParamsNoWarnEdit(nodep->rhsp());
}
return;
}
if (AstNodeExpr* const fallDelayp = nodep->fallDelay()) {
iterateCheckDelay(nodep, "delay", nodep->lhsp(), BOTH);
iterateCheckDelay(nodep, "delay", fallDelayp, BOTH);

View File

@ -13,6 +13,8 @@
module t (
input clk
);
parameter P = 1;
integer cyc = 0;
reg [63:0] crc = '0;
reg [63:0] sum = '0;
@ -64,6 +66,11 @@ module t (
assert property (@(posedge clk) disable iff (cyc < 2)
a |-> ##[1:3] (a | b | c | d | e));
// Parameterized range bound
assert property (@(posedge clk) disable iff (cyc < 2)
a |-> ##[P:P+3] (a | b | c | d | e));
assert property (@(posedge clk) ##[P:P+3] 1);
// ##[2:4] range delay
assert property (@(posedge clk) disable iff (cyc < 2)
b |-> ##[2:4] (a | b | c | d | e));