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

equiv_simple, equiv_induct: error by default on missing model, add -ignore-unknown-cells

This commit is contained in:
Emil J. Tywoniak 2026-02-03 17:59:31 +01:00
parent 8e73e2a306
commit 8d1c1faf82
3 changed files with 10 additions and 2 deletions

View file

@ -33,6 +33,7 @@ struct EquivWorker {
bool model_undef = false;
int max_seq = 1;
bool set_assumes = false;
bool ignore_unknown_cells = false;
bool parse(const std::vector<std::string>& args, size_t& idx) {
if (args[idx] == "-undef") {
@ -47,6 +48,10 @@ struct EquivWorker {
set_assumes = true;
return true;
}
if (args[idx] == "-ignore-unknown-cells") {
ignore_unknown_cells = true;
return true;
}
return false;
}
static std::string help(const char* default_seq) {
@ -59,6 +64,9 @@ struct EquivWorker {
"\n"
" -set-assumes\n"
" set all assumptions provided via $assume cells\n"
"\n"
" -ignore-unknown-cells\n"
" ignore all cells that can not be matched to a SAT model\n"
, default_seq);
}
};

View file

@ -45,7 +45,7 @@ struct EquivInductWorker : public EquivWorker
for (auto cell : cells) {
if (!satgen.importCell(cell, step)) {
report_missing_model(true, cell);
report_missing_model(cfg.ignore_unknown_cells, cell);
}
if (cell->type == ID($equiv)) {
SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit();

View file

@ -336,7 +336,7 @@ struct EquivSimpleWorker : public EquivWorker
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(true, cell);
report_missing_model(cfg.ignore_unknown_cells, cell);
}
imported_cells_cache.insert(key);
}