mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-12 06:00:55 +00:00
Code Activity

Less verbose equiv assumes

Browse source 
both only print on the first step, and equiv_simple only prints if also verbose
This commit is contained in:
Krystine Sherwin 2025-08-06 15:21:10 +12:00
parent f9e8127e2b
commit b1eeb7de3d
No known key found for this signature in database
2 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

10
passes/equiv/equiv_induct.cc
View file

@ -79,10 +79,12 @@ struct EquivInductWorker
} }
if (set_assumes) { if (set_assumes) {
RTLIL::SigSpec assumes_a, assumes_en; if (step == 1) {
satgen.getAssumes(assumes_a, assumes_en, step); RTLIL::SigSpec assumes_a, assumes_en;
for (int i = 0; i < GetSize(assumes_a); i++) satgen.getAssumes(assumes_a, assumes_en, step);
log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); for (int i = 0; i < GetSize(assumes_a); i++)
log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]));
}
ez->assume(satgen.importAssumes(step)); ez->assume(satgen.importAssumes(step));
} }

10
passes/equiv/equiv_simple.cc
View file

@ -243,10 +243,12 @@ struct EquivSimpleWorker
} }
if (set_assumes) { if (set_assumes) {
RTLIL::SigSpec assumes_a, assumes_en; if (verbose && step == max_seq) {
satgen.getAssumes(assumes_a, assumes_en, step+1); RTLIL::SigSpec assumes_a, assumes_en;
for (int i = 0; i < GetSize(assumes_a); i++) satgen.getAssumes(assumes_a, assumes_en, step+1);
log("Import constraint from assume cell: %s when %s.\n", log_signal(assumes_a[i]), log_signal(assumes_en[i])); for (int i = 0; i < GetSize(assumes_a); i++)
log(" Import constraint from assume cell: %s when %s (%d).\n", log_signal(assumes_a[i]), log_signal(assumes_en[i]), step);
}
ez->assume(satgen.importAssumes(step+1)); ez->assume(satgen.importAssumes(step+1));
} }