Fix bare variable constraint: wrap expr != 0 per IEEE 18.5.1

This commit is contained in:
Yilou Wang 2026-03-03 09:45:49 +01:00
parent 79464b72bc
commit a08c67685d
1 changed files with 14 additions and 0 deletions

View File

@ -1900,6 +1900,20 @@ class ConstraintExprVisitor final : public VNVisitor {
}
void visit(AstConstraintExpr* nodep) override {
// IEEE 1800-2017 18.5.1: A bare expression used as a constraint is
// implicitly treated as "expr != 0" when wider than 1 bit.
// Must wrap before iterateChildren, which converts to SMT format.
{
AstNodeExpr* const exprp = nodep->exprp();
if (exprp->width() > 1) {
FileLine* const fl = exprp->fileline();
V3Number numZero{fl, exprp->width(), 0};
AstNodeExpr* const neqp
= new AstNeq{fl, exprp->unlinkFrBack(), new AstConst{fl, numZero}};
neqp->user1(true); // Mark as rand-dependent for SMT path
nodep->exprp(neqp);
}
}
iterateChildren(nodep);
if (m_wantSingle) {
nodep->replaceWith(nodep->exprp()->unlinkFrBack());