Width inside range bounds in the InsideRange visitor per review
This commit is contained in:
parent
cc0d06c87b
commit
0e055fd334
|
|
@ -3431,14 +3431,8 @@ class WidthVisitor final : public VNVisitor {
|
|||
for (AstNode *nextip, *itemp = nodep->itemsp(); itemp; itemp = nextip) {
|
||||
nextip = itemp->nextp();
|
||||
itemp = VN_AS(itemp, DistItem)->rangep();
|
||||
if (AstInsideRange* const rangep = VN_CAST(itemp, InsideRange)) {
|
||||
// Finalize both bounds now: the in-constraint path keeps the dist
|
||||
// (and its ranges) for constraint lowering, which cannot re-width
|
||||
// a mixed-width bound expression
|
||||
iterateCheck(nodep, "Dist Range", rangep->lhsp(), CONTEXT_DET, FINAL, subDTypep,
|
||||
EXTEND_EXP);
|
||||
iterateCheck(nodep, "Dist Range", rangep->rhsp(), CONTEXT_DET, FINAL, subDTypep,
|
||||
EXTEND_EXP);
|
||||
if (VN_IS(itemp, InsideRange)) {
|
||||
userIterate(itemp, WidthVP{subDTypep, FINAL}.p());
|
||||
} else {
|
||||
iterateCheck(nodep, "Dist Item", itemp, CONTEXT_DET, FINAL, subDTypep, EXTEND_EXP);
|
||||
}
|
||||
|
|
@ -3479,8 +3473,6 @@ class WidthVisitor final : public VNVisitor {
|
|||
UINFOTREE(9, nodep, "", "dist-out");
|
||||
nodep->replaceWith(newp);
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
// Width the replacement (same reason as in visit(AstInside) below)
|
||||
userIterate(newp, m_vup);
|
||||
}
|
||||
|
||||
void visit(AstInside* nodep) override {
|
||||
|
|
@ -3518,10 +3510,12 @@ class WidthVisitor final : public VNVisitor {
|
|||
EXTEND_EXP);
|
||||
for (AstNode *nextip, *itemp = nodep->itemsp(); itemp; itemp = nextip) {
|
||||
nextip = itemp->nextp(); // iterate may cause the node to get replaced
|
||||
// InsideRange will get replaced with Lte&Gte and finalized later
|
||||
if (!VN_IS(itemp, InsideRange) && !itemp->dtypep()->isNonPackedArray())
|
||||
if (VN_IS(itemp, InsideRange)) {
|
||||
userIterate(itemp, WidthVP{expDTypep, FINAL}.p());
|
||||
} else if (!itemp->dtypep()->isNonPackedArray()) {
|
||||
iterateCheck(nodep, "Inside Item", itemp, CONTEXT_DET, FINAL, expDTypep,
|
||||
EXTEND_EXP);
|
||||
}
|
||||
}
|
||||
|
||||
AstNodeExpr* exprp;
|
||||
|
|
@ -3576,10 +3570,6 @@ class WidthVisitor final : public VNVisitor {
|
|||
UINFOTREE(9, newp, "", "inside-out");
|
||||
nodep->replaceWith(newp);
|
||||
VL_DO_DANGLING(pushDeletep(nodep), nodep);
|
||||
// Width the replacement: InsideRange bounds are skipped above (finalized
|
||||
// "later"), and a single-BOTH context (e.g. the RHS of '->' via
|
||||
// iterateCheckBool) never revisits it, leaving mixed-width bounds unextended.
|
||||
userIterate(newp, m_vup);
|
||||
}
|
||||
AstNodeExpr* insideItem(AstNode* nodep, AstNodeExpr* exprp, AstNodeExpr* itemp) {
|
||||
const AstNodeDType* const itemDtp = itemp->dtypep()->skipRefp();
|
||||
|
|
@ -3617,8 +3607,25 @@ class WidthVisitor final : public VNVisitor {
|
|||
V3Const::constifyEdit(nodep->lhsp()); // lhsp may change
|
||||
V3Const::constifyEdit(nodep->rhsp()); // rhsp may change
|
||||
} else {
|
||||
userIterateAndNext(nodep->lhsp(), m_vup);
|
||||
userIterateAndNext(nodep->rhsp(), m_vup);
|
||||
if (m_vup->prelim()) {
|
||||
userIterateAndNext(nodep->lhsp(), m_vup);
|
||||
userIterateAndNext(nodep->rhsp(), m_vup);
|
||||
}
|
||||
if (m_vup->final()) {
|
||||
AstNodeDType* const expDTypep = m_vup->dtypeOverridep(nodep->dtypep());
|
||||
// Warning waivers match visit_cmp_eq_gt on the lowered Gte/Lte
|
||||
const int expWidth = expDTypep->width();
|
||||
const bool waiveLhs = expWidth == 32
|
||||
&& !(expDTypep->isSigned() && nodep->lhsp()->isSigned())
|
||||
&& expDTypep->widthMin() >= nodep->lhsp()->width();
|
||||
const bool waiveRhs = expWidth == 32
|
||||
&& !(expDTypep->isSigned() && nodep->rhsp()->isSigned())
|
||||
&& expWidth >= nodep->rhsp()->widthMin();
|
||||
iterateCheck(nodep, "Range LHS", nodep->lhsp(), CONTEXT_DET, FINAL, expDTypep,
|
||||
EXTEND_EXP, !waiveLhs);
|
||||
iterateCheck(nodep, "Range RHS", nodep->rhsp(), CONTEXT_DET, FINAL, expDTypep,
|
||||
EXTEND_EXP, !waiveRhs);
|
||||
}
|
||||
}
|
||||
nodep->dtypeFrom(nodep->lhsp());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -14,8 +14,7 @@ test.scenarios('simulator')
|
|||
if not test.have_solver:
|
||||
test.skip("No constraint solver installed")
|
||||
|
||||
# The mixed-width range bound (64-bit minus 32-bit) is intentional.
|
||||
test.compile(verilator_flags2=["-Wno-WIDTHEXPAND"])
|
||||
test.compile()
|
||||
|
||||
test.execute()
|
||||
|
||||
|
|
|
|||
|
|
@ -9,33 +9,32 @@
|
|||
`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0);
|
||||
// verilog_format: on
|
||||
|
||||
// Mixed-width inside-range bound under an implication (and other single-BOTH
|
||||
// contexts) must be zero-extended in the emitted SMT.
|
||||
// verilator lint_off WIDTHEXPAND
|
||||
class Impl;
|
||||
rand bit [63:0] x, y;
|
||||
rand bit [31:0] g;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
y != 0 -> x inside {[y - g : y]};
|
||||
}
|
||||
endclass
|
||||
|
||||
class Neg; // inside under logical-not under implication
|
||||
class Neg; // inside under logical-not
|
||||
rand bit [63:0] x, y;
|
||||
rand bit [31:0] g;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
y != 0 -> !(x inside {[y - g : y - 1]});
|
||||
}
|
||||
endclass
|
||||
|
||||
class LAnd; // inside as a logical-and operand (no implication)
|
||||
class LAnd; // inside as a logical-and operand
|
||||
rand bit [63:0] x, y;
|
||||
rand bit [31:0] g;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
(x inside {[y - g : y]}) && (x[0] == 1'b0);
|
||||
}
|
||||
|
|
@ -46,7 +45,7 @@ class Nest; // nested implication a -> (b -> inside)
|
|||
rand bit [31:0] g;
|
||||
rand bit a, b;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
a == 1;
|
||||
b == 1;
|
||||
|
|
@ -59,28 +58,41 @@ class CondCtx; // inside as a ?: condition
|
|||
rand bit [31:0] g;
|
||||
rand bit s;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
(x inside {[y - g : y]}) ? (s == 1'b1) : (s == 1'b0);
|
||||
}
|
||||
endclass
|
||||
|
||||
class Ctl; // all-32-bit control: no extension needed anywhere
|
||||
class Ctl; // all-32-bit control
|
||||
rand bit [31:0] x, y, g;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 32'h100;
|
||||
y != 0 -> x inside {[y - g : y]};
|
||||
}
|
||||
endclass
|
||||
|
||||
class DistRange; // mixed-width dist range bound (kept for constraint lowering)
|
||||
class DistRange; // mixed-width dist range bound
|
||||
rand bit [63:0] x, y;
|
||||
rand bit [31:0] g;
|
||||
constraint c {
|
||||
g inside {[1:10]};
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
x dist {[y - g : y] := 1, 5 := 1};
|
||||
x dist {
|
||||
[y - g : y] := 1,
|
||||
5 := 1
|
||||
};
|
||||
}
|
||||
endclass
|
||||
|
||||
class Bare; // bare narrow variable as a bound
|
||||
rand bit [63:0] x, y;
|
||||
rand bit [31:0] g;
|
||||
constraint c {
|
||||
g inside {[1 : 10]};
|
||||
y == 64'h100;
|
||||
y != 0 -> x inside {[g : y]};
|
||||
}
|
||||
endclass
|
||||
|
||||
|
|
@ -92,6 +104,7 @@ module t;
|
|||
CondCtx cx;
|
||||
Ctl ct;
|
||||
DistRange dr;
|
||||
Bare br;
|
||||
int ok;
|
||||
initial begin
|
||||
im = new;
|
||||
|
|
@ -101,6 +114,7 @@ module t;
|
|||
cx = new;
|
||||
ct = new;
|
||||
dr = new;
|
||||
br = new;
|
||||
for (int i = 0; i < 20; ++i) begin
|
||||
ok = im.randomize();
|
||||
`checkd(ok, 1);
|
||||
|
|
@ -129,8 +143,13 @@ module t;
|
|||
ok = dr.randomize();
|
||||
`checkd(ok, 1);
|
||||
if (dr.x != 5 && (dr.x < (64'h100 - dr.g) || dr.x > 64'h100)) `checkd(0, 1);
|
||||
|
||||
ok = br.randomize();
|
||||
`checkd(ok, 1);
|
||||
if (br.x < {32'h0, br.g} || br.x > 64'h100) `checkd(0, 1);
|
||||
end
|
||||
$write("*-* All Finished *-*\n");
|
||||
$finish;
|
||||
end
|
||||
endmodule
|
||||
// verilator lint_on WIDTHEXPAND
|
||||
|
|
|
|||
Loading…
Reference in New Issue