mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-15 03:35:40 +00:00
Code Activity

Fix flaky opt_priokey -strict and cover binary exclusive scan

Browse source 
ASLR-dependent ConstEval seeding let E4 miss OOR counterexamples; use a
deterministic seed and force OOR key collisions. Add I9 (NB=12) for the
thermometer fallback path Greptile flagged.

Co-authored-by: Cursor <cursoragent@cursor.com>
This commit is contained in:
Akash Levy 2026-07-08 23:20:22 -07:00
parent 665bd1099a
commit a022ca524d
2 changed files with 78 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

51
passes/opt/opt_priokey.cc
View file

@ -264,26 +264,21 @@ struct OptPrioKeyWorker {
range = 1ULL << cap;
}
ConstEval ce(module);
uint64_t lfsr = 0x9e3779b97f4a7c15ULL ^ (uintptr_t)read;
// Deterministic seed (not a Cell*): ASLR made uintptr_t seeding flake
// across runs, so -strict could miss the OOR counterexample.
uint64_t lfsr = 0x9e3779b97f4a7c15ULL ^ ((uint64_t)S << 1) ^
((uint64_t)kw << 17) ^ (uint64_t)GetSize(steps);
auto rnd = [&]() {
lfsr ^= lfsr << 13; lfsr ^= lfsr >> 7; lfsr ^= lfsr << 17;
return lfsr;
};
for (int t = 0; t < fp_trials; t++) {
auto trial = [&](int rk, const vector<int> &kv, const vector<int> &gv) -> bool {
ce.push();
int rk = (int)(rnd() % range);
ce.set(read_key, Const(rk, GetSize(read_key)));
vector<int> kv(GetSize(steps));
vector<int> gv(GetSize(steps));
for (int i = 0; i < GetSize(steps); i++) {
kv[i] = (int)(rnd() % range);
ce.set(steps[i].key, Const(kv[i], GetSize(steps[i].key)));
if (steps[i].guard == State::S1) {
gv[i] = 1;
} else {
gv[i] = (int)(rnd() & 1);
if (steps[i].guard != State::S1)
ce.set(SigSpec(steps[i].guard), Const(gv[i], 1));
}
}
SigSpec out(read->getPort(ID::Y));
SigSpec undef;
@ -293,7 +288,39 @@ struct OptPrioKeyWorker {
for (int i = 0; i < GetSize(steps); i++)
if (gv[i] && kv[i] == rk) { expect = 1; break; }
ce.pop();
if (!ok || actual != expect)
return ok && actual == expect;
};
// Strict + non-pow2 S: force OOR key collisions the rewrite would accept
// but the S-bit accumulator cannot store (taken[key>=S] is not a set bit).
if (strict && range > (uint64_t)S && !steps.empty()) {
int oor_n = (int)(range - (uint64_t)S);
int forced = oor_n < 16 ? oor_n : 16;
for (int f = 0; f < forced; f++) {
int rk = S + f;
vector<int> kv(GetSize(steps), 0);
vector<int> gv(GetSize(steps), 0);
kv[0] = rk;
gv[0] = 1;
for (int i = 1; i < GetSize(steps); i++) {
kv[i] = (int)(rnd() % range);
gv[i] = steps[i].guard == State::S1 ? 1 : (int)(rnd() & 1);
}
if (!trial(rk, kv, gv))
return false;
}
}
for (int t = 0; t < fp_trials; t++) {
int rk = (int)(rnd() % range);
vector<int> kv(GetSize(steps));
vector<int> gv(GetSize(steps));
for (int i = 0; i < GetSize(steps); i++) {
kv[i] = (int)(rnd() % range);
if (steps[i].guard == State::S1)
gv[i] = 1;
else
gv[i] = (int)(rnd() & 1);
}
if (!trial(rk, kv, gv))
return false;
}
return true;

39
tests/opt/opt_first_fit_alloc.ys
View file

@ -1171,3 +1171,42 @@ design -load postopt
select -assert-min 1 w:*ffa_*
design -reset
log -pop
# I9: exclusive with NB > max_therm_nb (8) — forces the binary saturating
# Hillis–Steele fallback (emit_scan_exclusive_bin / emit_sat_add) instead of
# the thermometer scan used by I1–I8.
log -header "I9: exclusive binary-scan fallback N=16 NB=12 (equiv)"
log -push
design -reset
read_verilog -sv <<EOF
module top #(parameter N=16, NB=12, W=4) (
input logic mode,
input logic [N-1:0] req,
output logic [N*W-1:0] dsel_flat
);
logic [N-1:0] en = req & {N{mode}};
logic [W-1:0] dsel [0:N-1];
logic [NB-1:0] taken;
logic [N-1:0] done;
always_comb begin
for (int i=0;i<N;i++) dsel[i] = '0;
taken = '0; done = '0;
for (int i=0;i<N;i++)
if (en[i])
for (int j=0;j<NB;j++)
if (!taken[j] && !done[i]) begin
dsel[i] = W'(j); done[i] = 1'b1; taken[j] = 1'b1;
end
end
for (genvar g=0;g<N;g++) assign dsel_flat[g*W +: W] = dsel[g];
endmodule
EOF
hierarchy -top top
proc
opt
check -assert
equiv_opt -assert opt_first_fit_alloc
design -load postopt
select -assert-min 1 w:*ffa_*
design -reset
log -pop