From 370db33a4c347049cb8f66c181d39fd2f2ce5e3a Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 15 Mar 2019 20:18:38 +0100
Subject: Add fmcombine pass
Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
kernel/celltypes.h | 45 +++++---
kernel/rtlil.cc | 4 +-
passes/sat/Makefile.inc | 1 +
passes/sat/fmcombine.cc | 292 ++++++++++++++++++++++++++++++++++++++++++++++++
4 files changed, 325 insertions(+), 17 deletions(-)
create mode 100644 passes/sat/fmcombine.cc
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 8b8a56111..ae88f4aaf 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -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()
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 7f1816190..d0fa88890 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -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;
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index e91df1eb0..4eced2ff1 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -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
diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
new file mode 100644
index 000000000..b8a0e94c8
--- /dev/null
+++ b/passes/sat/fmcombine.cc
@@ -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
--
cgit v1.2.3
From dacaebae35c81b4f4970af3ef8bfdb73691fa215 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 15 Mar 2019 21:45:37 +0100
Subject: Add "fmcombine -fwd -bwd -nop"
Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
passes/sat/fmcombine.cc | 69 ++++++++++++++++++++++++++++++++++++++++++-------
1 file changed, 59 insertions(+), 10 deletions(-)
diff --git a/passes/sat/fmcombine.cc b/passes/sat/fmcombine.cc
index b8a0e94c8..cd75ca860 100644
--- a/passes/sat/fmcombine.cc
+++ b/passes/sat/fmcombine.cc
@@ -24,15 +24,23 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
+struct opts_t
+{
+ bool fwd = false;
+ bool bwd = false;
+ bool nop = false;
+};
+
struct FmcombineWorker
{
+ const opts_t &opts;
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)),
+ FmcombineWorker(Design *design, IdString orig_type, const opts_t &opts) :
+ opts(opts), design(design), original(design->module(orig_type)),
orig_type(orig_type), combined_type("$fmcombine" + orig_type.str())
{
}
@@ -63,7 +71,7 @@ struct FmcombineWorker
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);
+ FmcombineWorker sub_worker(design, cell->type, opts);
sub_worker.generate();
Cell *c = module->addCell(cell->name.str() + "_combined", sub_worker.combined_type);
@@ -106,6 +114,9 @@ struct FmcombineWorker
module->connect(import_sig(conn.first, "_gate"), import_sig(conn.second, "_gate"));
}
+ if (opts.nop)
+ return;
+
CellTypes ct;
ct.setup_internals_eval();
ct.setup_stdcells_eval();
@@ -184,15 +195,19 @@ struct FmcombineWorker
consequent = reduce_db.at(consequent);
}
- module->addAssume(NEW_ID, consequent, antecedent);
+ if (opts.fwd)
+ module->addAssume(NEW_ID, consequent, antecedent);
- if (invert_db.count(antecedent) == 0)
- invert_db[antecedent] = module->Not(NEW_ID, antecedent);
+ if (opts.bwd)
+ {
+ 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);
+ 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));
+ module->addAssume(NEW_ID, invert_db.at(antecedent), invert_db.at(consequent));
+ }
}
}
}
@@ -214,9 +229,25 @@ struct FmcombinePass : public Pass {
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");
+ log(" -fwd\n");
+ log(" Insert forward hint assumptions into the combined module.\n");
+ log("\n");
+ log(" -bwd\n");
+ log(" Insert backward hint assumptions into the combined module.\n");
+ log(" (Backward hints are logically equivalend to fordward hits, but\n");
+ log(" some solvers are faster with bwd hints, or even both -bwd and -fwd.)\n");
+ log("\n");
+ log(" -nop\n");
+ log(" Don't insert hint assumptions into the combined module.\n");
+ log(" (This should not provide any speedup over the original design, but\n");
+ log(" strangely sometimes it does.)\n");
+ log("\n");
+ log("If none of -fwd, -bwd, and -nop is given, then -fwd is used as default.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
+ opts_t opts;
Module *module = nullptr;
Cell *gold_cell = nullptr;
Cell *gate_cell = nullptr;
@@ -230,6 +261,18 @@ struct FmcombinePass : public Pass {
// filename = args[++argidx];
// continue;
// }
+ if (args[argidx] == "-fwd") {
+ opts.fwd = true;
+ continue;
+ }
+ if (args[argidx] == "-bwd") {
+ opts.bwd = true;
+ continue;
+ }
+ if (args[argidx] == "-nop") {
+ opts.nop = true;
+ continue;
+ }
break;
}
if (argidx+2 == args.size())
@@ -262,6 +305,12 @@ struct FmcombinePass : public Pass {
}
// extra_args(args, argidx, design);
+ if (opts.nop && (opts.fwd || opts.bwd))
+ log_cmd_error("Option -nop can not be combined with -fwd and/or -bwd.\n");
+
+ if (!opts.nop && !opts.fwd && !opts.bwd)
+ opts.fwd = true;
+
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())
@@ -269,7 +318,7 @@ struct FmcombinePass : public Pass {
if (!gate_cell->parameters.empty())
log_cmd_error("Gold cell has unresolved instance parameters.\n");
- FmcombineWorker worker(design, gold_cell->type);
+ FmcombineWorker worker(design, gold_cell->type, opts);
worker.generate();
IdString combined_cell_name = module->uniquify(stringf("\\%s_%s", log_id(gold_cell), log_id(gate_cell)));
--
cgit v1.2.3