From c28119e51d4cf4d61e936c5e69f4999722567df4 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 12 Feb 2026 13:44:46 +0100 Subject: [PATCH 1/3] Fix enum variables in constraint solver producing invalid enum values MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit When enum variables (rand or randc) are referenced in user constraints, the constraint solver declares them as unconstrained bitvectors, which can produce values outside the valid enum range. Add implicit membership constraints to restrict solver output to valid enum members (IEEE 1800-2017 ยง18.4.2). Co-Authored-By: Claude Opus 4.6 --- src/V3Randomize.cpp | 35 ++++++++++++ test_regress/t/t_randc_enum_constraint.py | 21 +++++++ test_regress/t/t_randc_enum_constraint.v | 69 +++++++++++++++++++++++ 3 files changed, 125 insertions(+) create mode 100755 test_regress/t/t_randc_enum_constraint.py create mode 100644 test_regress/t/t_randc_enum_constraint.v diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index 83309b453..cacd0c803 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -3209,6 +3209,41 @@ 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). + { + AstNodeModule* const genModp = VN_AS(genp->user2p(), NodeModule); + nodep->foreachMember([&](AstClass*, AstVar* memberVarp) { + if (!memberVarp->user3()) return; // Not in solver path + 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)) { + const AstConst* const vconstp = VN_AS(itemp->valuep(), Const); + constraint += " (= " + smtName + " (_ bv" + + cvtToStr(vconstp->toUInt()) + " " + + cvtToStr(width) + "))"; + } + constraint += "))"; + AstCMethodHard* const callp = new AstCMethodHard{ + fl, + new AstVarRef{fl, genModp, genp, VAccess::READWRITE}, + VCMethod::RANDOMIZER_HARD, + new AstCExpr{fl, AstCExpr::Pure{}, + "\"" + constraint + "\""}}; + callp->dtypeSetVoid(); + randomizep->addStmtsp(callp->makeStmt()); + }); + } + AstTask* setupAllTaskp = getCreateConstraintSetupFunc(nodep); AstTaskRef* const setupTaskRefp = new AstTaskRef{fl, setupAllTaskp, nullptr}; randomizep->addStmtsp(setupTaskRefp->makeStmt()); diff --git a/test_regress/t/t_randc_enum_constraint.py b/test_regress/t/t_randc_enum_constraint.py new file mode 100755 index 000000000..e8c23441f --- /dev/null +++ b/test_regress/t/t_randc_enum_constraint.py @@ -0,0 +1,21 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# 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-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('simulator') + +if not test.have_solver: + test.skip("No constraint solver installed") + +test.compile() + +test.execute() + +test.passes() diff --git a/test_regress/t/t_randc_enum_constraint.v b/test_regress/t/t_randc_enum_constraint.v new file mode 100644 index 000000000..5f750931f --- /dev/null +++ b/test_regress/t/t_randc_enum_constraint.v @@ -0,0 +1,69 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +// Test that randc enum variables with user constraints only produce +// valid enum members (not arbitrary bitvector values). + +module t; + + typedef enum bit [2:0] { + RED = 0, + GREEN = 1, + BLUE = 2, + WHITE = 3, + BLACK = 4 + } color_t; + + class ColorClass; + randc color_t color; + constraint c_no_dark { color != BLACK; } + endclass + + // Test with all enum values allowed (no exclusion constraint) + class AllColorsClass; + randc color_t color; + constraint c_range { color <= WHITE; } + endclass + + initial begin + ColorClass c; + AllColorsClass ac; + int color_seen[5]; + + // Test 1: randc enum with exclusion constraint + // Values must be valid enum members (0-4) and not BLACK (4) + c = new; + repeat (40) begin + `checkd(c.randomize(), 1); + // Must be a valid enum member (not 5, 6, 7) + `checkd(c.color <= BLACK, 1); + // Must not be BLACK (excluded by constraint) + `checkd(c.color == BLACK, 0); + end + + // Test 2: randc enum with range constraint - verify all valid values seen + ac = new; + repeat (40) begin + `checkd(ac.randomize(), 1); + `checkd(ac.color <= WHITE, 1); + color_seen[ac.color] = 1; + end + // After 40 iterations (10 full cycles of 4), all values should appear + `checkd(color_seen[0], 1); + `checkd(color_seen[1], 1); + `checkd(color_seen[2], 1); + `checkd(color_seen[3], 1); + + $write("*-* All Finished *-*\n"); + $finish; + end + +endmodule From 7550f9ce39149d1fbf43b4ca37120168b7b2647b Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 12 Feb 2026 13:45:43 +0100 Subject: [PATCH 2/3] review and format --- src/V3Randomize.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/V3Randomize.cpp b/src/V3Randomize.cpp index cacd0c803..3d8a6cc5d 100644 --- a/src/V3Randomize.cpp +++ b/src/V3Randomize.cpp @@ -3218,8 +3218,8 @@ class RandomizeVisitor final : public VNVisitor { AstNodeModule* const genModp = VN_AS(genp->user2p(), NodeModule); nodep->foreachMember([&](AstClass*, AstVar* memberVarp) { if (!memberVarp->user3()) return; // Not in solver path - AstEnumDType* const enumDtp = VN_CAST( - memberVarp->dtypep()->skipRefToEnump(), EnumDType); + AstEnumDType* const enumDtp + = VN_CAST(memberVarp->dtypep()->skipRefToEnump(), EnumDType); if (!enumDtp) return; const int width = enumDtp->width(); const std::string smtName = memberVarp->name(); @@ -3228,17 +3228,14 @@ class RandomizeVisitor final : public VNVisitor { for (AstEnumItem* itemp = enumDtp->itemsp(); itemp; itemp = VN_AS(itemp->nextp(), EnumItem)) { const AstConst* const vconstp = VN_AS(itemp->valuep(), Const); - constraint += " (= " + smtName + " (_ bv" - + cvtToStr(vconstp->toUInt()) + " " - + cvtToStr(width) + "))"; + constraint += " (= " + smtName + " (_ bv" + cvtToStr(vconstp->toUInt()) + + " " + cvtToStr(width) + "))"; } constraint += "))"; AstCMethodHard* const callp = new AstCMethodHard{ - fl, - new AstVarRef{fl, genModp, genp, VAccess::READWRITE}, + fl, new AstVarRef{fl, genModp, genp, VAccess::READWRITE}, VCMethod::RANDOMIZER_HARD, - new AstCExpr{fl, AstCExpr::Pure{}, - "\"" + constraint + "\""}}; + new AstCExpr{fl, AstCExpr::Pure{}, "\"" + constraint + "\""}}; callp->dtypeSetVoid(); randomizep->addStmtsp(callp->makeStmt()); }); From a5e8e1df320be91a8f591a88754b8e2b08b9fed7 Mon Sep 17 00:00:00 2001 From: Yilou Wang Date: Thu, 12 Feb 2026 13:45:43 +0100 Subject: [PATCH 3/3] 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