Support reduction XOR/AND operations in constraints (#7753)

This commit is contained in:
Kornel Uriasz
2026-06-11 09:43:18 -04:00
committed by GitHub
parent c6caa94fe0
commit 4c92c035e7
4 changed files with 180 additions and 0 deletions
+35
View File
@@ -1509,6 +1509,41 @@ class ConstraintExprVisitor final : public VNVisitor {
VL_DO_DANGLING(nodep->deleteTree(), nodep);
iterate(sump);
}
void visit(AstRedXor* nodep) override {
if (editFormat(nodep)) return;
// Build popcount expansion: (extract x 1 1) ^ (extract x 2 2) ^ ...
FileLine* const fl = nodep->fileline();
AstNodeExpr* const argp = nodep->lhsp()->unlinkFrBack();
AstNodeExpr* redxorp = new AstSel{fl, argp, 0, 1};
redxorp->user1(true);
for (int i = 1; i < argp->width(); i++) {
AstSel* const selp = new AstSel{fl, argp->cloneTreePure(false), i, 1};
selp->user1(true);
redxorp = new AstXor{fl, redxorp, selp};
redxorp->user1(true);
}
nodep->replaceWith(redxorp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
iterate(redxorp);
}
void visit(AstRedAnd* nodep) override {
if (editFormat(nodep)) return;
// Convert to (~x == 0)
FileLine* const fl = nodep->fileline();
AstNodeExpr* const argp = nodep->lhsp()->unlinkFrBack();
const V3Number numZero{fl, argp->width(), 0};
AstNodeExpr* const negp = new AstNot{fl, argp};
negp->user1(true);
AstNodeExpr* const eqp = new AstEq{fl, negp, new AstConst{fl, numZero}};
eqp->user1(true);
nodep->replaceWith(eqp);
VL_DO_DANGLING(nodep->deleteTree(), nodep);
iterate(eqp);
}
void visit(AstRedOr* nodep) override {
if (editFormat(nodep)) return;
// Convert to (x != 0)