luke/verilator
1
0
Fork 0
mirror of https://github.com/verilator/verilator.git synced 2026-08-30 01:38:21 +02:00
Code Issues Packages Projects Releases Wiki Activity

Fix shift width mismatch in constraint solver SMT emission (#5420) (#7265)

Browse Source
This commit is contained in:
Yilou Wang
2026-03-16 18:48:09 -04:00
committed by GitHub
parent bf792f1809
commit be0f4a507e
3 changed files with 162 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/V3Randomize.cpp
+19
View File
@@ -1600,6 +1600,25 @@ class ConstraintExprVisitor final : public VNVisitor {
void visit(AstPowSS* nodep) override { handlePow(nodep); }
void visit(AstPowSU* nodep) override { handlePow(nodep); }
void visit(AstPowUS* nodep) override { handlePow(nodep); }
// SMT-LIB2 shift operations (bvshl/bvlshr/bvashr) require both operands
// to have the same bitvector width. Zero-extend the RHS if narrower.
void handleShift(AstNodeBiop* nodep) {
if (editFormat(nodep)) return;
const int lhsWidth = nodep->lhsp()->width();
const int rhsWidth = nodep->rhsp()->width();
if (rhsWidth < lhsWidth) {
FileLine* const fl = nodep->fileline();
AstNodeExpr* const rhsp = nodep->rhsp()->unlinkFrBack();
const bool rhsDependent = rhsp->user1();
AstExtend* const extendp = new AstExtend{fl, rhsp, lhsWidth};
extendp->user1(rhsDependent);
nodep->rhsp(extendp);
}
editSMT(nodep, nodep->lhsp(), nodep->rhsp());
}
void visit(AstShiftL* nodep) override { handleShift(nodep); }
void visit(AstShiftR* nodep) override { handleShift(nodep); }
void visit(AstShiftRS* nodep) override { handleShift(nodep); }
void visit(AstNodeBiop* nodep) override {
if (editFormat(nodep)) return;
editSMT(nodep, nodep->lhsp(), nodep->rhsp());