mirror of
https://github.com/YosysHQ/yosys
synced 2025-08-11 13:40:53 +00:00
Merge pull request #5273 from YosysHQ/emil/krys-equiv_assume-refactor
equiv_simple: refactor
This commit is contained in:
Emil J
GitHub
commit
94d3b3eb5a
2 changed files with 272 additions and 203 deletions
|
|
@ -64,7 +64,7 @@ struct ezSatPtr : public std::unique_ptr<ezSAT> {
|
|||
struct SatGen
|
||||
{
|
||||
ezSAT *ez;
|
||||
SigMap *sigmap;
|
||||
const SigMap *sigmap;
|
||||
std::string prefix;
|
||||
SigPool initial_state;
|
||||
std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en;
|
||||
|
|
@ -75,12 +75,12 @@ struct SatGen
|
|||
bool model_undef;
|
||||
bool def_formal = false;
|
||||
|
||||
SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
|
||||
SatGen(ezSAT *ez, const SigMap *sigmap, std::string prefix = std::string()) :
|
||||
ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
|
||||
{
|
||||
}
|
||||
|
||||
void setContext(SigMap *sigmap, std::string prefix = std::string())
|
||||
void setContext(const SigMap *sigmap, std::string prefix = std::string())
|
||||
{
|
||||
this->sigmap = sigmap;
|
||||
this->prefix = prefix;
|
||||
|
|
|
|||
|
|
@ -28,273 +28,344 @@ struct EquivSimpleWorker
|
|||
Module *module;
|
||||
const vector<Cell*> &equiv_cells;
|
||||
const vector<Cell*> &assume_cells;
|
||||
Cell *equiv_cell;
|
||||
struct Cone {
|
||||
pool<Cell*> cells;
|
||||
pool<SigBit> bits;
|
||||
void clear() {
|
||||
cells.clear();
|
||||
bits.clear();
|
||||
}
|
||||
};
|
||||
|
||||
SigMap &sigmap;
|
||||
dict<SigBit, Cell*> &bit2driver;
|
||||
struct DesignModel {
|
||||
const SigMap &sigmap;
|
||||
dict<SigBit, Cell*> &bit2driver;
|
||||
};
|
||||
DesignModel model;
|
||||
|
||||
ezSatPtr ez;
|
||||
SatGen satgen;
|
||||
int max_seq;
|
||||
bool short_cones;
|
||||
bool verbose;
|
||||
bool set_assumes;
|
||||
|
||||
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, SigMap &sigmap, dict<SigBit, Cell*> &bit2driver, int max_seq, bool short_cones, bool verbose, bool model_undef, bool set_assumes) :
|
||||
module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells), equiv_cell(nullptr),
|
||||
sigmap(sigmap), bit2driver(bit2driver), satgen(ez.get(), &sigmap), max_seq(max_seq), short_cones(short_cones), verbose(verbose), set_assumes(set_assumes)
|
||||
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 = model_undef;
|
||||
satgen.model_undef = cfg.model_undef;
|
||||
}
|
||||
|
||||
bool find_input_cone(pool<SigBit> &next_seed, pool<Cell*> &cells_cone, pool<SigBit> &bits_cone, const pool<Cell*> &cells_stop, const pool<SigBit> &bits_stop, pool<SigBit> *input_bits, Cell *cell)
|
||||
{
|
||||
if (cells_cone.count(cell))
|
||||
struct ConeFinder {
|
||||
DesignModel model;
|
||||
// Bits we should also analyze in a later iteration (flop inputs)
|
||||
pool<SigBit> &next_seed;
|
||||
// Cells and bits we've seen so far while traversing
|
||||
Cone& cone;
|
||||
// We're not allowed to traverse past cells and bits in `stop`
|
||||
const Cone& stop;
|
||||
// Input bits are bits that no longer can be traversed
|
||||
// Tracking these is optional
|
||||
pool<SigBit>* input_bits;
|
||||
|
||||
// Recursively traverses backwards from a cell to find all cells in its input cone
|
||||
// Adds cell to cone.cells, stops at cells in 'stop' set
|
||||
// Returns true if stopped on a stop cell
|
||||
bool find_input_cone(Cell *cell)
|
||||
{
|
||||
if (cone.cells.count(cell))
|
||||
return false;
|
||||
|
||||
cone.cells.insert(cell);
|
||||
|
||||
if (stop.cells.count(cell))
|
||||
return true;
|
||||
|
||||
for (auto &conn : cell->connections())
|
||||
if (yosys_celltypes.cell_input(cell->type, conn.first))
|
||||
for (auto bit : model.sigmap(conn.second)) {
|
||||
if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
|
||||
if (!conn.first.in(ID::CLK, ID::C))
|
||||
next_seed.insert(bit);
|
||||
} else
|
||||
find_input_cone(bit);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
void find_input_cone(SigBit bit)
|
||||
{
|
||||
if (cone.bits.count(bit))
|
||||
return;
|
||||
|
||||
cells_cone.insert(cell);
|
||||
cone.bits.insert(bit);
|
||||
|
||||
if (cells_stop.count(cell))
|
||||
return true;
|
||||
if (stop.bits.count(bit)) {
|
||||
if (input_bits != nullptr) input_bits->insert(bit);
|
||||
return;
|
||||
}
|
||||
|
||||
for (auto &conn : cell->connections())
|
||||
if (yosys_celltypes.cell_input(cell->type, conn.first))
|
||||
for (auto bit : sigmap(conn.second)) {
|
||||
if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
|
||||
if (!conn.first.in(ID::CLK, ID::C))
|
||||
next_seed.insert(bit);
|
||||
} else
|
||||
find_input_cone(next_seed, cells_cone, bits_cone, cells_stop, bits_stop, input_bits, bit);
|
||||
}
|
||||
return false;
|
||||
}
|
||||
if (!model.bit2driver.count(bit))
|
||||
return;
|
||||
|
||||
void find_input_cone(pool<SigBit> &next_seed, pool<Cell*> &cells_cone, pool<SigBit> &bits_cone, const pool<Cell*> &cells_stop, const pool<SigBit> &bits_stop, pool<SigBit> *input_bits, SigBit bit)
|
||||
// If the input cone of the driver cell reaches a stop bit,
|
||||
// then `bit` is an "input bit"
|
||||
if (find_input_cone(model.bit2driver.at(bit)))
|
||||
if (input_bits != nullptr) input_bits->insert(bit);
|
||||
}
|
||||
void find_input_cone(pool<SigBit> bits)
|
||||
{
|
||||
for (auto bit : bits)
|
||||
find_input_cone(bit);
|
||||
}
|
||||
};
|
||||
|
||||
// Builds (full or short) input cones from the seeds
|
||||
// Creates full cones (no stops) and optionally short cones (stop at other side's cone)
|
||||
// Updates seed_a/seed_b with next iteration's FF inputs
|
||||
// Returns input bits and cone structures for SAT problem construction
|
||||
std::tuple<pool<SigBit>, Cone, Cone> init_iter(pool<SigBit>& seed_a, pool<SigBit>& seed_b) const
|
||||
{
|
||||
if (bits_cone.count(bit))
|
||||
return;
|
||||
// Empty, never inserted to, to traverse full cones
|
||||
const Cone no_stop;
|
||||
Cone full_cone_a, full_cone_b;
|
||||
|
||||
bits_cone.insert(bit);
|
||||
// Values of seed_* for the next iteration
|
||||
pool<SigBit> next_seed_a, next_seed_b;
|
||||
|
||||
if (bits_stop.count(bit)) {
|
||||
if (input_bits != nullptr) input_bits->insert(bit);
|
||||
return;
|
||||
{
|
||||
ConeFinder finder_a {model, next_seed_a, full_cone_a, no_stop, nullptr};
|
||||
finder_a.find_input_cone(seed_a);
|
||||
|
||||
ConeFinder finder_b {model, next_seed_b, full_cone_b, no_stop, nullptr};
|
||||
finder_b.find_input_cone(seed_b);
|
||||
}
|
||||
|
||||
if (!bit2driver.count(bit))
|
||||
return;
|
||||
Cone short_cone_a, short_cone_b;
|
||||
pool<SigBit> input_bits;
|
||||
|
||||
if (find_input_cone(next_seed, cells_cone, bits_cone, cells_stop, bits_stop, input_bits, bit2driver.at(bit)))
|
||||
if (input_bits != nullptr) input_bits->insert(bit);
|
||||
if (cfg.short_cones)
|
||||
{
|
||||
// Rebuild cones with the knowledge of the full cones.
|
||||
// Avoids stuffing overlaps in input cones into the solver
|
||||
// e.g. for A by using the full B cone as stops
|
||||
next_seed_a.clear();
|
||||
ConeFinder short_finder_a = {model, next_seed_a, short_cone_a, short_cone_b, &input_bits};
|
||||
short_finder_a.find_input_cone(seed_a);
|
||||
next_seed_a.swap(seed_a);
|
||||
|
||||
next_seed_b.clear();
|
||||
ConeFinder short_finder_b = {model, next_seed_b, short_cone_b, short_cone_a, &input_bits};
|
||||
short_finder_b.find_input_cone(seed_b);
|
||||
next_seed_b.swap(seed_b);
|
||||
}
|
||||
else
|
||||
{
|
||||
short_cone_a = full_cone_a;
|
||||
next_seed_a.swap(seed_a);
|
||||
|
||||
short_cone_b = full_cone_b;
|
||||
next_seed_b.swap(seed_b);
|
||||
}
|
||||
return std::make_tuple(input_bits, short_cone_a, short_cone_b);
|
||||
}
|
||||
|
||||
bool run_cell()
|
||||
void report_new_cells(const pool<Cell*>& cells, const Cone& cone_a, const Cone& cone_b) const
|
||||
{
|
||||
SigBit bit_a = sigmap(equiv_cell->getPort(ID::A)).as_bit();
|
||||
SigBit bit_b = sigmap(equiv_cell->getPort(ID::B)).as_bit();
|
||||
int ez_context = ez->frozen_literal();
|
||||
log(" Adding %d new cells to the problem (%d A, %d B, %d shared).\n",
|
||||
GetSize(cells), GetSize(cone_a.cells), GetSize(cone_b.cells),
|
||||
(GetSize(cone_a.cells) + GetSize(cone_b.cells)) - GetSize(cells));
|
||||
#if 0
|
||||
for (auto cell : short_cells_cone_a)
|
||||
log(" A-side cell: %s\n", log_id(cell));
|
||||
|
||||
for (auto cell : short_cells_cone_b)
|
||||
log(" B-side cell: %s\n", log_id(cell));
|
||||
#endif
|
||||
}
|
||||
void report_new_assume_cells(const pool<Cell*>& extra_problem_cells, int old_size, const pool<Cell*>& problem_cells) const
|
||||
{
|
||||
if (cfg.verbose) {
|
||||
log(" Adding %d new cells to check assumptions (and reusing %d).\n",
|
||||
GetSize(problem_cells) - old_size,
|
||||
old_size - (GetSize(problem_cells) - GetSize(extra_problem_cells)));
|
||||
#if 0
|
||||
for (auto cell : extra_problem_cells)
|
||||
log(" cell: %s\n", log_id(cell));
|
||||
#endif
|
||||
}
|
||||
}
|
||||
|
||||
// Ensure the input cones of $assume cells get modelled by the problem
|
||||
pool<Cell*> add_assumes_to_problem(const Cone& cone_a, const Cone& cone_b) const
|
||||
{
|
||||
pool<Cell*> extra_problem_cells;
|
||||
for (auto assume : assume_cells) {
|
||||
pool<SigBit> assume_seed, dummy_next_seed, overlap_bits;
|
||||
assume_seed.insert(model.sigmap(assume->getPort(ID::A)).as_bit());
|
||||
assume_seed.insert(model.sigmap(assume->getPort(ID::EN)).as_bit());
|
||||
|
||||
for (auto& cone : {cone_a, cone_b}) {
|
||||
Cone assume_cone;
|
||||
ConeFinder{model, dummy_next_seed, assume_cone, cone, &overlap_bits}
|
||||
.find_input_cone(assume_seed);
|
||||
if (GetSize(overlap_bits)) {
|
||||
extra_problem_cells.insert(assume);
|
||||
extra_problem_cells.insert(assume_cone.cells.begin(), assume_cone.cells.end());
|
||||
overlap_bits.clear();
|
||||
}
|
||||
assume_cone.clear();
|
||||
dummy_next_seed.clear();
|
||||
}
|
||||
}
|
||||
return extra_problem_cells;
|
||||
}
|
||||
|
||||
static void report_missing_model(Cell* cell)
|
||||
{
|
||||
if (RTLIL::builtin_ff_cell_types().count(cell->type))
|
||||
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)
|
||||
{
|
||||
int ez_a = satgen.importSigBit(bit_a, max_seq+1);
|
||||
int ez_b = satgen.importDefSigBit(bit_b, max_seq+1);
|
||||
int ez_undef_a = satgen.importUndefSigBit(bit_a, max_seq+1);
|
||||
int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1);
|
||||
int ez_b = satgen.importDefSigBit(bit_b, cfg.max_seq+1);
|
||||
int ez_undef_a = satgen.importUndefSigBit(bit_a, cfg.max_seq+1);
|
||||
|
||||
ez->assume(ez->XOR(ez_a, ez_b), ez_context);
|
||||
ez->assume(ez->NOT(ez_undef_a), ez_context);
|
||||
}
|
||||
else
|
||||
{
|
||||
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);
|
||||
ez->assume(ez->XOR(ez_a, ez_b), ez_context);
|
||||
}
|
||||
}
|
||||
void construct_ezsat(const pool<SigBit>& input_bits, int step)
|
||||
{
|
||||
if (cfg.set_assumes) {
|
||||
if (cfg.verbose && step == cfg.max_seq) {
|
||||
RTLIL::SigSpec assumes_a, assumes_en;
|
||||
satgen.getAssumes(assumes_a, assumes_en, step+1);
|
||||
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));
|
||||
}
|
||||
|
||||
if (satgen.model_undef) {
|
||||
for (auto bit : input_bits)
|
||||
ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1)));
|
||||
}
|
||||
|
||||
if (cfg.verbose)
|
||||
log(" Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses());
|
||||
}
|
||||
|
||||
bool prove_equiv_cell(Cell* cell)
|
||||
{
|
||||
SigBit bit_a = model.sigmap(cell->getPort(ID::A)).as_bit();
|
||||
SigBit bit_b = model.sigmap(cell->getPort(ID::B)).as_bit();
|
||||
int ez_context = ez->frozen_literal();
|
||||
|
||||
prepare_ezsat(ez_context, bit_a, bit_b);
|
||||
|
||||
// Two bits, bit_a, and bit_b, have been marked equivalent in the design
|
||||
// We will be traversing the input cones for each of them
|
||||
// In the first iteration, we will using those as starting points
|
||||
pool<SigBit> seed_a = { bit_a };
|
||||
pool<SigBit> seed_b = { bit_b };
|
||||
|
||||
if (verbose) {
|
||||
log(" Trying to prove $equiv cell %s:\n", log_id(equiv_cell));
|
||||
log(" A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(equiv_cell->getPort(ID::Y)));
|
||||
if (cfg.verbose) {
|
||||
log(" Trying to prove $equiv cell %s:\n", log_id(cell));
|
||||
log(" A = %s, B = %s, Y = %s\n", log_signal(bit_a), log_signal(bit_b), log_signal(cell->getPort(ID::Y)));
|
||||
} else {
|
||||
log(" Trying to prove $equiv for %s:", log_signal(equiv_cell->getPort(ID::Y)));
|
||||
log(" Trying to prove $equiv for %s:", log_signal(cell->getPort(ID::Y)));
|
||||
}
|
||||
|
||||
int step = max_seq;
|
||||
int step = cfg.max_seq;
|
||||
while (1)
|
||||
{
|
||||
pool<Cell*> no_stop_cells;
|
||||
pool<SigBit> no_stop_bits;
|
||||
|
||||
pool<Cell*> full_cells_cone_a, full_cells_cone_b;
|
||||
pool<SigBit> full_bits_cone_a, full_bits_cone_b;
|
||||
|
||||
pool<SigBit> next_seed_a, next_seed_b;
|
||||
|
||||
for (auto bit_a : seed_a)
|
||||
find_input_cone(next_seed_a, full_cells_cone_a, full_bits_cone_a, no_stop_cells, no_stop_bits, nullptr, bit_a);
|
||||
|
||||
for (auto bit_b : seed_b)
|
||||
find_input_cone(next_seed_b, full_cells_cone_b, full_bits_cone_b, no_stop_cells, no_stop_bits, nullptr, bit_b);
|
||||
|
||||
pool<Cell*> short_cells_cone_a, short_cells_cone_b;
|
||||
pool<SigBit> short_bits_cone_a, short_bits_cone_b;
|
||||
pool<SigBit> input_bits;
|
||||
|
||||
if (short_cones)
|
||||
{
|
||||
next_seed_a.clear();
|
||||
for (auto bit_a : seed_a)
|
||||
find_input_cone(next_seed_a, short_cells_cone_a, short_bits_cone_a, full_cells_cone_b, full_bits_cone_b, &input_bits, bit_a);
|
||||
next_seed_a.swap(seed_a);
|
||||
|
||||
next_seed_b.clear();
|
||||
for (auto bit_b : seed_b)
|
||||
find_input_cone(next_seed_b, short_cells_cone_b, short_bits_cone_b, full_cells_cone_a, full_bits_cone_a, &input_bits, bit_b);
|
||||
next_seed_b.swap(seed_b);
|
||||
}
|
||||
else
|
||||
{
|
||||
short_cells_cone_a = full_cells_cone_a;
|
||||
short_bits_cone_a = full_bits_cone_a;
|
||||
next_seed_a.swap(seed_a);
|
||||
|
||||
short_cells_cone_b = full_cells_cone_b;
|
||||
short_bits_cone_b = full_bits_cone_b;
|
||||
next_seed_b.swap(seed_b);
|
||||
}
|
||||
// Traverse input cones of seed_a and seed_b, potentially finding new seeds
|
||||
auto [input_bits, cone_a, cone_b] = init_iter(seed_a, seed_b);
|
||||
|
||||
// Cells to model in SAT solver
|
||||
pool<Cell*> problem_cells;
|
||||
problem_cells.insert(short_cells_cone_a.begin(), short_cells_cone_a.end());
|
||||
problem_cells.insert(short_cells_cone_b.begin(), short_cells_cone_b.end());
|
||||
problem_cells.insert(cone_a.cells.begin(), cone_a.cells.end());
|
||||
problem_cells.insert(cone_b.cells.begin(), cone_b.cells.end());
|
||||
|
||||
if (verbose)
|
||||
{
|
||||
log(" Adding %d new cells to the problem (%d A, %d B, %d shared).\n",
|
||||
GetSize(problem_cells), GetSize(short_cells_cone_a), GetSize(short_cells_cone_b),
|
||||
(GetSize(short_cells_cone_a) + GetSize(short_cells_cone_b)) - GetSize(problem_cells));
|
||||
#if 0
|
||||
for (auto cell : short_cells_cone_a)
|
||||
log(" A-side cell: %s\n", log_id(cell));
|
||||
if (cfg.verbose)
|
||||
report_new_cells(problem_cells, cone_a, cone_b);
|
||||
|
||||
for (auto cell : short_cells_cone_b)
|
||||
log(" B-side cell: %s\n", log_id(cell));
|
||||
#endif
|
||||
}
|
||||
|
||||
if (set_assumes) {
|
||||
pool<Cell*> extra_problem_cells;
|
||||
for (auto assume : assume_cells) {
|
||||
pool<SigBit> assume_seed, next_assume_seed;
|
||||
assume_seed.insert(sigmap(assume->getPort(ID::A)).as_bit());
|
||||
assume_seed.insert(sigmap(assume->getPort(ID::EN)).as_bit());
|
||||
pool<Cell*> assume_cells_cone;
|
||||
pool<SigBit> assume_bits_cone;
|
||||
pool<SigBit> overlap_bits;
|
||||
for (auto bit_x : assume_seed) {
|
||||
find_input_cone(next_assume_seed, assume_cells_cone, assume_bits_cone, short_cells_cone_a, short_bits_cone_a, &overlap_bits, bit_x);
|
||||
}
|
||||
if (GetSize(overlap_bits)) {
|
||||
extra_problem_cells.insert(assume);
|
||||
extra_problem_cells.insert(assume_cells_cone.begin(), assume_cells_cone.end());
|
||||
overlap_bits.clear();
|
||||
}
|
||||
assume_cells_cone.clear();
|
||||
assume_bits_cone.clear();
|
||||
for (auto bit_x : assume_seed) {
|
||||
find_input_cone(next_assume_seed, assume_cells_cone, assume_bits_cone, short_cells_cone_b, short_bits_cone_b, &overlap_bits, bit_x);
|
||||
}
|
||||
if (GetSize(overlap_bits)) {
|
||||
extra_problem_cells.insert(assume);
|
||||
extra_problem_cells.insert(assume_cells_cone.begin(), assume_cells_cone.end());
|
||||
overlap_bits.clear();
|
||||
}
|
||||
assume_cells_cone.clear();
|
||||
assume_bits_cone.clear();
|
||||
next_assume_seed.clear();
|
||||
}
|
||||
|
||||
if (GetSize(extra_problem_cells)) {
|
||||
if (cfg.set_assumes) {
|
||||
auto extras = add_assumes_to_problem(cone_a, cone_b);
|
||||
if (GetSize(extras)) {
|
||||
auto old_size = GetSize(problem_cells);
|
||||
problem_cells.insert(extra_problem_cells.begin(), extra_problem_cells.end());
|
||||
if (verbose) {
|
||||
log(" Adding %d new cells to check assumptions (and reusing %d).\n",
|
||||
GetSize(problem_cells) - old_size,
|
||||
old_size - (GetSize(problem_cells) - GetSize(extra_problem_cells)));
|
||||
#if 0
|
||||
for (auto cell : extra_problem_cells)
|
||||
log(" cell: %s\n", log_id(cell));
|
||||
#endif
|
||||
}
|
||||
problem_cells.insert(extras.begin(), extras.end());
|
||||
report_new_assume_cells(extras, old_size, problem_cells);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto cell : problem_cells) {
|
||||
auto key = pair<Cell*, int>(cell, step+1);
|
||||
if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
|
||||
if (RTLIL::builtin_ff_cell_types().count(cell->type))
|
||||
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));
|
||||
report_missing_model(cell);
|
||||
}
|
||||
imported_cells_cache.insert(key);
|
||||
}
|
||||
|
||||
if (set_assumes) {
|
||||
if (verbose && step == max_seq) {
|
||||
RTLIL::SigSpec assumes_a, assumes_en;
|
||||
satgen.getAssumes(assumes_a, assumes_en, step+1);
|
||||
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));
|
||||
}
|
||||
|
||||
if (satgen.model_undef) {
|
||||
for (auto bit : input_bits)
|
||||
ez->assume(ez->NOT(satgen.importUndefSigBit(bit, step+1)));
|
||||
}
|
||||
|
||||
if (verbose)
|
||||
log(" Problem size at t=%d: %d literals, %d clauses\n", step, ez->numCnfVariables(), ez->numCnfClauses());
|
||||
construct_ezsat(input_bits, step);
|
||||
|
||||
if (!ez->solve(ez_context)) {
|
||||
log(verbose ? " Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n");
|
||||
equiv_cell->setPort(ID::B, equiv_cell->getPort(ID::A));
|
||||
log(cfg.verbose ? " Proved equivalence! Marking $equiv cell as proven.\n" : " success!\n");
|
||||
// Replace $equiv cell with a short
|
||||
cell->setPort(ID::B, cell->getPort(ID::A));
|
||||
ez->assume(ez->NOT(ez_context));
|
||||
return true;
|
||||
}
|
||||
|
||||
if (verbose)
|
||||
log(" Failed to prove equivalence with sequence length %d.\n", max_seq - step);
|
||||
if (cfg.verbose)
|
||||
log(" Failed to prove equivalence with sequence length %d.\n", cfg.max_seq - step);
|
||||
|
||||
if (--step < 0) {
|
||||
if (verbose)
|
||||
if (cfg.verbose)
|
||||
log(" Reached sequence limit.\n");
|
||||
break;
|
||||
}
|
||||
|
||||
if (seed_a.empty() && seed_b.empty()) {
|
||||
if (verbose)
|
||||
if (cfg.verbose)
|
||||
log(" No nets to continue in previous time step.\n");
|
||||
break;
|
||||
}
|
||||
|
||||
if (seed_a.empty()) {
|
||||
if (verbose)
|
||||
if (cfg.verbose)
|
||||
log(" No nets on A-side to continue in previous time step.\n");
|
||||
break;
|
||||
}
|
||||
|
||||
if (seed_b.empty()) {
|
||||
if (verbose)
|
||||
if (cfg.verbose)
|
||||
log(" No nets on B-side to continue in previous time step.\n");
|
||||
break;
|
||||
}
|
||||
|
||||
if (verbose) {
|
||||
if (cfg.verbose) {
|
||||
#if 0
|
||||
log(" Continuing analysis in previous time step with the following nets:\n");
|
||||
for (auto bit : seed_a)
|
||||
|
|
@ -307,7 +378,7 @@ struct EquivSimpleWorker
|
|||
}
|
||||
}
|
||||
|
||||
if (!verbose)
|
||||
if (!cfg.verbose)
|
||||
log(" failed.\n");
|
||||
|
||||
ez->assume(ez->NOT(ez_context));
|
||||
|
|
@ -319,14 +390,13 @@ struct EquivSimpleWorker
|
|||
if (GetSize(equiv_cells) > 1) {
|
||||
SigSpec sig;
|
||||
for (auto c : equiv_cells)
|
||||
sig.append(sigmap(c->getPort(ID::Y)));
|
||||
sig.append(model.sigmap(c->getPort(ID::Y)));
|
||||
log(" Grouping SAT models for %s:\n", log_signal(sig));
|
||||
}
|
||||
|
||||
int counter = 0;
|
||||
for (auto c : equiv_cells) {
|
||||
equiv_cell = c;
|
||||
if (run_cell())
|
||||
if (prove_equiv_cell(c))
|
||||
counter++;
|
||||
}
|
||||
return counter;
|
||||
|
|
@ -366,37 +436,35 @@ struct EquivSimplePass : public Pass {
|
|||
}
|
||||
void execute(std::vector<std::string> args, Design *design) override
|
||||
{
|
||||
bool verbose = false, short_cones = false, model_undef = false, nogroup = false;
|
||||
bool set_assumes = false;
|
||||
EquivSimpleWorker::Config cfg = {};
|
||||
int success_counter = 0;
|
||||
int max_seq = 1;
|
||||
|
||||
log_header(design, "Executing EQUIV_SIMPLE pass.\n");
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++) {
|
||||
if (args[argidx] == "-v") {
|
||||
verbose = true;
|
||||
cfg.verbose = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-short") {
|
||||
short_cones = true;
|
||||
cfg.short_cones = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-undef") {
|
||||
model_undef = true;
|
||||
cfg.model_undef = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-nogroup") {
|
||||
nogroup = true;
|
||||
cfg.nogroup = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
|
||||
max_seq = atoi(args[++argidx].c_str());
|
||||
cfg.max_seq = atoi(args[++argidx].c_str());
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-set-assumes") {
|
||||
set_assumes = true;
|
||||
cfg.set_assumes = true;
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
|
|
@ -421,7 +489,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 (!nogroup && bit_group.wire)
|
||||
if (!cfg.nogroup && bit_group.wire)
|
||||
bit_group.offset = 0;
|
||||
unproven_equiv_cells[bit_group][bit] = cell;
|
||||
unproven_cells_counter++;
|
||||
|
|
@ -446,15 +514,16 @@ struct EquivSimplePass : public Pass {
|
|||
}
|
||||
|
||||
unproven_equiv_cells.sort();
|
||||
for (auto it : unproven_equiv_cells)
|
||||
for (auto [_, d] : unproven_equiv_cells)
|
||||
{
|
||||
it.second.sort();
|
||||
d.sort();
|
||||
|
||||
vector<Cell*> cells;
|
||||
for (auto it2 : it.second)
|
||||
cells.push_back(it2.second);
|
||||
for (auto [_, cell] : d)
|
||||
cells.push_back(cell);
|
||||
|
||||
EquivSimpleWorker worker(cells, assumes, sigmap, bit2driver, max_seq, short_cones, verbose, model_undef, set_assumes);
|
||||
EquivSimpleWorker::DesignModel model {sigmap, bit2driver};
|
||||
EquivSimpleWorker worker(cells, assumes, model, cfg);
|
||||
success_counter += worker.run();
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue