mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-02-14 21:01:50 +00:00
Code Activity

equiv_simple, equiv_induct: refactor

Browse source
This commit is contained in:
Emil J. Tywoniak 2026-02-03 17:54:46 +01:00
parent 6dbe03f0f5
commit 000be270ca
3 changed files with 136 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

73
passes/equiv/equiv.h Normal file
View file

@ -0,0 +1,73 @@
#ifndef EQUIV_H
#define EQUIV_H
#include "kernel/log.h"
#include "kernel/yosys_common.h"
#include "kernel/sigtools.h"
#include "kernel/satgen.h"
YOSYS_NAMESPACE_BEGIN
static void report_missing_model(bool warn_only, RTLIL::Cell* cell)
{
std::string s;
if (cell->is_builtin_ff())
s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
else
s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
if (warn_only) {
log_formatted_warning_noprefix(s);
} else {
log_formatted_error(s);
}
}
struct EquivWorker {
RTLIL::Module *module;
ezSatPtr ez;
SatGen satgen;
struct Config {
bool model_undef = false;
int max_seq = 1;
bool set_assumes = false;
bool parse(const std::vector<std::string>& args, size_t& idx) {
if (args[idx] == "-undef") {
model_undef = true;
return true;
}
if (args[idx] == "-seq" && idx+1 < args.size()) {
max_seq = atoi(args[++idx].c_str());
return true;
}
if (args[idx] == "-set-assumes") {
set_assumes = true;
return true;
}
return false;
}
static std::string help(const char* default_seq) {
return stringf(
" -undef\n"
" enable modelling of undef states\n"
"\n"
" -seq <N>\n"
" the max. number of time steps to be considered (default = %s)\n"
"\n"
" -set-assumes\n"
" set all assumptions provided via $assume cells\n"
, default_seq);
}
};
Config cfg;
EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) {
satgen.model_undef = cfg.model_undef;
}
};
YOSYS_NAMESPACE_END
#endif // EQUIV_H

66
passes/equiv/equiv_induct.cc
View file

@ -18,49 +18,34 @@
*/
#include "kernel/yosys.h"
#include "kernel/satgen.h"
#include "kernel/sigtools.h"
#include "passes/equiv/equiv.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct EquivInductWorker
struct EquivInductWorker : public EquivWorker
{
Module *module;
SigMap sigmap;
vector<Cell*> cells;
pool<Cell*> workset;
ezSatPtr ez;
SatGen satgen;
int max_seq;
int success_counter;
bool set_assumes;
dict<int, int> ez_step_is_consistent;
pool<Cell*> cell_warn_cache;
SigPool undriven_signals;
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module),
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, Config cfg) : EquivWorker(module, &sigmap, cfg), sigmap(module),
cells(module->selected_cells()), workset(unproven_equiv_cells),
satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes)
{
satgen.model_undef = model_undef;
}
success_counter(0) {}
void create_timestep(int step)
{
vector<int> ez_equal_terms;
for (auto cell : cells) {
if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) {
if (cell->is_builtin_ff())
log_warning("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
else
log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
cell_warn_cache.insert(cell);
if (!satgen.importCell(cell, step)) {
report_missing_model(true, cell);
}
if (cell->type == ID($equiv)) {
SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit();
@ -78,7 +63,7 @@ struct EquivInductWorker
}
}
if (set_assumes) {
if (cfg.set_assumes) {
if (step == 1) {
RTLIL::SigSpec assumes_a, assumes_en;
satgen.getAssumes(assumes_a, assumes_en, step);
@ -123,7 +108,7 @@ struct EquivInductWorker
GetSize(satgen.initial_state), GetSize(undriven_signals));
}
for (int step = 1; step <= max_seq; step++)
for (int step = 1; step <= cfg.max_seq; step++)
{
ez->assume(ez_step_is_consistent[step]);
@ -146,7 +131,7 @@ struct EquivInductWorker
return;
}
log(" Proof for induction step failed. %s\n", step != max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset.");
log(" Proof for induction step failed. %s\n", step != cfg.max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset.");
}
workset.sort();
@ -158,12 +143,12 @@ struct EquivInductWorker
log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort(ID::Y))));
int ez_a = satgen.importSigBit(bit_a, max_seq+1);
int ez_b = satgen.importSigBit(bit_b, max_seq+1);
int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1);
int ez_b = satgen.importSigBit(bit_b, cfg.max_seq+1);
int cond = ez->XOR(ez_a, ez_b);
if (satgen.model_undef)
cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1)));
cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, cfg.max_seq+1)));
if (!ez->solve(cond)) {
log(" success!\n");
@ -189,14 +174,7 @@ struct EquivInductPass : public Pass {
log("Only selected $equiv cells are proven and only selected cells are used to\n");
log("perform the proof.\n");
log("\n");
log(" -undef\n");
log(" enable modelling of undef states\n");
log("\n");
log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 4)\n");
log("\n");
log(" -set-assumes\n");
log(" set all assumptions provided via $assume cells\n");
EquivWorker::Config::help("4");
log("\n");
log("This command is very effective in proving complex sequential circuits, when\n");
log("the internal state of the circuit quickly propagates to $equiv cells.\n");
@ -214,25 +192,15 @@ struct EquivInductPass : public Pass {
void execute(std::vector<std::string> args, Design *design) override
{
int success_counter = 0;
bool model_undef = false, set_assumes = false;
int max_seq = 4;
EquivWorker::Config cfg;
cfg.max_seq = 4;
log_header(design, "Executing EQUIV_INDUCT pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-undef") {
model_undef = true;
if (cfg.parse(args, argidx))
continue;
}
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
max_seq = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-set-assumes") {
set_assumes = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -253,7 +221,7 @@ struct EquivInductPass : public Pass {
continue;
}
EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes);
EquivInductWorker worker(module, unproven_equiv_cells, cfg);
worker.run();
success_counter += worker.success_counter;
}

118
passes/equiv/equiv_simple.cc
View file

@ -17,15 +17,52 @@
*
*/
#include "kernel/log.h"
#include "kernel/yosys.h"
#include "kernel/satgen.h"
#include "passes/equiv/equiv.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct EquivSimpleWorker
struct EquivSimpleWorker : public EquivWorker
{
Module *module;
struct Config : EquivWorker::Config {
bool verbose = false;
bool short_cones = false;
bool group = true;
bool parse(const std::vector<std::string>& args, size_t& idx) {
if (EquivWorker::Config::parse(args, idx))
return true;
if (args[idx] == "-v") {
verbose = true;
return true;
}
if (args[idx] == "-short") {
short_cones = true;
return true;
}
if (args[idx] == "-nogroup") {
group = false;
return true;
}
return false;
}
static std::string help(const char* default_seq) {
return EquivWorker::Config::help(default_seq) +
" -v\n"
" verbose output\n"
"\n"
" -short\n"
" create shorter input cones that stop at shared nodes. This yields\n"
" simpler SAT problems but sometimes fails to prove equivalence.\n"
"\n"
" -nogroup\n"
" disabling grouping of $equiv cells by output wire\n"
"\n";
}
};
Config cfg;
const vector<Cell*> &equiv_cells;
const vector<Cell*> &assume_cells;
struct Cone {
@ -43,27 +80,11 @@ struct EquivSimpleWorker
};
DesignModel model;
ezSatPtr ez;
SatGen satgen;
struct Config {
bool verbose = false;
bool short_cones = false;
bool model_undef = false;
bool nogroup = false;
bool set_assumes = false;
int max_seq = 1;
};
Config cfg;
pool<pair<Cell*, int>> imported_cells_cache;
EquivSimpleWorker(const vector<Cell*> &equiv_cells, const vector<Cell*> &assume_cells, DesignModel model, Config cfg) :
module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells),
model(model), satgen(ez.get(), &model.sigmap), cfg(cfg)
{
satgen.model_undef = cfg.model_undef;
}
EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells),
model(model) {}
struct ConeFinder {
DesignModel model;
@ -229,14 +250,6 @@ struct EquivSimpleWorker
return extra_problem_cells;
}
static void report_missing_model(Cell* cell)
{
if (cell->is_builtin_ff())
log_cmd_error("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
else
log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
}
void prepare_ezsat(int ez_context, SigBit bit_a, SigBit bit_b)
{
if (satgen.model_undef)
@ -323,7 +336,7 @@ struct EquivSimpleWorker
for (auto cell : problem_cells) {
auto key = pair<Cell*, int>(cell, step+1);
if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
report_missing_model(cell);
report_missing_model(true, cell);
}
imported_cells_cache.insert(key);
}
@ -414,24 +427,7 @@ struct EquivSimplePass : public Pass {
log("\n");
log("This command tries to prove $equiv cells using a simple direct SAT approach.\n");
log("\n");
log(" -v\n");
log(" verbose output\n");
log("\n");
log(" -undef\n");
log(" enable modelling of undef states\n");
log("\n");
log(" -short\n");
log(" create shorter input cones that stop at shared nodes. This yields\n");
log(" simpler SAT problems but sometimes fails to prove equivalence.\n");
log("\n");
log(" -nogroup\n");
log(" disabling grouping of $equiv cells by output wire\n");
log("\n");
log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 1)\n");
log("\n");
log(" -set-assumes\n");
log(" set all assumptions provided via $assume cells\n");
EquivSimpleWorker::Config::help("1");
log("\n");
}
void execute(std::vector<std::string> args, Design *design) override
@ -443,30 +439,8 @@ struct EquivSimplePass : public Pass {
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-v") {
cfg.verbose = true;
if (cfg.parse(args, argidx))
continue;
}
if (args[argidx] == "-short") {
cfg.short_cones = true;
continue;
}
if (args[argidx] == "-undef") {
cfg.model_undef = true;
continue;
}
if (args[argidx] == "-nogroup") {
cfg.nogroup = true;
continue;
}
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
cfg.max_seq = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-set-assumes") {
cfg.set_assumes = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -489,7 +463,7 @@ struct EquivSimplePass : public Pass {
if (cell->type == ID($equiv) && cell->getPort(ID::A) != cell->getPort(ID::B)) {
auto bit = sigmap(cell->getPort(ID::Y).as_bit());
auto bit_group = bit;
if (!cfg.nogroup && bit_group.wire)
if (cfg.group && bit_group.wire)
bit_group.offset = 0;
unproven_equiv_cells[bit_group][bit] = cell;
unproven_cells_counter++;