mirror of
https://github.com/YosysHQ/yosys
synced 2026-02-14 12:51:48 +00:00
equiv_simple, equiv_induct: fix config
This commit is contained in:
Emil J. Tywoniak
parent
c768e55983
commit
ed53ff2f49
3 changed files with 90 additions and 88 deletions
|
|
@ -23,54 +23,55 @@ static void report_missing_model(bool warn_only, RTLIL::Cell* cell)
|
|||
}
|
||||
}
|
||||
|
||||
struct EquivBasicConfig {
|
||||
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") {
|
||||
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;
|
||||
}
|
||||
if (args[idx] == "-ignore-unknown-cells") {
|
||||
ignore_unknown_cells = 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"
|
||||
"\n"
|
||||
" -ignore-unknown-cells\n"
|
||||
" ignore all cells that can not be matched to a SAT model\n"
|
||||
, default_seq);
|
||||
}
|
||||
};
|
||||
|
||||
template<typename Config = EquivBasicConfig>
|
||||
struct EquivWorker {
|
||||
RTLIL::Module *module;
|
||||
|
||||
ezSatPtr ez;
|
||||
ezSatPtr ez;
|
||||
SatGen satgen;
|
||||
|
||||
struct Config {
|
||||
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") {
|
||||
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;
|
||||
}
|
||||
if (args[idx] == "-ignore-unknown-cells") {
|
||||
ignore_unknown_cells = 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"
|
||||
"\n"
|
||||
" -ignore-unknown-cells\n"
|
||||
" ignore all cells that can not be matched to a SAT model\n"
|
||||
, default_seq);
|
||||
}
|
||||
};
|
||||
Config cfg;
|
||||
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;
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@
|
|||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct EquivInductWorker : public EquivWorker
|
||||
struct EquivInductWorker : public EquivWorker<>
|
||||
{
|
||||
SigMap sigmap;
|
||||
|
||||
|
|
@ -35,7 +35,7 @@ struct EquivInductWorker : public EquivWorker
|
|||
dict<int, int> ez_step_is_consistent;
|
||||
SigPool undriven_signals;
|
||||
|
||||
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, Config cfg) : EquivWorker(module, &sigmap, cfg), sigmap(module),
|
||||
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, EquivBasicConfig cfg) : EquivWorker<>(module, &sigmap, cfg), sigmap(module),
|
||||
cells(module->selected_cells()), workset(unproven_equiv_cells),
|
||||
success_counter(0) {}
|
||||
|
||||
|
|
@ -174,7 +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");
|
||||
EquivWorker::Config::help("4");
|
||||
EquivBasicConfig::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");
|
||||
|
|
@ -192,7 +192,7 @@ struct EquivInductPass : public Pass {
|
|||
void execute(std::vector<std::string> args, Design *design) override
|
||||
{
|
||||
int success_counter = 0;
|
||||
EquivWorker::Config cfg;
|
||||
EquivBasicConfig cfg {};
|
||||
cfg.max_seq = 4;
|
||||
|
||||
log_header(design, "Executing EQUIV_INDUCT pass.\n");
|
||||
|
|
|
|||
|
|
@ -24,45 +24,44 @@
|
|||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct EquivSimpleWorker : public EquivWorker
|
||||
{
|
||||
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;
|
||||
struct EquivSimpleConfig : EquivBasicConfig {
|
||||
bool verbose = false;
|
||||
bool short_cones = false;
|
||||
bool group = true;
|
||||
bool parse(const std::vector<std::string>& args, size_t& idx) {
|
||||
if (EquivBasicConfig::parse(args, idx))
|
||||
return true;
|
||||
if (args[idx] == "-v") {
|
||||
verbose = true;
|
||||
return true;
|
||||
}
|
||||
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";
|
||||
if (args[idx] == "-short") {
|
||||
short_cones = true;
|
||||
return true;
|
||||
}
|
||||
};
|
||||
Config cfg;
|
||||
if (args[idx] == "-nogroup") {
|
||||
group = false;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
static std::string help(const char* default_seq) {
|
||||
return EquivBasicConfig::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";
|
||||
}
|
||||
};
|
||||
|
||||
struct EquivSimpleWorker : public EquivWorker<EquivSimpleConfig>
|
||||
{
|
||||
const vector<Cell*> &equiv_cells;
|
||||
const vector<Cell*> &assume_cells;
|
||||
struct Cone {
|
||||
|
|
@ -82,8 +81,8 @@ struct EquivSimpleWorker : public EquivWorker
|
|||
|
||||
pool<pair<Cell*, int>> imported_cells_cache;
|
||||
|
||||
EquivSimpleWorker(const vector<Cell*> &equiv_cells, const vector<Cell*> &assume_cells, DesignModel model, Config cfg) :
|
||||
EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells),
|
||||
EquivSimpleWorker(const vector<Cell*> &equiv_cells, const vector<Cell*> &assume_cells, DesignModel model, EquivSimpleConfig cfg) :
|
||||
EquivWorker<EquivSimpleConfig>(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells),
|
||||
model(model) {}
|
||||
|
||||
struct ConeFinder {
|
||||
|
|
@ -270,7 +269,9 @@ struct EquivSimpleWorker : public EquivWorker
|
|||
}
|
||||
void construct_ezsat(const pool<SigBit>& input_bits, int step)
|
||||
{
|
||||
log("ezsat\n");
|
||||
if (cfg.set_assumes) {
|
||||
log("yep assume\n");
|
||||
if (cfg.verbose && step == cfg.max_seq) {
|
||||
RTLIL::SigSpec assumes_a, assumes_en;
|
||||
satgen.getAssumes(assumes_a, assumes_en, step+1);
|
||||
|
|
@ -427,12 +428,12 @@ struct EquivSimplePass : public Pass {
|
|||
log("\n");
|
||||
log("This command tries to prove $equiv cells using a simple direct SAT approach.\n");
|
||||
log("\n");
|
||||
EquivSimpleWorker::Config::help("1");
|
||||
EquivSimpleConfig::help("1");
|
||||
log("\n");
|
||||
}
|
||||
void execute(std::vector<std::string> args, Design *design) override
|
||||
{
|
||||
EquivSimpleWorker::Config cfg = {};
|
||||
EquivSimpleConfig cfg {};
|
||||
int success_counter = 0;
|
||||
|
||||
log_header(design, "Executing EQUIV_SIMPLE pass.\n");
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue