Fix randc cycling in a class that also uses solve...before (Part1 of #7991) (#8055)

This commit is contained in:
Yilou Wang 2026-08-14 13:16:44 +02:00 committed by GitHub
parent 7da43d8302
commit abf199cf0e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 189 additions and 2 deletions

View File

@ -1000,6 +1000,10 @@ bool VlRandomizer::nextPhased(VlRNG& rngr, const std::vector<std::string>& uniqu
// One layer: all solve_before vars are independent, no ordering required
if (layers.size() <= 1) return nextFlat(rngr, uniqueExprs);
if (solvePhases(rngr, layers, uniqueExprs)) return true;
// Retry once with the randc cycle cleared, as nextFlat does
if (m_randcUsedValues.empty()) return false;
m_randcUsedValues.clear();
return solvePhases(rngr, layers, uniqueExprs);
}
@ -1037,13 +1041,12 @@ bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector<std::vector<std::s
// Final phase: use parseSolution to write ALL values to memory
const bool sat = parseSolution(os);
if (!sat) {
if (!m_randcVarNames.empty()) m_randcUsedValues.clear();
os << "(reset)\n";
return false;
}
solveDiversityXor(rngr, os);
// Record solved randc values for future exclusion
recordRandcValues();
solveDiversityXor(rngr, os);
os << "(reset)\n";
} else {
if (!checkSat(os)) {

View File

@ -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 Wilson Snyder
# 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()

View File

@ -0,0 +1,163 @@
// 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
// randc values excluded by the value of another rand variable: c cannot be 3
class Phased;
randc bit [1:0] c;
rand bit [1:0] x;
rand bit [3:0] y;
constraint order_c {solve x before y;}
constraint rel_c {y > {2'b00, x};}
constraint link_c {c < x;}
endclass
// Three dependency layers, so exhaustion lands two phases before the last
class Layered;
randc bit [1:0] c;
rand bit [3:0] a;
rand bit [3:0] b;
rand bit [3:0] d;
constraint order_ab {solve a before b;}
constraint order_bd {solve b before d;}
constraint rel_c {
b > a;
d > b;
}
endclass
// Constraint on the randc variable alone, so the permutation itself holds three values
class Limited;
randc bit [1:0] c;
rand bit [3:0] x;
rand bit [3:0] y;
constraint order_c {solve x before y;}
constraint rel_c {y > x;}
constraint lim_c {c != 2'd3;}
endclass
// randc tied to a solve-before variable, so x cycles only if the exclusions reach phase one
class Ordered;
randc bit [1:0] c;
rand bit [1:0] x;
rand bit [1:0] y;
constraint order_c {solve x before y;}
constraint tie_c {x == c;}
constraint rel_c {y == ~x;}
endclass
// Unsatisfiable before any randc value is recorded
class Unsat;
randc bit [1:0] c;
rand bit [3:0] x;
rand bit [3:0] y;
constraint order_c {solve x before y;}
constraint rel_c {y > x;}
endclass
module t;
Phased p;
Layered q;
Limited r;
Ordered o;
Unsat u;
bit [3:0] seen;
int pcount[4];
int qcount[4];
int rcount[4];
int ocount[4];
int ok;
int psolved;
initial begin
// c == 3 satisfies no x
p = new;
seen = 4'b0;
psolved = 0;
for (int i = 0; i < 12 && psolved < 9; ++i) begin
if (p.randomize() == 1) begin
`checkd(p.y > {2'b00, p.x}, 1'b1);
`checkd(p.c < p.x, 1'b1);
seen[p.c] = 1'b1;
++pcount[p.c];
++psolved;
if (psolved % 3 == 0) begin
`checkd(seen, 4'b0111); // Three draws covered three values, so none repeated
seen = 4'b0;
end
end
end
`checkd(psolved, 9); // Three cycles of three solvable values
for (int v = 0; v < 3; ++v) `checkd(pcount[v], 3);
`checkd(pcount[3], 0); // zero-ok: c == 3 satisfies no x
q = new;
seen = 4'b0;
for (int i = 0; i < 8; ++i) begin
ok = q.randomize();
`checkd(ok, 1);
`checkd(q.b > q.a, 1'b1);
`checkd(q.d > q.b, 1'b1);
seen[q.c] = 1'b1;
++qcount[q.c];
if (i % 4 == 3) begin
`checkd(seen, 4'b1111);
seen = 4'b0;
end
end
for (int v = 0; v < 4; ++v) `checkd(qcount[v], 2);
r = new;
seen = 4'b0;
for (int i = 0; i < 6; ++i) begin
ok = r.randomize();
`checkd(ok, 1);
`checkd(r.y > r.x, 1'b1);
seen[r.c] = 1'b1;
++rcount[r.c];
if (i % 3 == 2) begin
`checkd(seen, 4'b0111);
seen = 4'b0;
end
end
for (int v = 0; v < 3; ++v) `checkd(rcount[v], 2);
`checkd(rcount[3], 0); // zero-ok: excluded by lim_c
o = new;
seen = 4'b0;
for (int i = 0; i < 8; ++i) begin
ok = o.randomize();
`checkd(ok, 1);
`checkd(o.x, o.c);
`checkd(o.y, ~o.x);
seen[o.x] = 1'b1;
++ocount[o.x];
if (i % 4 == 3) begin
`checkd(seen, 4'b1111);
seen = 4'b0;
end
end
for (int v = 0; v < 4; ++v) `checkd(ocount[v], 2);
// Fails with an empty cycle, then the object still randomizes
u = new;
ok = u.randomize() with {
x > 14;
y > x;
};
`checkd(ok, 0); // zero-ok: constraints are unsatisfiable
ok = u.randomize();
`checkd(ok, 1);
`checkd(u.y > u.x, 1'b1);
$write("*-* All Finished *-*\n");
$finish;
end
endmodule