aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/setundef.cc22
-rw-r--r--passes/memory/memory_bram.cc48
-rw-r--r--passes/memory/memory_map.cc119
-rw-r--r--passes/opt/opt_clean.cc6
-rw-r--r--passes/opt/opt_expr.cc162
-rw-r--r--passes/sat/Makefile.inc1
-rw-r--r--passes/sat/qbfsat.cc550
-rw-r--r--passes/techmap/Makefile.inc7
-rw-r--r--passes/techmap/abc.cc10
-rw-r--r--passes/techmap/abc9.cc4
-rw-r--r--passes/techmap/abc9_exe.cc12
-rw-r--r--passes/techmap/abc9_ops.cc3
-rw-r--r--passes/techmap/dffinit.cc8
-rw-r--r--passes/techmap/dffsr2dff.cc213
-rw-r--r--passes/techmap/techmap.cc2
-rw-r--r--passes/techmap/zinit.cc72
16 files changed, 942 insertions, 297 deletions
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index 2556d188a..8d973869e 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -149,7 +149,7 @@ struct SetundefPass : public Pass {
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
- bool got_value = false;
+ int got_value = 0;
bool undriven_mode = false;
bool expose_mode = false;
bool init_mode = false;
@@ -170,31 +170,31 @@ struct SetundefPass : public Pass {
continue;
}
if (args[argidx] == "-zero") {
- got_value = true;
+ got_value++;
worker.next_bit_mode = MODE_ZERO;
worker.next_bit_state = 0;
continue;
}
if (args[argidx] == "-one") {
- got_value = true;
+ got_value++;
worker.next_bit_mode = MODE_ONE;
worker.next_bit_state = 0;
continue;
}
if (args[argidx] == "-anyseq") {
- got_value = true;
+ got_value++;
worker.next_bit_mode = MODE_ANYSEQ;
worker.next_bit_state = 0;
continue;
}
if (args[argidx] == "-anyconst") {
- got_value = true;
+ got_value++;
worker.next_bit_mode = MODE_ANYCONST;
worker.next_bit_state = 0;
continue;
}
if (args[argidx] == "-undef") {
- got_value = true;
+ got_value++;
worker.next_bit_mode = MODE_UNDEF;
worker.next_bit_state = 0;
continue;
@@ -207,8 +207,8 @@ struct SetundefPass : public Pass {
params_mode = true;
continue;
}
- if (args[argidx] == "-random" && !got_value && argidx+1 < args.size()) {
- got_value = true;
+ if (args[argidx] == "-random" && argidx+1 < args.size()) {
+ got_value++;
worker.next_bit_mode = MODE_RANDOM;
worker.next_bit_state = atoi(args[++argidx].c_str()) + 1;
for (int i = 0; i < 10; i++)
@@ -221,7 +221,7 @@ struct SetundefPass : public Pass {
if (!got_value && expose_mode) {
log("Using default as -undef with -expose.\n");
- got_value = true;
+ got_value++;
worker.next_bit_mode = MODE_UNDEF;
worker.next_bit_state = 0;
}
@@ -229,7 +229,9 @@ struct SetundefPass : public Pass {
if (expose_mode && !undriven_mode)
log_cmd_error("Option -expose must be used with option -undriven.\n");
if (!got_value)
- log_cmd_error("One of the options -zero, -one, -anyseq, -anyconst, or -random <seed> must be specified.\n");
+ log_cmd_error("One of the options -zero, -one, -anyseq, -anyconst, -random <seed>, or -expose must be specified.\n");
+ else if (got_value > 1)
+ log_cmd_error("Only one of the options -zero, -one, -anyseq, -anyconst, or -random <seed> can be specified.\n");
if (init_mode && (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST))
log_cmd_error("The options -init and -anyseq / -anyconst are exclusive.\n");
diff --git a/passes/memory/memory_bram.cc b/passes/memory/memory_bram.cc
index 52ee1e99d..0898ec288 100644
--- a/passes/memory/memory_bram.cc
+++ b/passes/memory/memory_bram.cc
@@ -137,9 +137,26 @@ struct rules_t
vector<vector<std::tuple<bool,IdString,Const>>> attributes;
};
+ bool attr_icase;
dict<IdString, vector<bram_t>> brams;
vector<match_t> matches;
+ std::string map_case(std::string value) const
+ {
+ if (attr_icase) {
+ for (char &c : value)
+ c = tolower(c);
+ }
+ return value;
+ }
+
+ RTLIL::Const map_case(RTLIL::Const value) const
+ {
+ if (value.flags & RTLIL::CONST_FLAG_STRING)
+ return map_case(value.decode_string());
+ return value;
+ }
+
std::ifstream infile;
vector<string> tokens;
vector<string> labels;
@@ -337,7 +354,7 @@ struct rules_t
IdString key = RTLIL::escape_id(tokens[idx].substr(c1, c2));
Const val = c2 != std::string::npos ? tokens[idx].substr(c2+1) : RTLIL::Const(1);
- data.attributes.back().emplace_back(exists, key, val);
+ data.attributes.back().emplace_back(exists, key, map_case(val));
}
continue;
}
@@ -351,6 +368,7 @@ struct rules_t
rewrite_filename(filename);
infile.open(filename);
linecount = 0;
+ attr_icase = false;
if (infile.fail())
log_error("Can't open rules file `%s'.\n", filename.c_str());
@@ -360,6 +378,11 @@ struct rules_t
if (!labels.empty())
syntax_error();
+ if (GetSize(tokens) == 2 && tokens[0] == "attr_icase") {
+ attr_icase = atoi(tokens[1].c_str());
+ continue;
+ }
+
if (tokens[0] == "bram") {
parse_bram();
continue;
@@ -843,7 +866,7 @@ grow_read_ports:;
}
else if (!exists)
continue;
- if (it->second != value)
+ if (rules.map_case(it->second) != value)
continue;
found = true;
break;
@@ -855,7 +878,7 @@ grow_read_ports:;
ss << "!";
IdString key = std::get<1>(sums.front());
ss << log_id(key);
- const Const &value = std::get<2>(sums.front());
+ const Const &value = rules.map_case(std::get<2>(sums.front()));
if (exists && value != Const(1))
ss << "=\"" << value.decode_string() << "\"";
@@ -1079,9 +1102,6 @@ void handle_cell(Cell *cell, const rules_t &rules)
auto &bram = rules.brams.at(match.name).at(vi);
bool or_next_if_better = match.or_next_if_better || vi+1 < GetSize(rules.brams.at(match.name));
- if (failed_brams.count(pair<IdString, int>(bram.name, bram.variant)))
- continue;
-
int avail_rd_ports = 0;
int avail_wr_ports = 0;
for (int j = 0; j < bram.groups; j++) {
@@ -1117,6 +1137,9 @@ void handle_cell(Cell *cell, const rules_t &rules)
int efficiency = (100 * match_properties["bits"]) / (dups * cells * bram.dbits * (1 << bram.abits));
match_properties["efficiency"] = efficiency;
+ if (failed_brams.count(pair<IdString, int>(bram.name, bram.variant)))
+ goto next_match_rule;
+
log(" Metrics for %s: awaste=%d dwaste=%d bwaste=%d waste=%d efficiency=%d\n",
log_id(match.name), awaste, dwaste, bwaste, waste, efficiency);
@@ -1167,7 +1190,7 @@ void handle_cell(Cell *cell, const rules_t &rules)
}
else if (!exists)
continue;
- if (it->second != value)
+ if (rules.map_case(it->second) != value)
continue;
found = true;
break;
@@ -1179,7 +1202,7 @@ void handle_cell(Cell *cell, const rules_t &rules)
ss << "!";
IdString key = std::get<1>(sums.front());
ss << log_id(key);
- const Const &value = std::get<2>(sums.front());
+ const Const &value = rules.map_case(std::get<2>(sums.front()));
if (exists && value != Const(1))
ss << "=\"" << value.decode_string() << "\"";
@@ -1252,8 +1275,13 @@ struct MemoryBramPass : public Pass {
log("The given rules file describes the available resources and how they should be\n");
log("used.\n");
log("\n");
- log("The rules file contains a set of block ram description and a sequence of match\n");
- log("rules. A block ram description looks like this:\n");
+ log("The rules file contains configuration options, a set of block ram description\n");
+ log("and a sequence of match rules.\n");
+ log("\n");
+ log("The option 'attr_icase' configures how attribute values are matched. The value 0\n");
+ log("means case-sensitive, 1 means case-insensitive.\n");
+ log("\n");
+ log("A block ram description looks like this:\n");
log("\n");
log(" bram RAMB1024X32 # name of BRAM cell\n");
log(" init 1 # set to '1' if BRAM can be initialized\n");
diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc
index da0673c8f..9d455f55b 100644
--- a/passes/memory/memory_map.cc
+++ b/passes/memory/memory_map.cc
@@ -28,11 +28,32 @@ PRIVATE_NAMESPACE_BEGIN
struct MemoryMapWorker
{
+ bool attr_icase = false;
+ dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
+
RTLIL::Design *design;
RTLIL::Module *module;
std::map<std::pair<RTLIL::SigSpec, RTLIL::SigSpec>, RTLIL::SigBit> decoder_cache;
+ MemoryMapWorker(RTLIL::Design *design, RTLIL::Module *module) : design(design), module(module) {}
+
+ std::string map_case(std::string value) const
+ {
+ if (attr_icase) {
+ for (char &c : value)
+ c = tolower(c);
+ }
+ return value;
+ }
+
+ RTLIL::Const map_case(RTLIL::Const value) const
+ {
+ if (value.flags & RTLIL::CONST_FLAG_STRING)
+ return map_case(value.decode_string());
+ return value;
+ }
+
std::string genid(RTLIL::IdString name, std::string token1 = "", int i = -1, std::string token2 = "", int j = -1, std::string token3 = "", int k = -1, std::string token4 = "")
{
std::stringstream sstr;
@@ -98,6 +119,36 @@ struct MemoryMapWorker
return;
}
+ // check if attributes allow us to infer FFRAM for this cell
+ for (const auto &attr : attributes) {
+ if (cell->attributes.count(attr.first)) {
+ const auto &cell_attr = cell->attributes[attr.first];
+ if (attr.second.empty()) {
+ log("Not mapping memory cell %s in module %s (attribute %s is set).\n",
+ cell->name.c_str(), module->name.c_str(), attr.first.c_str());
+ return;
+ }
+
+ bool found = false;
+ for (auto &value : attr.second) {
+ if (map_case(cell_attr) == map_case(value)) {
+ found = true;
+ break;
+ }
+ }
+ if (!found) {
+ if (cell_attr.flags & RTLIL::CONST_FLAG_STRING) {
+ log("Not mapping memory cell %s in module %s (attribute %s is set to \"%s\").\n",
+ cell->name.c_str(), module->name.c_str(), attr.first.c_str(), cell_attr.decode_string().c_str());
+ } else {
+ log("Not mapping memory cell %s in module %s (attribute %s is set to %d).\n",
+ cell->name.c_str(), module->name.c_str(), attr.first.c_str(), cell_attr.as_int());
+ }
+ return;
+ }
+ }
+ }
+
// all write ports must share the same clock
RTLIL::SigSpec clocks = cell->getPort(ID::WR_CLK);
RTLIL::Const clocks_pol = cell->parameters[ID::WR_CLK_POLARITY];
@@ -339,7 +390,7 @@ struct MemoryMapWorker
module->remove(cell);
}
- MemoryMapWorker(RTLIL::Design *design, RTLIL::Module *module) : design(design), module(module)
+ void run()
{
std::vector<RTLIL::Cell*> cells;
for (auto cell : module->selected_cells())
@@ -356,17 +407,73 @@ struct MemoryMapPass : public Pass {
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" memory_map [selection]\n");
+ log(" memory_map [options] [selection]\n");
log("\n");
log("This pass converts multiport memory cells as generated by the memory_collect\n");
log("pass to word-wide DFFs and address decoders.\n");
log("\n");
+ log(" -attr !<name>\n");
+ log(" do not map memories that have attribute <name> set.\n");
+ log("\n");
+ log(" -attr <name>[=<value>]\n");
+ log(" for memories that have attribute <name> set, only map them if its value\n");
+ log(" is a string <value> (if specified), or an integer 1 (otherwise). if this\n");
+ log(" option is specified multiple times, map the memory if the attribute is\n");
+ log(" to any of the values.\n");
+ log("\n");
+ log(" -iattr\n");
+ log(" for -attr, ignore case of <value>.\n");
+ log("\n");
}
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE {
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ bool attr_icase = false;
+ dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
+
log_header(design, "Executing MEMORY_MAP pass (converting $mem cells to logic and flip-flops).\n");
- extra_args(args, 1, design);
- for (auto mod : design->selected_modules())
- MemoryMapWorker(design, mod);
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-attr" && argidx + 1 < args.size())
+ {
+ std::string attr_arg = args[++argidx];
+ std::string name;
+ RTLIL::Const value;
+ size_t eq_at = attr_arg.find('=');
+ if (eq_at != std::string::npos) {
+ name = attr_arg.substr(0, eq_at);
+ value = attr_arg.substr(eq_at + 1);
+ } else {
+ name = attr_arg;
+ value = RTLIL::Const(1);
+ }
+ if (attr_arg.size() > 1 && attr_arg[0] == '!') {
+ if (value != RTLIL::Const(1)) {
+ --argidx;
+ break; // we don't support -attr !<name>=<value>
+ }
+ attributes[RTLIL::escape_id(name.substr(1))].clear();
+ } else {
+ attributes[RTLIL::escape_id(name)].push_back(value);
+ }
+ continue;
+ }
+ if (args[argidx] == "-iattr")
+ {
+ attr_icase = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ for (auto mod : design->selected_modules()) {
+ MemoryMapWorker worker(design, mod);
+ worker.attr_icase = attr_icase;
+ worker.attributes = attributes;
+ worker.run();
+ }
}
} MemoryMapPass;
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index da3961218..6271376f1 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -406,6 +406,9 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
if (verbose && del_temp_wires_count)
log_debug(" removed %d unused temporary wires.\n", del_temp_wires_count);
+ if (!del_wires_queue.empty())
+ module->design->scratchpad_set_bool("opt.did_something", true);
+
return !del_wires_queue.empty();
}
@@ -476,6 +479,9 @@ bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose)
next_wire:;
}
+ if (did_something)
+ module->design->scratchpad_set_bool("opt.did_something", true);
+
return did_something;
}
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index 1a4dd9239..3229dd1b2 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -717,31 +717,27 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
RTLIL::SigSpec sig_y = cell->getPort(ID::Y);
RTLIL::SigSpec sig_co = cell->getPort(ID::CO);
- bool sub = (sig_ci == State::S1 && sig_bi == State::S1);
+ if (sig_bi != State::S0 && sig_bi != State::S1)
+ goto skip_fine_alu;
+ if (sig_ci != State::S0 && sig_ci != State::S1)
+ goto skip_fine_alu;
- // If not a subtraction, yet there is a carry or B is inverted
- // then no optimisation is possible as carry will not be constant
- if (!sub && (sig_ci != State::S0 || sig_bi != State::S0))
- goto next_cell;
+ bool bi = sig_bi == State::S1;
+ bool ci = sig_ci == State::S1;
int i;
for (i = 0; i < GetSize(sig_y); i++) {
RTLIL::SigBit b = sig_b.at(i, State::Sx);
RTLIL::SigBit a = sig_a.at(i, State::Sx);
- if (b == State::S0 && a != State::Sx) {
- module->connect(sig_y[i], sig_a[i]);
- module->connect(sig_x[i], sub ? module->Not(NEW_ID, a).as_bit() : a);
- module->connect(sig_co[i], sub ? State::S1 : State::S0);
- }
- else if (sub && b == State::S1 && a == State::S1) {
- module->connect(sig_y[i], State::S0);
- module->connect(sig_x[i], module->Not(NEW_ID, a));
- module->connect(sig_co[i], State::S0);
+ if (b == ((bi ^ ci) ? State::S1 : State::S0) && a != State::Sx) {
+ module->connect(sig_y[i], a);
+ module->connect(sig_x[i], ci ? module->Not(NEW_ID, a).as_bit() : a);
+ module->connect(sig_co[i], ci ? State::S1 : State::S0);
}
- else if (!sub && a == State::S0 && b != State::Sx) {
- module->connect(sig_y[i], b);
- module->connect(sig_x[i], b);
- module->connect(sig_co[i], State::S0);
+ else if (a == (ci ? State::S1 : State::S0) && b != State::Sx) {
+ module->connect(sig_y[i], bi ? module->Not(NEW_ID, b).as_bit() : b);
+ module->connect(sig_x[i], (bi ^ ci) ? module->Not(NEW_ID, b).as_bit() : b);
+ module->connect(sig_co[i], ci ? State::S1 : State::S0);
}
else
break;
@@ -758,6 +754,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
}
}
}
+skip_fine_alu:
if (cell->type.in(ID($reduce_xor), ID($reduce_xnor), ID($shift), ID($shiftx), ID($shl), ID($shr), ID($sshl), ID($sshr),
ID($lt), ID($le), ID($ge), ID($gt), ID($neg), ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($pow)))
@@ -1089,7 +1086,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
// If not a subtraction, yet there is a carry or B is inverted
// then no optimisation is possible as carry will not be constant
if (!sub && (sig_ci != State::S0 || sig_bi != State::S0))
- goto next_cell;
+ goto skip_identity;
}
if (!sub && a.is_fully_const() && a.as_bool() == false)
@@ -1163,6 +1160,7 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
goto next_cell;
}
}
+skip_identity:
if (mux_bool && cell->type.in(ID($mux), ID($_MUX_)) &&
cell->getPort(ID::A) == State::S0 && cell->getPort(ID::B) == State::S1) {
@@ -1426,6 +1424,39 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
goto next_cell;
}
}
+
+ sig_a = assign_map(cell->getPort(ID::A));
+ sig_b = assign_map(cell->getPort(ID::B));
+ int a_zeros, b_zeros;
+ for (a_zeros = 0; a_zeros < GetSize(sig_a); a_zeros++)
+ if (sig_a[a_zeros] != RTLIL::State::S0)
+ break;
+ for (b_zeros = 0; b_zeros < GetSize(sig_b); b_zeros++)
+ if (sig_b[b_zeros] != RTLIL::State::S0)
+ break;
+ if (a_zeros || b_zeros) {
+ int y_zeros = a_zeros + b_zeros;
+ cover("opt.opt_expr.mul_low_zeros");
+
+ log_debug("Removing low %d A and %d B bits from cell `%s' in module `%s'.\n",
+ a_zeros, b_zeros, cell->name.c_str(), module->name.c_str());
+
+ if (a_zeros) {
+ cell->setPort(ID::A, sig_a.extract_end(a_zeros));
+ cell->parameters[ID::A_WIDTH] = GetSize(sig_a) - a_zeros;
+ }
+ if (b_zeros) {
+ cell->setPort(ID::B, sig_b.extract_end(b_zeros));
+ cell->parameters[ID::B_WIDTH] = GetSize(sig_b) - b_zeros;
+ }
+ cell->setPort(ID::Y, sig_y.extract_end(y_zeros));
+ cell->parameters[ID::Y_WIDTH] = GetSize(sig_y) - y_zeros;
+ module->connect(RTLIL::SigSig(sig_y.extract(0, y_zeros), RTLIL::SigSpec(0, y_zeros)));
+ cell->check();
+
+ did_something = true;
+ goto next_cell;
+ }
}
if (!keepdc && cell->type.in(ID($div), ID($mod)))
@@ -1497,6 +1528,99 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
}
}
+ // Find places in $alu cell where the carry is constant, and split it at these points.
+ if (do_fine && !keepdc && cell->type == ID($alu))
+ {
+ bool a_signed = cell->parameters[ID::A_SIGNED].as_bool();
+ bool b_signed = cell->parameters[ID::B_SIGNED].as_bool();
+ bool is_signed = a_signed && b_signed;
+
+ RTLIL::SigSpec sig_a = assign_map(cell->getPort(ID::A));
+ RTLIL::SigSpec sig_b = assign_map(cell->getPort(ID::B));
+ RTLIL::SigSpec sig_y = assign_map(cell->getPort(ID::Y));
+ RTLIL::SigSpec sig_bi = assign_map(cell->getPort(ID::BI));
+ if (GetSize(sig_a) == 0)
+ sig_a = State::S0;
+ if (GetSize(sig_b) == 0)
+ sig_b = State::S0;
+ sig_a.extend_u0(GetSize(sig_y), is_signed);
+ sig_b.extend_u0(GetSize(sig_y), is_signed);
+
+ if (sig_bi != State::S0 && sig_bi != State::S1)
+ goto skip_alu_split;
+
+ std::vector<std::pair<int, State>> split_points;
+
+ for (int i = 0; i < GetSize(sig_y); i++) {
+ SigBit bit_a = sig_a[i];
+ SigBit bit_b = sig_b[i];
+ if (bit_a != State::S0 && bit_a != State::S1)
+ continue;
+ if (bit_b != State::S0 && bit_b != State::S1)
+ continue;
+ if (sig_bi == State::S1) {
+ if (bit_b == State::S0)
+ bit_b = State::S1;
+ else
+ bit_b = State::S0;
+ }
+ if (bit_a != bit_b)
+ continue;
+ split_points.push_back(std::make_pair(i + 1, bit_a.data));
+ }
+
+ if (split_points.empty() || split_points[0].first == GetSize(sig_y))
+ goto skip_alu_split;
+
+ for (auto &p : split_points)
+ log_debug("Splitting $alu cell `%s' in module `%s' at const-carry point %d.\n",
+ cell->name.c_str(), module->name.c_str(), p.first);
+
+ if (split_points.back().first != GetSize(sig_y))
+ split_points.push_back(std::make_pair(GetSize(sig_y), State::Sx));
+
+ RTLIL::SigSpec sig_ci = assign_map(cell->getPort(ID::CI));
+ int prev = 0;
+ RTLIL::SigSpec sig_x = assign_map(cell->getPort(ID::X));
+ RTLIL::SigSpec sig_co = assign_map(cell->getPort(ID::CO));
+
+ for (auto &p : split_points) {
+ int cur = p.first;
+ int sz = cur - prev;
+ bool last = cur == GetSize(sig_y);
+
+ RTLIL::Cell *c = module->addCell(NEW_ID, cell->type);
+ c->setPort(ID::A, sig_a.extract(prev, sz));
+ c->setPort(ID::B, sig_b.extract(prev, sz));
+ c->setPort(ID::BI, sig_bi);
+ c->setPort(ID::CI, sig_ci);
+ c->setPort(ID::Y, sig_y.extract(prev, sz));
+ c->setPort(ID::X, sig_x.extract(prev, sz));
+ RTLIL::SigSpec new_co = sig_co.extract(prev, sz);
+ if (p.second != State::Sx) {
+ module->connect(new_co[sz-1], p.second);
+ RTLIL::Wire *dummy = module->addWire(NEW_ID);
+ new_co[sz-1] = dummy;
+ }
+ c->setPort(ID::CO, new_co);
+ c->parameters[ID::A_WIDTH] = sz;
+ c->parameters[ID::B_WIDTH] = sz;
+ c->parameters[ID::Y_WIDTH] = sz;
+ c->parameters[ID::A_SIGNED] = last ? a_signed : false;
+ c->parameters[ID::B_SIGNED] = last ? b_signed : false;
+
+ prev = p.first;
+ sig_ci = p.second;
+ }
+
+ cover("opt.opt_expr.alu_split");
+ module->remove(cell);
+
+ did_something = true;
+ goto next_cell;
+ }
+skip_alu_split:
+
// remove redundant pairs of bits in ==, ===, !=, and !==
// replace cell with const driver if inputs can't be equal
if (do_fine && cell->type.in(ID($eq), ID($ne), ID($eqx), ID($nex)))
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index 4bb4b0edc..a928c57de 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -13,4 +13,5 @@ OBJS += passes/sat/fmcombine.o
OBJS += passes/sat/mutate.o
OBJS += passes/sat/cutpoint.o
OBJS += passes/sat/fminit.o
+OBJS += passes/sat/qbfsat.o
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
new file mode 100644
index 000000000..44691425f
--- /dev/null
+++ b/passes/sat/qbfsat.cc
@@ -0,0 +1,550 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2020 Alberto Gonzalez <boqwxp@airmail.cc>
+ *
+ * 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/celltypes.h"
+#include "kernel/log.h"
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include <cstdio>
+#include <algorithm>
+
+#if defined(_WIN32)
+# define WIFEXITED(x) 1
+# define WIFSIGNALED(x) 0
+# define WIFSTOPPED(x) 0
+# define WEXITSTATUS(x) ((x) & 0xff)
+# define WTERMSIG(x) SIGTERM
+#else
+# include <sys/wait.h>
+#endif
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct QbfSolutionType {
+ std::vector<std::string> stdout;
+ dict<std::string, std::string> hole_to_value;
+ bool sat;
+ bool unknown; //true if neither 'sat' nor 'unsat'
+ bool success; //true if exit code 0
+
+ QbfSolutionType() : sat(false), unknown(true), success(false) {}
+};
+
+struct QbfSolveOptions {
+ bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs;
+ bool sat, unsat, show_smtbmc;
+ std::string specialize_soln_file;
+ std::string write_soln_soln_file;
+ std::string dump_final_smt2_file;
+ size_t argidx;
+ QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
+ nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false),
+ show_smtbmc(false), argidx(0) {};
+};
+
+void recover_solution(QbfSolutionType &sol) {
+ YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
+ YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
+ YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
+#ifndef NDEBUG
+ YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
+ YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
+#endif
+ YS_REGEX_MATCH_TYPE m;
+ bool sat_regex_found = false;
+ bool unsat_regex_found = false;
+ dict<std::string, bool> hole_value_recovered;
+ for (const std::string &x : sol.stdout) {
+ if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
+ std::string loc = m[1].str();
+ std::string val = m[2].str();
+#ifndef NDEBUG
+ log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
+ log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
+#endif
+ sol.hole_to_value[loc] = val;
+ }
+ else if (YS_REGEX_NS::regex_search(x, sat_regex))
+ sat_regex_found = true;
+ else if (YS_REGEX_NS::regex_search(x, unsat_regex))
+ unsat_regex_found = true;
+ }
+#ifndef NDEBUG
+ log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
+ log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
+#endif
+}
+
+dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) {
+ dict<std::string, std::string> hole_loc_to_name;
+ for (auto cell : module->cells()) {
+ std::string cell_src = cell->get_src_attribute();
+ auto pos = sol.hole_to_value.find(cell_src);
+ if (pos != sol.hole_to_value.end()) {
+#ifndef NDEBUG
+ log_assert(cell->type.in("$anyconst", "$anyseq"));
+ log_assert(cell->getPort(ID::Y).is_wire());
+#endif
+ hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str();
+ }
+ }
+
+ return hole_loc_to_name;
+}
+
+void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) {
+ std::ofstream fout(file.c_str());
+ if (!fout)
+ log_cmd_error("could not open solution file for writing.\n");
+
+ dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
+ for(auto &x : sol.hole_to_value)
+ fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl;
+}
+
+void specialize_from_file(RTLIL::Module *module, const std::string &file) {
+ YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$");
+ YS_REGEX_MATCH_TYPE m;
+ pool<RTLIL::Cell *> anyconsts_to_remove;
+ dict<std::string, std::string> hole_name_to_value;
+ std::ifstream fin(file.c_str());
+ if (!fin)
+ log_cmd_error("could not read solution file.\n");
+
+ std::string buf;
+ while (std::getline(fin, buf)) {
+ log_assert(YS_REGEX_NS::regex_search(buf, m, hole_assn_regex));
+ std::string hole_name = m[1].str();
+ std::string hole_value = m[2].str();
+ hole_name_to_value[hole_name] = hole_value;
+ }
+
+ for (auto cell : module->cells())
+ if (cell->type == "$anyconst") {
+ auto anyconst_port_y = cell->getPort(ID::Y).as_wire();
+ if (anyconst_port_y == nullptr)
+ continue;
+ if (hole_name_to_value.find(anyconst_port_y->name.str()) != hole_name_to_value.end())
+ anyconsts_to_remove.insert(cell);
+ }
+ for (auto cell : anyconsts_to_remove)
+ module->remove(cell);
+
+ for (auto &it : hole_name_to_value) {
+ std::string hole_name = it.first;
+ std::string hole_value = it.second;
+ RTLIL::Wire *wire = module->wire(hole_name);
+#ifndef NDEBUG
+ log_assert(wire != nullptr);
+ log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
+#endif
+
+ log("Specializing %s from file with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
+ std::vector<RTLIL::SigBit> value_bv;
+ value_bv.reserve(wire->width);
+ for (char c : hole_value)
+ value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
+ std::reverse(value_bv.begin(), value_bv.end());
+ module->connect(wire, value_bv);
+ }
+}
+
+void specialize(RTLIL::Module *module, const QbfSolutionType &sol) {
+ dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
+ pool<RTLIL::Cell *> anyconsts_to_remove;
+ for (auto cell : module->cells())
+ if (cell->type == "$anyconst")
+ if (hole_loc_to_name.find(cell->get_src_attribute()) != hole_loc_to_name.end())
+ anyconsts_to_remove.insert(cell);
+ for (auto cell : anyconsts_to_remove)
+ module->remove(cell);
+ for (auto &it : sol.hole_to_value) {
+ std::string hole_loc = it.first;
+ std::string hole_value = it.second;
+
+#ifndef NDEBUG
+ auto pos = hole_loc_to_name.find(hole_loc);
+ log_assert(pos != hole_loc_to_name.end());
+#endif
+
+ std::string hole_name = hole_loc_to_name[hole_loc];
+ RTLIL::Wire *wire = module->wire(hole_name);
+#ifndef NDEBUG
+ log_assert(wire != nullptr);
+ log_assert(wire->width > 0 && GetSize(hole_value) == wire->width);
+#endif
+
+ log("Specializing %s with %s = %d'b%s.\n", module->name.c_str(), hole_name.c_str(), wire->width, hole_value.c_str());
+ std::vector<RTLIL::SigBit> value_bv;
+ value_bv.reserve(wire->width);
+ for (char c : hole_value)
+ value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
+ std::reverse(value_bv.begin(), value_bv.end());
+ module->connect(wire, value_bv);
+ }
+}
+
+void dump_model(RTLIL::Module *module, const QbfSolutionType &sol) {
+ log("Satisfiable model:\n");
+ dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
+ for (auto &it : sol.hole_to_value) {
+ std::string hole_loc = it.first;
+ std::string hole_value = it.second;
+
+#ifndef NDEBUG
+ auto pos = hole_loc_to_name.find(hole_loc);
+ log_assert(pos != hole_loc_to_name.end());
+#endif
+
+ std::string hole_name = hole_loc_to_name[hole_loc];
+ log("\t%s = %lu'b%s\n", hole_name.c_str(), hole_value.size(), hole_value.c_str());
+ std::vector<RTLIL::SigBit> value_bv;
+ value_bv.reserve(hole_value.size());
+ for (char c : hole_value)
+ value_bv.emplace_back(c == '1'? RTLIL::S1 : RTLIL::S0);
+ std::reverse(value_bv.begin(), value_bv.end());
+ }
+
+}
+
+void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wires) {
+ for (auto &n : input_wires) {
+ RTLIL::Wire *input = module->wire(n);
+#ifndef NDEBUG
+ log_assert(input != nullptr);
+#endif
+
+ RTLIL::Cell *allconst = module->addCell("$allconst$" + n, "$allconst");
+ allconst->setParam(ID(WIDTH), input->width);
+ allconst->setPort(ID::Y, input);
+ allconst->set_src_attribute(input->get_src_attribute());
+ input->port_input = false;
+ log("Replaced input %s with $allconst cell.\n", n.c_str());
+ }
+ module->fixup_ports();
+}
+
+void assume_miter_outputs(RTLIL::Module *module) {
+ std::vector<RTLIL::Wire *> wires_to_assume;
+ for (auto w : module->wires())
+ if (w->port_output && w->width == 1)
+ wires_to_assume.push_back(w);
+
+ if (wires_to_assume.size() == 0)
+ return;
+ else {
+ log("Adding $assume cell for output(s): ");
+ for (auto w : wires_to_assume)
+ log("\"%s\" ", w->name.c_str());
+ log("\n");
+ }
+
+ for(auto i = 0; wires_to_assume.size() > 1; ++i) {
+ std::vector<RTLIL::Wire *> buf;
+ for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) {
+ std::stringstream strstr; strstr << i << "_" << j;
+ RTLIL::Wire *and_wire = module->addWire("\\_qbfsat_and_" + strstr.str(), 1);
+ module->addLogicAnd("$_qbfsat_and_" + strstr.str(), wires_to_assume[j], wires_to_assume[j+1], and_wire, false, wires_to_assume[j]->get_src_attribute());
+ buf.push_back(and_wire);
+ }
+ if (wires_to_assume.size() % 2 == 1)
+ buf.push_back(wires_to_assume[wires_to_assume.size() - 1]);
+ wires_to_assume.swap(buf);
+ }
+
+#ifndef NDEBUG
+ log_assert(wires_to_assume.size() == 1);
+#endif
+ module->addAssume("$assume_qbfsat_miter_outputs", wires_to_assume[0], RTLIL::S1);
+}
+
+QbfSolutionType qbf_solve(RTLIL::Module *mod, const QbfSolveOptions &opt) {
+ QbfSolutionType ret;
+ const std::string yosys_smtbmc_exe = proc_self_dirname() + "yosys-smtbmc";
+ const std::string smtbmc_warning = "z3: WARNING:";
+ const bool show_smtbmc = opt.show_smtbmc;
+
+ const std::string tempdir_name = make_temp_dir("/tmp/yosys-z3-XXXXXX");
+ const std::string smt2_command = "write_smt2 -stbv -wires " + tempdir_name + "/problem.smt2";
+#ifndef NDEBUG
+ log_assert(mod->design != nullptr);
+#endif
+ Pass::call(mod->design, smt2_command);
+ log_header(mod->design, "Solving QBF-SAT problem.\n");
+
+ //Execute and capture stdout from `yosys-smtbmc -s z3 -t 1 -g --binary [--dump-smt2 <file>]`
+ {
+ const std::string cmd = yosys_smtbmc_exe + " -s z3 -t 1 -g --binary " + (opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file + " " : "") + tempdir_name + "/problem.smt2 2>&1";
+ auto process_line = [&ret, &smtbmc_warning, &show_smtbmc](const std::string &line) {
+ ret.stdout.push_back(line.substr(0, line.size()-1)); //don't include trailing newline
+ auto warning_pos = line.find(smtbmc_warning);
+ if (warning_pos != std::string::npos)
+ log_warning("%s", line.substr(warning_pos + smtbmc_warning.size() + 1).c_str());
+ else
+ if (show_smtbmc)
+ log("smtbmc output: %s", line.c_str());
+ };
+
+ log("Launching \"%s\".\n", cmd.c_str());
+ int retval = run_command(cmd, process_line);
+ if (retval == 0) {
+ ret.sat = true;
+ ret.unknown = false;
+ } else if (retval == 1) {
+ ret.sat = false;
+ ret.unknown = false;
+ }
+ }
+
+ if(!opt.nocleanup)
+ remove_directory(tempdir_name);
+
+ recover_solution(ret);
+
+ return ret;
+}
+
+pool<std::string> validate_design_and_get_inputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
+ bool found_input = false;
+ bool found_hole = false;
+ bool found_1bit_output = false;
+ bool found_assert_assume = false;
+ pool<std::string> input_wires;
+ for (auto wire : module->wires()) {
+ if (wire->port_input) {
+ found_input = true;
+ input_wires.insert(wire->name.str());
+ }
+ if (wire->port_output && wire->width == 1)
+ found_1bit_output = true;
+ }
+ for (auto cell : module->cells()) {
+ if (cell->type == "$allconst")
+ found_input = true;
+ if (cell->type == "$anyconst")
+ found_hole = true;
+ if (cell->type.in("$assert", "$assume"))
+ found_assert_assume = true;
+ }
+ if (!found_input)
+ log_cmd_error("Can't perform QBF-SAT on a miter with no inputs!\n");
+ if (!found_hole)
+ log_cmd_error("Did not find any existentially-quantified variables. Use 'sat' instead.\n");
+ if (!found_1bit_output && !found_assert_assume)
+ log_cmd_error("Did not find any single-bit outputs or $assert/$assume cells. Is this a miter circuit?\n");
+ if (!found_assert_assume && !opt.assume_outputs)
+ log_cmd_error("Did not find any $assert/$assume cells. Single-bit outputs were found, but `-assume-outputs` was not specified.\n");
+
+ return input_wires;
+}
+
+QbfSolveOptions parse_args(const std::vector<std::string> &args) {
+ QbfSolveOptions opt;
+ for (opt.argidx = 1; opt.argidx < args.size(); opt.argidx++) {
+ if (args[opt.argidx] == "-nocleanup") {
+ opt.nocleanup = true;
+ continue;
+ }
+ else if (args[opt.argidx] == "-specialize") {
+ opt.specialize = true;
+ continue;
+ }
+ else if (args[opt.argidx] == "-assume-outputs") {
+ opt.assume_outputs = true;
+ continue;
+ }
+ else if (args[opt.argidx] == "-sat") {
+ opt.sat = true;
+ continue;
+ }
+ else if (args[opt.argidx] == "-unsat") {
+ opt.unsat = true;
+ continue;
+ }
+ else if (args[opt.argidx] == "-show-smtbmc") {
+ opt.show_smtbmc = true;
+ continue;
+ }
+ else if (args[opt.argidx] == "-dump-final-smt2") {
+ opt.dump_final_smt2 = true;
+ if (args.size() <= opt.argidx + 1)
+ log_cmd_error("smt2 file not specified.\n");
+ else
+ opt.dump_final_smt2_file = args[++opt.argidx];
+ continue;
+ }
+ else if (args[opt.argidx] == "-specialize-from-file") {
+ opt.specialize_from_file = true;
+ if (args.size() <= opt.argidx + 1)
+ log_cmd_error("solution file not specified.\n");
+ else
+ opt.specialize_soln_file = args[++opt.argidx];
+ continue;
+ }
+ else if (args[opt.argidx] == "-write-solution") {
+ opt.write_solution = true;
+ if (args.size() <= opt.argidx + 1)
+ log_cmd_error("solution file not specified.\n");
+ else
+ opt.write_soln_soln_file = args[++opt.argidx];
+ continue;
+ }
+ break;
+ }
+
+ return opt;
+}
+
+void print_proof_failed()
+{
+ log("\n");
+ log(" ______ ___ ___ _ _ _ _ \n");
+ log(" (_____ \\ / __) / __) (_) | | | |\n");
+ log(" _____) )___ ___ ___ _| |__ _| |__ _____ _| | _____ __| | |\n");
+ log(" | ____/ ___) _ \\ / _ (_ __) (_ __|____ | | || ___ |/ _ |_|\n");
+ log(" | | | | | |_| | |_| || | | | / ___ | | || ____( (_| |_ \n");
+ log(" |_| |_| \\___/ \\___/ |_| |_| \\_____|_|\\_)_____)\\____|_|\n");
+ log("\n");
+}
+
+void print_qed()
+{
+ log("\n");
+ log(" /$$$$$$ /$$$$$$$$ /$$$$$$$ \n");
+ log(" /$$__ $$ | $$_____/ | $$__ $$ \n");
+ log(" | $$ \\ $$ | $$ | $$ \\ $$ \n");
+ log(" | $$ | $$ | $$$$$ | $$ | $$ \n");
+ log(" | $$ | $$ | $$__/ | $$ | $$ \n");
+ log(" | $$/$$ $$ | $$ | $$ | $$ \n");
+ log(" | $$$$$$/ /$$| $$$$$$$$ /$$| $$$$$$$//$$\n");
+ log(" \\____ $$$|__/|________/|__/|_______/|__/\n");
+ log(" \\__/ \n");
+ log("\n");
+}
+
+struct QbfSatPass : public Pass {
+ QbfSatPass() : Pass("qbfsat", "solve a 2QBF-SAT problem in the circuit") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" qbfsat [options] [selection]\n");
+ log("\n");
+ log("This command solves a 2QBF-SAT problem defined over the currently selected module.\n");
+ log("Existentially-quantified variables are declared by assigning a wire \"$anyconst\".\n");
+ log("Universally-quantified variables may be explicitly declared by assigning a wire\n");
+ log("\"$allconst\", but module inputs will be treated as universally-quantified variables\n");
+ log("by default.\n");
+ log("\n");
+ log(" -nocleanup\n");
+ log(" Do not delete temporary files and directories. Useful for\n");
+ log(" debugging.\n");
+ log("\n");
+ log(" -dump-final-smt2 <file>\n");
+ log(" Pass the --dump-smt2 option to yosys-smtbmc.\n");
+ log("\n");
+ log(" -assume-outputs\n");
+ log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n");
+ log("\n");
+ log(" -sat\n");
+ log(" Generate an error if the solver does not return \"sat\".\n");
+ log("\n");
+ log(" -unsat\n");
+ log(" Generate an error if the solver does not return \"unsat\".\n");
+ log("\n");
+ log(" -show-smtbmc\n");
+ log(" Print the output from yosys-smtbmc.\n");
+ log("\n");
+ log(" -specialize\n");
+ log(" Replace all \"$anyconst\" cells with constant values determined by the solver.\n");
+ log("\n");
+ log(" -specialize-from-file <solution file>\n");
+ log(" Do not run the solver, but instead only attempt to replace all \"$anyconst\"\n");
+ log(" cells in the current module with values provided by the specified file.\n");
+ log("\n");
+ log(" -write-solution <solution file>\n");
+ log(" Write the assignments discovered by the solver for all \"$anyconst\" cells\n");
+ log(" to the specified file.");
+ log("\n");
+ log("\n");
+ }
+
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ log_header(design, "Executing QBFSAT pass (solving QBF-SAT problems in the circuit).\n");
+ QbfSolveOptions opt = parse_args(args);
+ extra_args(args, opt.argidx, design);
+
+ RTLIL::Module *module = nullptr;
+ for (auto mod : design->selected_modules()) {
+ if (module)
+ log_cmd_error("Only one module must be selected for the QBF-SAT pass! (selected: %s and %s)\n", log_id(module), log_id(mod));
+ module = mod;
+ }
+ if (module == nullptr)
+ log_cmd_error("Can't perform QBF-SAT on an empty selection!\n");
+
+ log_push();
+ if (!opt.specialize_from_file) {
+ //Save the design to restore after modiyfing the current module.
+ std::string module_name = module->name.str();
+ Pass::call(design, "design -push-copy");
+
+ //Replace input wires with wires assigned $allconst cells.
+ pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
+ allconstify_inputs(module, input_wires);
+ if (opt.assume_outputs)
+ assume_miter_outputs(module);
+
+ QbfSolutionType ret = qbf_solve(module, opt);
+ Pass::call(design, "design -pop");
+ module = design->module(module_name);
+
+ if (ret.unknown)
+ log_warning("solver did not give an answer\n");
+ else if (ret.sat)
+ print_qed();
+ else
+ print_proof_failed();
+
+ if(!ret.unknown && ret.sat) {
+ if (opt.write_solution) {
+ write_solution(module, ret, opt.write_soln_soln_file);
+ }
+ if (opt.specialize) {
+ specialize(module, ret);
+ } else {
+ dump_model(module, ret);
+ }
+ if (opt.unsat)
+ log_cmd_error("expected problem to be UNSAT\n");
+ }
+ else if (!ret.unknown && !ret.sat && opt.sat)
+ log_cmd_error("expected problem to be SAT\n");
+ else if (ret.unknown && (opt.sat || opt.unsat))
+ log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT");
+ } else
+ specialize_from_file(module, opt.specialize_soln_file);
+ log_pop();
+ }
+} QbfSatPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc
index c16db0d57..766b954df 100644
--- a/passes/techmap/Makefile.inc
+++ b/passes/techmap/Makefile.inc
@@ -34,7 +34,6 @@ OBJS += passes/techmap/aigmap.o
OBJS += passes/techmap/tribuf.o
OBJS += passes/techmap/lut2mux.o
OBJS += passes/techmap/nlutmap.o
-OBJS += passes/techmap/dffsr2dff.o
OBJS += passes/techmap/shregmap.o
OBJS += passes/techmap/deminout.o
OBJS += passes/techmap/insbuf.o
@@ -59,10 +58,10 @@ passes/techmap/techmap.inc: techlibs/common/techmap.v
passes/techmap/techmap.o: passes/techmap/techmap.inc
ifneq ($(CONFIG),emcc)
-TARGETS += yosys-filterlib$(EXE)
+TARGETS += $(PROGRAM_PREFIX)yosys-filterlib$(EXE)
EXTRA_OBJS += passes/techmap/filterlib.o
-yosys-filterlib$(EXE): passes/techmap/filterlib.o
+$(PROGRAM_PREFIX)yosys-filterlib$(EXE): passes/techmap/filterlib.o
$(Q) mkdir -p $(dir $@)
- $(P) $(LD) -o yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS)
+ $(P) $(LD) -o $(PROGRAM_PREFIX)yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS)
endif
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 78ecab1e7..0ee495abd 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -702,7 +702,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
if (dff_mode && clk_sig.empty())
log_cmd_error("Clock domain %s not found.\n", clk_str.c_str());
- std::string tempdir_name = "/tmp/yosys-abc-XXXXXX";
+ std::string tempdir_name = "/tmp/" + proc_program_prefix()+ "yosys-abc-XXXXXX";
if (!cleanup)
tempdir_name[0] = tempdir_name[4] = '_';
tempdir_name = make_temp_dir(tempdir_name);
@@ -1305,7 +1305,7 @@ struct AbcPass : public Pass {
#ifdef ABCEXTERNAL
log(" use the specified command instead of \"" ABCEXTERNAL "\" to execute ABC.\n");
#else
- log(" use the specified command instead of \"<yosys-bindir>/yosys-abc\" to execute ABC.\n");
+ log(" use the specified command instead of \"<yosys-bindir>/%syosys-abc\" to execute ABC.\n", proc_program_prefix().c_str());
#endif
log(" This can e.g. be used to call a specific version of ABC or a wrapper.\n");
log("\n");
@@ -1491,7 +1491,7 @@ struct AbcPass : public Pass {
#ifdef ABCEXTERNAL
std::string exe_file = ABCEXTERNAL;
#else
- std::string exe_file = proc_self_dirname() + "yosys-abc";
+ std::string exe_file = proc_self_dirname() + proc_program_prefix() + "yosys-abc";
#endif
std::string script_file, liberty_file, constr_file, clk_str;
std::string delay_target, sop_inputs, sop_products, lutin_shared = "-S 1";
@@ -1509,8 +1509,8 @@ struct AbcPass : public Pass {
#ifdef _WIN32
#ifndef ABCEXTERNAL
- if (!check_file_exists(exe_file + ".exe") && check_file_exists(proc_self_dirname() + "..\\yosys-abc.exe"))
- exe_file = proc_self_dirname() + "..\\yosys-abc";
+ if (!check_file_exists(exe_file + ".exe") && check_file_exists(proc_self_dirname() + "..\\" + proc_program_prefix()+ "yosys-abc.exe"))
+ exe_file = proc_self_dirname() + "..\\" + proc_program_prefix() + "yosys-abc";
#endif
#endif
diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc
index 9757b1539..1b3d5ff06 100644
--- a/passes/techmap/abc9.cc
+++ b/passes/techmap/abc9.cc
@@ -100,7 +100,7 @@ struct Abc9Pass : public ScriptPass
#ifdef ABCEXTERNAL
log(" use the specified command instead of \"" ABCEXTERNAL "\" to execute ABC.\n");
#else
- log(" use the specified command instead of \"<yosys-bindir>/yosys-abc\" to execute ABC.\n");
+ log(" use the specified command instead of \"<yosys-bindir>/%syosys-abc\" to execute ABC.\n", proc_program_prefix().c_str());
#endif
log(" This can e.g. be used to call a specific version of ABC or a wrapper.\n");
log("\n");
@@ -326,7 +326,7 @@ struct Abc9Pass : public ScriptPass
if (!active_design->selected_whole_module(mod))
log_error("Can't handle partially selected module %s!\n", log_id(mod));
- std::string tempdir_name = "/tmp/yosys-abc-XXXXXX";
+ std::string tempdir_name = "/tmp/" + proc_program_prefix() + "yosys-abc-XXXXXX";
if (!cleanup)
tempdir_name[0] = tempdir_name[4] = '_';
tempdir_name = make_temp_dir(tempdir_name);
diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc
index 898285c69..18618ff91 100644
--- a/passes/techmap/abc9_exe.cc
+++ b/passes/techmap/abc9_exe.cc
@@ -222,9 +222,9 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
abc9_script += stringf("; &ps -l; &write -n %s/output.aig", tempdir_name.c_str());
if (design->scratchpad_get_bool("abc9.verify")) {
if (dff_mode)
- abc9_script += "; verify -s";
+ abc9_script += "; &verify -s";
else
- abc9_script += "; verify";
+ abc9_script += "; &verify";
}
abc9_script += "; time";
abc9_script = add_echos_to_abc9_cmd(abc9_script);
@@ -293,7 +293,7 @@ struct Abc9ExePass : public Pass {
#ifdef ABCEXTERNAL
log(" use the specified command instead of \"" ABCEXTERNAL "\" to execute ABC.\n");
#else
- log(" use the specified command instead of \"<yosys-bindir>/yosys-abc\" to execute ABC.\n");
+ log(" use the specified command instead of \"<yosys-bindir>/%syosys-abc\" to execute ABC.\n", proc_program_prefix().c_str());
#endif
log(" This can e.g. be used to call a specific version of ABC or a wrapper.\n");
log("\n");
@@ -367,7 +367,7 @@ struct Abc9ExePass : public Pass {
#ifdef ABCEXTERNAL
std::string exe_file = ABCEXTERNAL;
#else
- std::string exe_file = proc_self_dirname() + "yosys-abc";
+ std::string exe_file = proc_self_dirname() + proc_program_prefix()+ "yosys-abc";
#endif
std::string script_file, clk_str, box_file, lut_file;
std::string delay_target, lutin_shared = "-S 1", wire_delay;
@@ -383,8 +383,8 @@ struct Abc9ExePass : public Pass {
#ifdef _WIN32
#ifndef ABCEXTERNAL
- if (!check_file_exists(exe_file + ".exe") && check_file_exists(proc_self_dirname() + "..\\yosys-abc.exe"))
- exe_file = proc_self_dirname() + "..\\yosys-abc";
+ if (!check_file_exists(exe_file + ".exe") && check_file_exists(proc_self_dirname() + "..\\" + proc_program_prefix() + "yosys-abc.exe"))
+ exe_file = proc_self_dirname() + "..\\" + proc_program_prefix() + "yosys-abc";
#endif
#endif
diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc
index 00af36615..8ae1b51ff 100644
--- a/passes/techmap/abc9_ops.cc
+++ b/passes/techmap/abc9_ops.cc
@@ -434,6 +434,9 @@ void prep_delays(RTLIL::Design *design, bool dff_mode)
auto &t = timing.at(derived_type).required;
for (auto &conn : cell->connections_) {
auto port_wire = inst_module->wire(conn.first);
+ if (!port_wire)
+ log_error("Port %s in cell %s (type %s) of module %s does not actually exist",
+ log_id(conn.first), log_id(cell->name), log_id(cell->type), log_id(module->name));
if (!port_wire->port_input)
continue;
diff --git a/passes/techmap/dffinit.cc b/passes/techmap/dffinit.cc
index 0424ce434..35645582b 100644
--- a/passes/techmap/dffinit.cc
+++ b/passes/techmap/dffinit.cc
@@ -154,9 +154,11 @@ struct DffinitPass : public Pass {
value = Const(low_string);
}
- log("Setting %s.%s.%s (port=%s, net=%s) to %s.\n", log_id(module), log_id(cell), log_id(it.second),
- log_id(it.first), log_signal(sig), log_signal(value));
- cell->setParam(it.second, value);
+ if (value.size() != 0) {
+ log("Setting %s.%s.%s (port=%s, net=%s) to %s.\n", log_id(module), log_id(cell), log_id(it.second),
+ log_id(it.first), log_signal(sig), log_signal(value));
+ cell->setParam(it.second, value);
+ }
}
}
diff --git a/passes/techmap/dffsr2dff.cc b/passes/techmap/dffsr2dff.cc
deleted file mode 100644
index 4a3ddaf73..000000000
--- a/passes/techmap/dffsr2dff.cc
+++ /dev/null
@@ -1,213 +0,0 @@
-/*
- * 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"
-
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-
-void dffsr_worker(SigMap &sigmap, Module *module, Cell *cell)
-{
- if (cell->type == ID($dffsr))
- {
- int width = cell->getParam(ID::WIDTH).as_int();
- bool setpol = cell->getParam(ID::SET_POLARITY).as_bool();
- bool clrpol = cell->getParam(ID::CLR_POLARITY).as_bool();
-
- SigBit setunused = setpol ? State::S0 : State::S1;
- SigBit clrunused = clrpol ? State::S0 : State::S1;
-
- SigSpec setsig = sigmap(cell->getPort(ID::SET));
- SigSpec clrsig = sigmap(cell->getPort(ID::CLR));
-
- Const reset_val;
- SigSpec setctrl, clrctrl;
-
- for (int i = 0; i < width; i++)
- {
- SigBit setbit = setsig[i], clrbit = clrsig[i];
-
- if (setbit == setunused) {
- clrctrl.append(clrbit);
- reset_val.bits.push_back(State::S0);
- continue;
- }
-
- if (clrbit == clrunused) {
- setctrl.append(setbit);
- reset_val.bits.push_back(State::S1);
- continue;
- }
-
- return;
- }
-
- setctrl.sort_and_unify();
- clrctrl.sort_and_unify();
-
- if (GetSize(setctrl) > 1 || GetSize(clrctrl) > 1)
- return;
-
- if (GetSize(setctrl) == 0 && GetSize(clrctrl) == 0)
- return;
-
- if (GetSize(setctrl) == 1 && GetSize(clrctrl) == 1) {
- if (setpol != clrpol)
- return;
- if (setctrl != clrctrl)
- return;
- }
-
- log("Converting %s cell %s.%s to $adff.\n", log_id(cell->type), log_id(module), log_id(cell));
-
- if (GetSize(setctrl) == 1) {
- cell->setPort(ID::ARST, setctrl);
- cell->setParam(ID::ARST_POLARITY, setpol);
- } else {
- cell->setPort(ID::ARST, clrctrl);
- cell->setParam(ID::ARST_POLARITY, clrpol);
- }
-
- cell->type = ID($adff);
- cell->unsetPort(ID::SET);
- cell->unsetPort(ID::CLR);
- cell->setParam(ID::ARST_VALUE, reset_val);
- cell->unsetParam(ID::SET_POLARITY);
- cell->unsetParam(ID::CLR_POLARITY);
-
- return;
- }
-
- if (cell->type.in(ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
- ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_)))
- {
- char clkpol = cell->type.c_str()[8];
- char setpol = cell->type.c_str()[9];
- char clrpol = cell->type.c_str()[10];
-
- SigBit setbit = sigmap(cell->getPort(ID::S));
- SigBit clrbit = sigmap(cell->getPort(ID::R));
-
- SigBit setunused = setpol == 'P' ? State::S0 : State::S1;
- SigBit clrunused = clrpol == 'P' ? State::S0 : State::S1;
-
- IdString oldtype = cell->type;
-
- if (setbit == setunused) {
- cell->type = stringf("$_DFF_%c%c0_", clkpol, clrpol);
- cell->unsetPort(ID::S);
- goto converted_gate;
- }
-
- if (clrbit == clrunused) {
- cell->type = stringf("$_DFF_%c%c1_", clkpol, setpol);
- cell->setPort(ID::R, cell->getPort(ID::S));
- cell->unsetPort(ID::S);
- goto converted_gate;
- }
-
- return;
-
- converted_gate:
- log("Converting %s cell %s.%s to %s.\n", log_id(oldtype), log_id(module), log_id(cell), log_id(cell->type));
- return;
- }
-}
-
-void adff_worker(SigMap &sigmap, Module *module, Cell *cell)
-{
- if (cell->type == ID($adff))
- {
- bool rstpol = cell->getParam(ID::ARST_POLARITY).as_bool();
- SigBit rstunused = rstpol ? State::S0 : State::S1;
- SigSpec rstsig = sigmap(cell->getPort(ID::ARST));
-
- if (rstsig != rstunused)
- return;
-
- log("Converting %s cell %s.%s to $dff.\n", log_id(cell->type), log_id(module), log_id(cell));
-
- cell->type = ID($dff);
- cell->unsetPort(ID::ARST);
- cell->unsetParam(ID::ARST_VALUE);
- cell->unsetParam(ID::ARST_POLARITY);
-
- return;
- }
-
- if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
- ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_)))
- {
- char clkpol = cell->type.c_str()[6];
- char rstpol = cell->type.c_str()[7];
-
- SigBit rstbit = sigmap(cell->getPort(ID::R));
- SigBit rstunused = rstpol == 'P' ? State::S0 : State::S1;
-
- if (rstbit != rstunused)
- return;
-
- IdString newtype = stringf("$_DFF_%c_", clkpol);
- log("Converting %s cell %s.%s to %s.\n", log_id(cell->type), log_id(module), log_id(cell), log_id(newtype));
-
- cell->type = newtype;
- cell->unsetPort(ID::R);
-
- return;
- }
-}
-
-struct Dffsr2dffPass : public Pass {
- Dffsr2dffPass() : Pass("dffsr2dff", "convert DFFSR cells to simpler FF cell types") { }
- void help() YS_OVERRIDE
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" dffsr2dff [options] [selection]\n");
- log("\n");
- log("This pass converts DFFSR cells ($dffsr, $_DFFSR_???_) and ADFF cells ($adff,\n");
- log("$_DFF_???_) to simpler FF cell types when any of the set/reset inputs is unused.\n");
- log("\n");
- }
- void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
- {
- log_header(design, "Executing DFFSR2DFF pass (mapping DFFSR cells to simpler FFs).\n");
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++)
- {
- // if (args[argidx] == "-v") {
- // continue;
- // }
- break;
- }
- extra_args(args, argidx, design);
-
- for (auto module : design->selected_modules()) {
- SigMap sigmap(module);
- for (auto cell : module->selected_cells()) {
- dffsr_worker(sigmap, module, cell);
- adff_worker(sigmap, module, cell);
- }
- }
- }
-} Dffsr2dffPass;
-
-PRIVATE_NAMESPACE_END
diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc
index 518afa1a7..a554be257 100644
--- a/passes/techmap/techmap.cc
+++ b/passes/techmap/techmap.cc
@@ -1282,7 +1282,7 @@ struct TechmapPass : public Pass {
if (fn.compare(0, 1, "%") == 0) {
if (!saved_designs.count(fn.substr(1))) {
delete map;
- log_cmd_error("Can't saved design `%s'.\n", fn.c_str()+1);
+ log_cmd_error("Can't open saved design `%s'.\n", fn.c_str()+1);
}
for (auto mod : saved_designs.at(fn.substr(1))->modules())
if (!map->has(mod->name))
diff --git a/passes/techmap/zinit.cc b/passes/techmap/zinit.cc
index a427c4987..74604ba3b 100644
--- a/passes/techmap/zinit.cc
+++ b/passes/techmap/zinit.cc
@@ -57,8 +57,7 @@ struct ZinitPass : public Pass {
for (auto module : design->selected_modules())
{
SigMap sigmap(module);
- dict<SigBit, State> initbits;
- pool<SigBit> donebits;
+ dict<SigBit, std::pair<State,SigBit>> initbits;
for (auto wire : module->selected_wires())
{
@@ -67,7 +66,6 @@ struct ZinitPass : public Pass {
SigSpec wirebits = sigmap(wire);
Const initval = wire->attributes.at(ID::init);
- wire->attributes.erase(ID::init);
for (int i = 0; i < GetSize(wirebits) && i < GetSize(initval); i++)
{
@@ -78,24 +76,35 @@ struct ZinitPass : public Pass {
continue;
if (initbits.count(bit)) {
- if (initbits.at(bit) != val)
+ if (initbits.at(bit).first != val)
log_error("Conflicting init values for signal %s (%s = %s != %s).\n",
log_signal(bit), log_signal(SigBit(wire, i)),
- log_signal(val), log_signal(initbits.at(bit)));
+ log_signal(val), log_signal(initbits.at(bit).first));
continue;
}
- initbits[bit] = val;
+ initbits[bit] = std::make_pair(val,SigBit(wire,i));
}
}
pool<IdString> dff_types = {
- ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($adff),
+ // FIXME: It would appear that supporting
+ // $dffsr/$_DFFSR_* would require a new
+ // cell type where S has priority over R
+ ID($ff), ID($dff), ID($dffe), /*ID($dffsr),*/ ID($adff),
ID($_FF_), ID($_DFFE_NN_), ID($_DFFE_NP_), ID($_DFFE_PN_), ID($_DFFE_PP_),
- ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
- ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_),
+ /*ID($_DFFSR_NNN_), ID($_DFFSR_NNP_), ID($_DFFSR_NPN_), ID($_DFFSR_NPP_),
+ ID($_DFFSR_PNN_), ID($_DFFSR_PNP_), ID($_DFFSR_PPN_), ID($_DFFSR_PPP_),*/
ID($_DFF_N_), ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
- ID($_DFF_P_), ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_)
+ ID($_DFF_P_), ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_),
+ // Async set/reset
+ ID($__DFFE_NN0), ID($__DFFE_NN1), ID($__DFFE_NP0), ID($__DFFE_NP1),
+ ID($__DFFE_PN0), ID($__DFFE_PN1), ID($__DFFE_PP0), ID($__DFFE_PP1),
+ // Sync set/reset
+ ID($__DFFS_NN0_), ID($__DFFS_NN1_), ID($__DFFS_NP0_), ID($__DFFS_NP1_),
+ ID($__DFFS_PN0_), ID($__DFFS_PN1_), ID($__DFFS_PP0_), ID($__DFFS_PP1_),
+ ID($__DFFSE_NN0), ID($__DFFSE_NN1), ID($__DFFSE_NP0), ID($__DFFSE_NP1),
+ ID($__DFFSE_PN0), ID($__DFFSE_PN1), ID($__DFFSE_PP0), ID($__DFFSE_PP1)
};
for (auto cell : module->selected_cells())
@@ -113,8 +122,10 @@ struct ZinitPass : public Pass {
for (int i = 0; i < GetSize(sig_q); i++) {
if (initbits.count(sig_q[i])) {
- initval.bits.push_back(initbits.at(sig_q[i]));
- donebits.insert(sig_q[i]);
+ const auto &d = initbits.at(sig_q[i]);
+ initval.bits.push_back(d.first);
+ const auto &b = d.second;
+ b.wire->attributes.at(ID::init)[b.offset] = State::Sx;
} else
initval.bits.push_back(all_mode ? State::S0 : State::Sx);
}
@@ -123,11 +134,11 @@ struct ZinitPass : public Pass {
initwire->attributes[ID::init] = initval;
for (int i = 0; i < GetSize(initwire); i++)
- if (initval.bits.at(i) == State::S1)
+ if (initval[i] == State::S1)
{
sig_d[i] = module->NotGate(NEW_ID, sig_d[i]);
module->addNotGate(NEW_ID, SigSpec(initwire, i), sig_q[i]);
- initwire->attributes[ID::init].bits.at(i) = State::S0;
+ initwire->attributes[ID::init][i] = State::S0;
}
else
{
@@ -139,11 +150,36 @@ struct ZinitPass : public Pass {
cell->setPort(ID::D, sig_d);
cell->setPort(ID::Q, initwire);
- }
- for (auto &it : initbits)
- if (donebits.count(it.first) == 0)
- log_error("Failed to handle init bit %s = %s.\n", log_signal(it.first), log_signal(it.second));
+ if (cell->type == ID($adff)) {
+ auto val = cell->getParam(ID::ARST_VALUE);
+ for (int i = 0; i < GetSize(initwire); i++)
+ if (initval[i] == State::S1)
+ val[i] = (val[i] == State::S1 ? State::S0 : State::S1);
+ cell->setParam(ID::ARST_VALUE, std::move(val));
+ }
+ else if (initval == State::S1) {
+ std::string t = cell->type.str();
+ if (cell->type.in(ID($_DFF_NN0_), ID($_DFF_NN1_), ID($_DFF_NP0_), ID($_DFF_NP1_),
+ ID($_DFF_PN0_), ID($_DFF_PN1_), ID($_DFF_PP0_), ID($_DFF_PP1_)))
+ {
+ t[8] = (t[8] == '0' ? '1' : '0');
+ }
+ else if (cell->type.in(ID($__DFFE_NN0), ID($__DFFE_NN1), ID($__DFFE_NP0), ID($__DFFE_NP1),
+ ID($__DFFE_PN0), ID($__DFFE_PN1), ID($__DFFE_PP0), ID($__DFFE_PP1),
+ ID($__DFFS_NN0_), ID($__DFFS_NN1_), ID($__DFFS_NP0_), ID($__DFFS_NP1_),
+ ID($__DFFS_PN0_), ID($__DFFS_PN1_), ID($__DFFS_PP0_), ID($__DFFS_PP1_)))
+ {
+ t[10] = (t[10] == '0' ? '1' : '0');
+ }
+ else if (cell->type.in(ID($__DFFSE_NN0), ID($__DFFSE_NN1), ID($__DFFSE_NP0), ID($__DFFSE_NP1),
+ ID($__DFFSE_PN0), ID($__DFFSE_PN1), ID($__DFFSE_PP0), ID($__DFFSE_PP1)))
+ {
+ t[11] = (t[11] == '0' ? '1' : '0');
+ }
+ cell->type = t;
+ }
+ }
}
}
} ZinitPass;
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-14 03:33:05 +0000