mirror of https://github.com/YosysHQ/yosys.git
Add fmcombine pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf
parent
b5cf8c9442
commit
370db33a4c
|
|
@ -81,6 +81,27 @@ struct CellTypes
|
|||
}
|
||||
|
||||
void setup_internals()
|
||||
{
|
||||
setup_internals_eval();
|
||||
|
||||
IdString A = "\\A", B = "\\B", EN = "\\EN", Y = "\\Y";
|
||||
|
||||
setup_type("$tribuf", {A, EN}, {Y}, true);
|
||||
|
||||
setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$live", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$fair", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$cover", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$allconst", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$allseq", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$equiv", {A, B}, {Y}, true);
|
||||
}
|
||||
|
||||
void setup_internals_eval()
|
||||
{
|
||||
std::vector<RTLIL::IdString> unary_ops = {
|
||||
"$not", "$pos", "$neg",
|
||||
|
|
@ -111,20 +132,6 @@ struct CellTypes
|
|||
setup_type("$lcu", {P, G, CI}, {CO}, true);
|
||||
setup_type("$alu", {A, B, CI, BI}, {X, Y, CO}, true);
|
||||
setup_type("$fa", {A, B, C}, {X, Y}, true);
|
||||
|
||||
setup_type("$tribuf", {A, EN}, {Y}, true);
|
||||
|
||||
setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$live", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$fair", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$cover", {A, EN}, pool<RTLIL::IdString>(), true);
|
||||
setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$allconst", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$allseq", pool<RTLIL::IdString>(), {Y}, true);
|
||||
setup_type("$equiv", {A, B}, {Y}, true);
|
||||
}
|
||||
|
||||
void setup_internals_mem()
|
||||
|
|
@ -153,6 +160,15 @@ struct CellTypes
|
|||
}
|
||||
|
||||
void setup_stdcells()
|
||||
{
|
||||
setup_stdcells_eval();
|
||||
|
||||
IdString A = "\\A", E = "\\E", Y = "\\Y";
|
||||
|
||||
setup_type("$_TBUF_", {A, E}, {Y}, true);
|
||||
}
|
||||
|
||||
void setup_stdcells_eval()
|
||||
{
|
||||
IdString A = "\\A", B = "\\B", C = "\\C", D = "\\D";
|
||||
IdString E = "\\E", F = "\\F", G = "\\G", H = "\\H";
|
||||
|
|
@ -179,7 +195,6 @@ struct CellTypes
|
|||
setup_type("$_OAI3_", {A, B, C}, {Y}, true);
|
||||
setup_type("$_AOI4_", {A, B, C, D}, {Y}, true);
|
||||
setup_type("$_OAI4_", {A, B, C, D}, {Y}, true);
|
||||
setup_type("$_TBUF_", {A, E}, {Y}, true);
|
||||
}
|
||||
|
||||
void setup_stdcells_mem()
|
||||
|
|
|
|||
|
|
@ -760,7 +760,7 @@ namespace {
|
|||
|
||||
void check()
|
||||
{
|
||||
if (cell->type.substr(0, 1) != "$" || cell->type.substr(0, 3) == "$__" || cell->type.substr(0, 8) == "$paramod" ||
|
||||
if (cell->type.substr(0, 1) != "$" || cell->type.substr(0, 3) == "$__" || cell->type.substr(0, 8) == "$paramod" || cell->type.substr(0,10) == "$fmcombine" ||
|
||||
cell->type.substr(0, 9) == "$verific$" || cell->type.substr(0, 7) == "$array:" || cell->type.substr(0, 8) == "$extern:")
|
||||
return;
|
||||
|
||||
|
|
@ -2360,7 +2360,7 @@ void RTLIL::Cell::check()
|
|||
|
||||
void RTLIL::Cell::fixup_parameters(bool set_a_signed, bool set_b_signed)
|
||||
{
|
||||
if (type.substr(0, 1) != "$" || type.substr(0, 2) == "$_" || type.substr(0, 8) == "$paramod" ||
|
||||
if (type.substr(0, 1) != "$" || type.substr(0, 2) == "$_" || type.substr(0, 8) == "$paramod" || type.substr(0,10) == "$fmcombine" ||
|
||||
type.substr(0, 9) == "$verific$" || type.substr(0, 7) == "$array:" || type.substr(0, 8) == "$extern:")
|
||||
return;
|
||||
|
||||
|
|
|
|||
|
|
@ -9,5 +9,6 @@ OBJS += passes/sat/assertpmux.o
|
|||
OBJS += passes/sat/clk2fflogic.o
|
||||
OBJS += passes/sat/async2sync.o
|
||||
OBJS += passes/sat/supercover.o
|
||||
OBJS += passes/sat/fmcombine.o
|
||||
OBJS += passes/sat/mutate.o
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,292 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/celltypes.h"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct FmcombineWorker
|
||||
{
|
||||
Design *design;
|
||||
Module *original = nullptr;
|
||||
Module *module = nullptr;
|
||||
IdString orig_type, combined_type;
|
||||
|
||||
FmcombineWorker(Design *design, IdString orig_type) :
|
||||
design(design), original(design->module(orig_type)),
|
||||
orig_type(orig_type), combined_type("$fmcombine" + orig_type.str())
|
||||
{
|
||||
}
|
||||
|
||||
SigSpec import_sig(SigSpec sig, const string &suffix)
|
||||
{
|
||||
SigSpec newsig;
|
||||
for (auto chunk : sig.chunks()) {
|
||||
if (chunk.wire != nullptr)
|
||||
chunk.wire = module->wire(chunk.wire->name.str() + suffix);
|
||||
newsig.append(chunk);
|
||||
}
|
||||
return newsig;
|
||||
}
|
||||
|
||||
void import_prim_cell(Cell *cell, const string &suffix)
|
||||
{
|
||||
Cell *c = module->addCell(cell->name.str() + suffix, cell->type);
|
||||
c->parameters = cell->parameters;
|
||||
c->attributes = cell->attributes;
|
||||
|
||||
for (auto &conn : cell->connections())
|
||||
c->setPort(conn.first, import_sig(conn.second, suffix));
|
||||
}
|
||||
|
||||
void import_hier_cell(Cell *cell)
|
||||
{
|
||||
if (!cell->parameters.empty())
|
||||
log_cmd_error("Cell %s.%s has unresolved instance parameters.\n", log_id(original), log_id(cell));
|
||||
|
||||
FmcombineWorker sub_worker(design, cell->type);
|
||||
sub_worker.generate();
|
||||
|
||||
Cell *c = module->addCell(cell->name.str() + "_combined", sub_worker.combined_type);
|
||||
// c->parameters = cell->parameters;
|
||||
c->attributes = cell->attributes;
|
||||
|
||||
for (auto &conn : cell->connections()) {
|
||||
c->setPort(conn.first.str() + "_gold", import_sig(conn.second, "_gold"));
|
||||
c->setPort(conn.first.str() + "_gate", import_sig(conn.second, "_gate"));
|
||||
}
|
||||
}
|
||||
|
||||
void generate()
|
||||
{
|
||||
if (design->module(combined_type)) {
|
||||
// log("Combined module %s already exists.\n", log_id(combined_type));
|
||||
return;
|
||||
}
|
||||
|
||||
log("Generating combined module %s from module %s.\n", log_id(combined_type), log_id(orig_type));
|
||||
module = design->addModule(combined_type);
|
||||
|
||||
for (auto wire : original->wires()) {
|
||||
module->addWire(wire->name.str() + "_gold", wire);
|
||||
module->addWire(wire->name.str() + "_gate", wire);
|
||||
}
|
||||
module->fixup_ports();
|
||||
|
||||
for (auto cell : original->cells()) {
|
||||
if (design->module(cell->type) == nullptr) {
|
||||
import_prim_cell(cell, "_gold");
|
||||
import_prim_cell(cell, "_gate");
|
||||
} else {
|
||||
import_hier_cell(cell);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto &conn : original->connections()) {
|
||||
module->connect(import_sig(conn.first, "_gold"), import_sig(conn.second, "_gold"));
|
||||
module->connect(import_sig(conn.first, "_gate"), import_sig(conn.second, "_gate"));
|
||||
}
|
||||
|
||||
CellTypes ct;
|
||||
ct.setup_internals_eval();
|
||||
ct.setup_stdcells_eval();
|
||||
|
||||
SigMap sigmap(module);
|
||||
|
||||
dict<SigBit, SigBit> data_bit_to_eq_net;
|
||||
dict<Cell*, SigSpec> cell_to_eq_nets;
|
||||
dict<SigSpec, SigSpec> reduce_db;
|
||||
dict<SigSpec, SigSpec> invert_db;
|
||||
|
||||
for (auto cell : original->cells())
|
||||
{
|
||||
if (!ct.cell_known(cell->type))
|
||||
continue;
|
||||
|
||||
for (auto &conn : cell->connections())
|
||||
{
|
||||
if (!cell->output(conn.first))
|
||||
continue;
|
||||
|
||||
SigSpec A = import_sig(conn.second, "_gold");
|
||||
SigSpec B = import_sig(conn.second, "_gate");
|
||||
SigBit EQ = module->Eq(NEW_ID, A, B);
|
||||
|
||||
for (auto bit : sigmap({A, B}))
|
||||
data_bit_to_eq_net[bit] = EQ;
|
||||
|
||||
cell_to_eq_nets[cell].append(EQ);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto cell : original->cells())
|
||||
{
|
||||
if (!ct.cell_known(cell->type))
|
||||
continue;
|
||||
|
||||
bool skip_cell = !cell_to_eq_nets.count(cell);
|
||||
pool<SigBit> src_eq_bits;
|
||||
|
||||
for (auto &conn : cell->connections())
|
||||
{
|
||||
if (skip_cell)
|
||||
break;
|
||||
|
||||
if (cell->output(conn.first))
|
||||
continue;
|
||||
|
||||
SigSpec A = import_sig(conn.second, "_gold");
|
||||
SigSpec B = import_sig(conn.second, "_gate");
|
||||
|
||||
for (auto bit : sigmap({A, B})) {
|
||||
if (data_bit_to_eq_net.count(bit))
|
||||
src_eq_bits.insert(data_bit_to_eq_net.at(bit));
|
||||
else
|
||||
skip_cell = true;
|
||||
}
|
||||
}
|
||||
|
||||
if (!skip_cell) {
|
||||
SigSpec antecedent = SigSpec(src_eq_bits);
|
||||
antecedent.sort_and_unify();
|
||||
|
||||
if (GetSize(antecedent) > 1) {
|
||||
if (reduce_db.count(antecedent) == 0)
|
||||
reduce_db[antecedent] = module->ReduceAnd(NEW_ID, antecedent);
|
||||
antecedent = reduce_db.at(antecedent);
|
||||
}
|
||||
|
||||
SigSpec consequent = cell_to_eq_nets.at(cell);
|
||||
consequent.sort_and_unify();
|
||||
|
||||
if (GetSize(consequent) > 1) {
|
||||
if (reduce_db.count(consequent) == 0)
|
||||
reduce_db[consequent] = module->ReduceAnd(NEW_ID, consequent);
|
||||
consequent = reduce_db.at(consequent);
|
||||
}
|
||||
|
||||
module->addAssume(NEW_ID, consequent, antecedent);
|
||||
|
||||
if (invert_db.count(antecedent) == 0)
|
||||
invert_db[antecedent] = module->Not(NEW_ID, antecedent);
|
||||
|
||||
if (invert_db.count(consequent) == 0)
|
||||
invert_db[consequent] = module->Not(NEW_ID, consequent);
|
||||
|
||||
module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent));
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
struct FmcombinePass : public Pass {
|
||||
FmcombinePass() : Pass("fmcombine", "combine two instances of a cell into one") { }
|
||||
void help() YS_OVERRIDE
|
||||
{
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
log("\n");
|
||||
log(" fmcombine [options] module_name gold_cell gate_cell\n");
|
||||
// log(" fmcombine [options] @gold_cell @gate_cell\n");
|
||||
log("\n");
|
||||
log("This pass takes two cells, which are instances of the same module, and replaces\n");
|
||||
log("them with one instance of a special 'combined' module, that effectively\n");
|
||||
log("contains two copies of the original module, plus some formal properties.\n");
|
||||
log("\n");
|
||||
log("This is useful for formal test benches that check what differences in behavior\n");
|
||||
log("a slight difference in input causes in a module.\n");
|
||||
log("\n");
|
||||
}
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
|
||||
{
|
||||
Module *module = nullptr;
|
||||
Cell *gold_cell = nullptr;
|
||||
Cell *gate_cell = nullptr;
|
||||
|
||||
log_header(design, "Executing FMCOMBINE pass.\n");
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++)
|
||||
{
|
||||
// if (args[argidx] == "-o" && argidx+1 < args.size()) {
|
||||
// filename = args[++argidx];
|
||||
// continue;
|
||||
// }
|
||||
break;
|
||||
}
|
||||
if (argidx+2 == args.size())
|
||||
{
|
||||
string gold_name = args[argidx++];
|
||||
string gate_name = args[argidx++];
|
||||
log_cmd_error("fmcombine @gold_cell @gate_cell call style is not implemented yet.");
|
||||
}
|
||||
else if (argidx+3 == args.size())
|
||||
{
|
||||
IdString module_name = RTLIL::escape_id(args[argidx++]);
|
||||
IdString gold_name = RTLIL::escape_id(args[argidx++]);
|
||||
IdString gate_name = RTLIL::escape_id(args[argidx++]);
|
||||
|
||||
module = design->module(module_name);
|
||||
if (module == nullptr)
|
||||
log_cmd_error("Module %s not found.\n", log_id(module_name));
|
||||
|
||||
gold_cell = module->cell(gold_name);
|
||||
if (gold_cell == nullptr)
|
||||
log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gold_name), log_id(module));
|
||||
|
||||
gate_cell = module->cell(gate_name);
|
||||
if (gate_cell == nullptr)
|
||||
log_cmd_error("Gold cell %s not found in module %s.\n", log_id(gate_name), log_id(module));
|
||||
}
|
||||
else
|
||||
{
|
||||
log_cmd_error("Invalid number of arguments.\n");
|
||||
}
|
||||
// extra_args(args, argidx, design);
|
||||
|
||||
if (gold_cell->type != gate_cell->type)
|
||||
log_cmd_error("Types of gold and gate cells do not match.\n");
|
||||
if (!gold_cell->parameters.empty())
|
||||
log_cmd_error("Gold cell has unresolved instance parameters.\n");
|
||||
if (!gate_cell->parameters.empty())
|
||||
log_cmd_error("Gold cell has unresolved instance parameters.\n");
|
||||
|
||||
FmcombineWorker worker(design, gold_cell->type);
|
||||
worker.generate();
|
||||
IdString combined_cell_name = module->uniquify(stringf("\\%s_%s", log_id(gold_cell), log_id(gate_cell)));
|
||||
|
||||
Cell *cell = module->addCell(combined_cell_name, worker.combined_type);
|
||||
cell->attributes = gold_cell->attributes;
|
||||
cell->add_strpool_attribute("\\src", gate_cell->get_strpool_attribute("\\src"));
|
||||
|
||||
log("Combining cells %s and %s in module %s into new cell %s.\n", log_id(gold_cell), log_id(gate_cell), log_id(module), log_id(cell));
|
||||
|
||||
for (auto &conn : gold_cell->connections())
|
||||
cell->setPort(conn.first.str() + "_gold", conn.second);
|
||||
module->remove(gold_cell);
|
||||
|
||||
for (auto &conn : gate_cell->connections())
|
||||
cell->setPort(conn.first.str() + "_gate", conn.second);
|
||||
module->remove(gate_cell);
|
||||
}
|
||||
} FmcombinePass;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
Loading…
Reference in New Issue