From a5e8e1df320be91a8f591a88754b8e2b08b9fed7 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 12 Feb 2026 13:45:43 +0100 Subject: [PATCH] Support randc enum variables with user constraints in solver When randc enum variables have user constraints, they go through the SMT solver path which treats them as unconstrained bitvectors. This adds implicit enum membership constraints so the solver only produces valid enum member values. Co-Authored-By: Claude Opus 4.6 --- src/V3Randomize.cpp | 8 ++------ test_regress/t/t_randc_enum_constraint.py | 2 +- 2 files changed, 3 insertions(+), 7 deletions(-) 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