mirror of
https://github.com/YosysHQ/yosys
synced 2026-03-01 11:16:55 +00:00
67 lines
1.5 KiB
C++
67 lines
1.5 KiB
C++
#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
|
|
|
|
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;
|
|
SatGen satgen;
|
|
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
|