luke
/
verilator
mirror of https://github.com/verilator/verilator.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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 <noreply@anthropic.com>
This commit is contained in:
Yilou Wang 2026-02-12 13:45:43 +01:00
parent 7550f9ce39
commit a5e8e1df32
2 changed files with 3 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/V3Randomize.cpp
View File

@ -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)) {

2
test_regress/t/t_randc_enum_constraint.py
View File

@ -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