summaryrefslogtreecommitdiff
path: root/passes/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-01-02 18:11:01 +0100
committerClifford Wolf <clifford@clifford.at>2014-01-02 18:11:01 +0100
commitc6b33f81eb458233be15e1f53882b3684449f3b7 (patch)
tree223b1fc26a69ce7d894ae4d9373380cf96a7163d /passes/sat
parent6dec0e0b3ef3aa42dec4a505896042fe7a2276c6 (diff)
Some cleanups in freduce -inv mode (and switched from -noinv to -inv)
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/freduce.cc55
1 files changed, 29 insertions, 26 deletions
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index 04d9e20d..9f822100 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -30,7 +30,7 @@
namespace {
-bool noinv_mode;
+bool inv_mode;
int verbose_level;
typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
@@ -154,6 +154,7 @@ struct PerformReduction
{
SigMap &sigmap;
drivers_t &drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
ezDefaultSAT ez;
SatGen satgen;
@@ -191,8 +192,8 @@ struct PerformReduction
return sigdepth[out];
}
- PerformReduction(SigMap &sigmap, drivers_t &drivers, std::vector<RTLIL::SigBit> &bits) :
- sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap), out_bits(bits)
+ PerformReduction(SigMap &sigmap, drivers_t &drivers, std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs, std::vector<RTLIL::SigBit> &bits) :
+ sigmap(sigmap), drivers(drivers), inv_pairs(inv_pairs), satgen(&ez, &sigmap), out_bits(bits)
{
satgen.model_undef = true;
@@ -205,15 +206,14 @@ struct PerformReduction
sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
}
- if (noinv_mode) {
- out_inverted = std::vector<bool>(sat_out.size(), false);
- } else {
+ if (inv_mode) {
if (!ez.solve(sat_out, out_inverted, ez.expression(ezSAT::OpAnd, sat_def)))
log_error("Solving for initial model failed!\n");
for (size_t i = 0; i < sat_out.size(); i++)
if (out_inverted.at(i))
sat_out[i] = ez.NOT(sat_out[i]);
- }
+ } else
+ out_inverted = std::vector<bool>(sat_out.size(), false);
}
void analyze(std::vector<std::vector<equiv_bit_t>> &results, std::vector<int> &bucket, int level)
@@ -277,7 +277,14 @@ struct PerformReduction
for (auto &bit : result)
bit.inverted = !bit.inverted;
- results.push_back(result);
+ for (size_t i = 1; i < result.size(); i++) {
+ std::pair<RTLIL::SigBit, RTLIL::SigBit> p(result[0].bit, result[i].bit);
+ if (inv_pairs.count(p) != 0)
+ result.erase(result.begin() + i);
+ }
+
+ if (result.size() > 1)
+ results.push_back(result);
}
}
@@ -296,6 +303,7 @@ struct FreduceHelper
SigMap sigmap;
drivers_t drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> inv_pairs;
FreduceHelper(RTLIL::Module *module) : module(module), sigmap(module)
{
@@ -310,7 +318,7 @@ struct FreduceHelper
ct.setup_stdcells();
std::vector<std::set<RTLIL::SigBit>> batches;
- for (auto &it : module->cells)
+ for (auto &it : module->cells) {
if (ct.cell_known(it.second->type)) {
std::set<RTLIL::SigBit> inputs, outputs;
for (auto &port : it.second->connections) {
@@ -325,6 +333,9 @@ struct FreduceHelper
drivers[bit] = drv;
batches.push_back(outputs);
}
+ if (inv_mode && it.second->type == "$_INV_")
+ inv_pairs.insert(std::pair<RTLIL::SigBit, RTLIL::SigBit>(sigmap(it.second->connections.at("\\A")), sigmap(it.second->connections.at("\\Y"))));
+ }
int bits_count = 0;
std::map<std::vector<RTLIL::SigBit>, std::vector<RTLIL::SigBit>> buckets;
@@ -355,7 +366,7 @@ struct FreduceHelper
bucket_sig.optimize();
log(" Trying to shatter bucket %s%c\n", log_signal(bucket_sig), verbose_level ? ':' : '.');
- PerformReduction worker(sigmap, drivers, bucket.second);
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second);
worker.analyze(equiv);
}
@@ -368,20 +379,12 @@ struct FreduceHelper
RTLIL::SigSpec inv_sig;
for (size_t i = 1; i < grp.size(); i++)
{
- RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
-
- if (grp[i].inverted && drv->type == "$_INV_" && sigmap(drv->connections.at("\\A")) == grp[0].bit) {
- log(" Skipping inverted slave %s: already in reduced form\n", log_signal(grp[i].bit));
- continue;
- }
-
log(" Connect slave%s: %s\n", grp[i].inverted ? " using inverter" : "", log_signal(grp[i].bit));
+ RTLIL::Cell *drv = drivers.at(grp[i].bit).first;
RTLIL::Wire *dummy_wire = module->new_wire(1, NEW_ID);
- for (auto &port : drv->connections) {
- RTLIL::SigSpec mapped = sigmap(port.second);
- mapped.replace(grp[i].bit, dummy_wire, &port.second);
- }
+ for (auto &port : drv->connections)
+ sigmap(port.second).replace(grp[i].bit, dummy_wire, &port.second);
if (grp[i].inverted)
{
@@ -428,14 +431,14 @@ struct FreducePass : public Pass {
log(" -v, -vv\n");
log(" enable verbose or very verbose output\n");
log("\n");
- log(" -noinv\n");
- log(" do not consolidate inverted signals\n");
+ log(" -inv\n");
+ log(" enable explicit handling of inverted signals\n");
log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
verbose_level = 0;
- noinv_mode = false;
+ inv_mode = false;
log_header("Executing FREDUCE pass (perform functional reduction).\n");
@@ -449,8 +452,8 @@ struct FreducePass : public Pass {
verbose_level = 2;
continue;
}
- if (args[argidx] == "-noinv") {
- noinv_mode = true;
+ if (args[argidx] == "-inv") {
+ inv_mode = true;
continue;
}
break;