diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 3d8a6cc5d..26f7d4f0f 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -3210,20 +3210,16 @@ class RandomizeVisitor final : public VNVisitor { } randomizep->addStmtsp(implementConstraintsClear(fl, genp)); - // Add implicit enum membership constraints for enum variables in the - // solver path. Without this, the solver treats enum variables as - // unconstrained bitvectors and may produce values outside the valid - // enum range (IEEE 1800-2017 18.4.2). + // Restrict enum variables in solver to valid members only { AstNodeModule* const genModp = VN_AS(genp->user2p(), NodeModule); nodep->foreachMember([&](AstClass*, AstVar* memberVarp) { - if (!memberVarp->user3()) return; // Not in solver path + if (!memberVarp->user3()) return; AstEnumDType* const enumDtp = VN_CAST(memberVarp->dtypep()->skipRefToEnump(), EnumDType); if (!enumDtp) return; const int width = enumDtp->width(); const std::string smtName = memberVarp->name(); - // Build: (__Vbv (or (= name (_ bvV W)) ...)) std::string constraint = "(__Vbv (or"; for (AstEnumItem* itemp = enumDtp->itemsp(); itemp; itemp = VN_AS(itemp->nextp(), EnumItem)) { diff --git a/test_regress/t/t_randc_enum_constraint.py b/test_regress/t/t_randc_enum_constraint.py index e8c23441f..db1adb3f9 100755 --- a/test_regress/t/t_randc_enum_constraint.py +++ b/test_regress/t/t_randc_enum_constraint.py @@ -4,7 +4,7 @@ # This program is free software; you can redistribute it and/or modify it # under the terms of either the GNU Lesser General Public License Version 3 # or the Perl Artistic License Version 2.0. -# SPDX-FileCopyrightText: 2026 PlanV GmbH +# SPDX-FileCopyrightText: 2026 Wilson Snyder # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 import vltest_bootstrap