aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/abc/Makefile.inc1
-rw-r--r--passes/abc/abc.cc281
-rw-r--r--passes/abc/blifparse.cc77
-rw-r--r--passes/abc/blifparse.h2
-rw-r--r--passes/abc/vlparse.cc227
-rw-r--r--passes/abc/vlparse.h28
-rw-r--r--passes/cmds/rename.cc45
-rw-r--r--passes/cmds/select.cc20
-rw-r--r--passes/extract/extract.cc2
-rw-r--r--passes/memory/memory_collect.cc21
-rw-r--r--passes/opt/opt_const.cc36
-rw-r--r--passes/proc/proc_arst.cc4
-rw-r--r--passes/sat/eval.cc2
-rw-r--r--passes/sat/freduce.cc689
-rw-r--r--passes/sat/sat.cc239
-rw-r--r--passes/techmap/dfflibmap.cc55
-rw-r--r--passes/techmap/simplemap.cc19
17 files changed, 1033 insertions, 715 deletions
diff --git a/passes/abc/Makefile.inc b/passes/abc/Makefile.inc
index dbb7496cf..a7c5b02c6 100644
--- a/passes/abc/Makefile.inc
+++ b/passes/abc/Makefile.inc
@@ -1,7 +1,6 @@
ifeq ($(ENABLE_ABC),1)
OBJS += passes/abc/abc.o
-OBJS += passes/abc/vlparse.o
OBJS += passes/abc/blifparse.o
endif
diff --git a/passes/abc/abc.cc b/passes/abc/abc.cc
index e37f896f2..efba43591 100644
--- a/passes/abc/abc.cc
+++ b/passes/abc/abc.cc
@@ -21,6 +21,10 @@
// Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification
// http://www.eecs.berkeley.edu/~alanmi/abc/
+// [[CITE]] Berkeley Logic Interchange Format (BLIF)
+// University of California. Berkeley. July 28, 1992
+// http://www.ece.cmu.edu/~ee760/760docs/blif.pdf
+
// [[CITE]] Kahn's Topological sorting algorithm
// Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558–562, doi:10.1145/368996.369025
// http://en.wikipedia.org/wiki/Topological_sorting
@@ -36,7 +40,6 @@
#include <dirent.h>
#include <sstream>
-#include "vlparse.h"
#include "blifparse.h"
struct gate_t
@@ -54,6 +57,9 @@ static RTLIL::Module *module;
static std::vector<gate_t> signal_list;
static std::map<RTLIL::SigSpec, int> signal_map;
+static bool clk_polarity;
+static RTLIL::SigSpec clk_sig;
+
static int map_signal(RTLIL::SigSpec sig, char gate_type = -1, int in1 = -1, int in2 = -1, int in3 = -1)
{
assert(sig.width == 1);
@@ -100,6 +106,26 @@ static void mark_port(RTLIL::SigSpec sig)
static void extract_cell(RTLIL::Cell *cell)
{
+ if (cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")
+ {
+ if (clk_polarity != (cell->type == "$_DFF_P_"))
+ return;
+ if (clk_sig != assign_map(cell->connections["\\C"]))
+ return;
+
+ RTLIL::SigSpec sig_d = cell->connections["\\D"];
+ RTLIL::SigSpec sig_q = cell->connections["\\Q"];
+
+ assign_map.apply(sig_d);
+ assign_map.apply(sig_q);
+
+ map_signal(sig_q, 'f', map_signal(sig_d));
+
+ module->cells.erase(cell->name);
+ delete cell;
+ return;
+ }
+
if (cell->type == "$_INV_")
{
RTLIL::SigSpec sig_a = cell->connections["\\A"];
@@ -135,7 +161,7 @@ static void extract_cell(RTLIL::Cell *cell)
else if (cell->type == "$_XOR_")
map_signal(sig_y, 'x', mapped_a, mapped_b);
else
- abort();
+ log_abort();
module->cells.erase(cell->name);
delete cell;
@@ -217,20 +243,21 @@ static void handle_loops()
// dot_f = fopen("test.dot", "w");
for (auto &g : signal_list) {
- if (g.type == -1) {
+ if (g.type == -1 || g.type == 'f') {
workpool.insert(g.id);
- }
- if (g.in1 >= 0) {
- edges[g.in1].insert(g.id);
- in_edges_count[g.id]++;
- }
- if (g.in2 >= 0 && g.in2 != g.in1) {
- edges[g.in2].insert(g.id);
- in_edges_count[g.id]++;
- }
- if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
- edges[g.in3].insert(g.id);
- in_edges_count[g.id]++;
+ } else {
+ if (g.in1 >= 0) {
+ edges[g.in1].insert(g.id);
+ in_edges_count[g.id]++;
+ }
+ if (g.in2 >= 0 && g.in2 != g.in1) {
+ edges[g.in2].insert(g.id);
+ in_edges_count[g.id]++;
+ }
+ if (g.in3 >= 0 && g.in3 != g.in2 && g.in3 != g.in1) {
+ edges[g.in3].insert(g.id);
+ in_edges_count[g.id]++;
+ }
}
}
@@ -327,7 +354,8 @@ static void handle_loops()
fclose(dot_f);
}
-static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file, std::string liberty_file, std::string constr_file, bool cleanup, int lut_mode)
+static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
+ std::string liberty_file, std::string constr_file, bool cleanup, int lut_mode, bool dff_mode, std::string clk_str)
{
module = current_module;
map_autoidx = RTLIL::autoidx++;
@@ -336,14 +364,56 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
signal_list.clear();
assign_map.set(module);
+ clk_polarity = true;
+ clk_sig = RTLIL::SigSpec();
+
char tempdir_name[] = "/tmp/yosys-abc-XXXXXX";
if (!cleanup)
tempdir_name[0] = tempdir_name[4] = '_';
char *p = mkdtemp(tempdir_name);
- log_header("Extracting gate netlist of module `%s' to `%s/input.v'..\n", module->name.c_str(), tempdir_name);
+ log_header("Extracting gate netlist of module `%s' to `%s/input.blif'..\n", module->name.c_str(), tempdir_name);
if (p == NULL)
log_error("For some reason mkdtemp() failed!\n");
+ if (clk_str.empty()) {
+ if (clk_str[0] == '!') {
+ clk_polarity = false;
+ clk_str = clk_str.substr(1);
+ }
+ if (module->wires.count(RTLIL::escape_id(clk_str)) != 0)
+ clk_sig = assign_map(RTLIL::SigSpec(module->wires.at(RTLIL::escape_id(clk_str)), 1));
+ }
+
+ if (dff_mode && clk_sig.width == 0)
+ {
+ int best_dff_counter = 0;
+ std::map<std::pair<bool, RTLIL::SigSpec>, int> dff_counters;
+
+ for (auto &it : module->cells)
+ {
+ RTLIL::Cell *cell = it.second;
+ if (cell->type != "$_DFF_N_" && cell->type != "$_DFF_P_")
+ continue;
+
+ std::pair<bool, RTLIL::SigSpec> key(cell->type == "$_DFF_P_", assign_map(cell->connections.at("\\C")));
+ if (++dff_counters[key] > best_dff_counter) {
+ best_dff_counter = dff_counters[key];
+ clk_polarity = key.first;
+ clk_sig = key.second;
+ }
+ }
+ }
+
+ if (dff_mode || !clk_str.empty()) {
+ if (clk_sig.width == 0)
+ log("No (matching) clock domain found. Not extracting any FF cells.\n");
+ else
+ log("Found (matching) %s clock domain: %s\n", clk_polarity ? "posedge" : "negedge", log_signal(clk_sig));
+ }
+
+ if (clk_sig.width != 0)
+ mark_port(clk_sig);
+
std::vector<RTLIL::Cell*> cells;
cells.reserve(module->cells.size());
for (auto &it : module->cells)
@@ -363,60 +433,75 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
handle_loops();
- if (asprintf(&p, "%s/input.v", tempdir_name) < 0) abort();
+ if (asprintf(&p, "%s/input.blif", tempdir_name) < 0) log_abort();
FILE *f = fopen(p, "wt");
if (f == NULL)
log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
free(p);
- fprintf(f, "module netlist (");
- bool first = true;
+ fprintf(f, ".model netlist\n");
+
+ int count_input = 0;
+ fprintf(f, ".inputs");
for (auto &si : signal_list) {
- if (!si.is_port)
+ if (!si.is_port || si.type >= 0)
continue;
- if (!first)
- fprintf(f, ", ");
- fprintf(f, "n%d", si.id);
- first = false;
+ fprintf(f, " n%d", si.id);
+ count_input++;
}
- fprintf(f, "); // %s\n", module->name.c_str());
+ fprintf(f, "\n");
- int count_input = 0, count_output = 0;
+ int count_output = 0;
+ fprintf(f, ".outputs");
for (auto &si : signal_list) {
- if (si.is_port) {
- if (si.type >= 0)
- count_output++;
- else
- count_input++;
- }
- fprintf(f, "%s n%d; // %s\n", si.is_port ? si.type >= 0 ?
- "output" : "input" : "wire", si.id, log_signal(si.sig));
+ if (!si.is_port || si.type < 0)
+ continue;
+ fprintf(f, " n%d", si.id);
+ count_output++;
}
+ fprintf(f, "\n");
+
+ for (auto &si : signal_list)
+ fprintf(f, "# n%-5d %s\n", si.id, log_signal(si.sig));
+
for (auto &si : signal_list) {
assert(si.sig.width == 1 && si.sig.chunks.size() == 1);
- if (si.sig.chunks[0].wire == NULL)
- fprintf(f, "assign n%d = %c;\n", si.id, si.sig.chunks[0].data.bits[0] == RTLIL::State::S1 ? '1' : '0');
+ if (si.sig.chunks[0].wire == NULL) {
+ fprintf(f, ".names n%d\n", si.id);
+ if (si.sig.chunks[0].data.bits[0] == RTLIL::State::S1)
+ fprintf(f, "1\n");
+ }
}
int count_gates = 0;
for (auto &si : signal_list) {
- if (si.type == 'n')
- fprintf(f, "not (n%d, n%d);\n", si.id, si.in1);
- else if (si.type == 'a')
- fprintf(f, "and (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
- else if (si.type == 'o')
- fprintf(f, "or (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
- else if (si.type == 'x')
- fprintf(f, "xor (n%d, n%d, n%d);\n", si.id, si.in1, si.in2);
- else if (si.type == 'm')
- fprintf(f, "assign n%d = n%d ? n%d : n%d;\n", si.id, si.in3, si.in2, si.in1);
- else if (si.type >= 0)
- abort();
+ if (si.type == 'n') {
+ fprintf(f, ".names n%d n%d\n", si.in1, si.id);
+ fprintf(f, "0 1\n");
+ } else if (si.type == 'a') {
+ fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+ fprintf(f, "11 1\n");
+ } else if (si.type == 'o') {
+ fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+ fprintf(f, "-1 1\n");
+ fprintf(f, "1- 1\n");
+ } else if (si.type == 'x') {
+ fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+ fprintf(f, "01 1\n");
+ fprintf(f, "10 1\n");
+ } else if (si.type == 'm') {
+ fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
+ fprintf(f, "1-0 1\n");
+ fprintf(f, "-11 1\n");
+ } else if (si.type == 'f') {
+ fprintf(f, ".latch n%d n%d\n", si.in1, si.id);
+ } else if (si.type >= 0)
+ log_abort();
if (si.type >= 0)
count_gates++;
}
- fprintf(f, "endmodule\n");
+ fprintf(f, ".end\n");
fclose(f);
log("Extracted %d gates and %zd wires to a netlist network with %d inputs and %d outputs.\n",
@@ -427,7 +512,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
{
log_header("Executing ABC.\n");
- if (asprintf(&p, "%s/stdcells.genlib", tempdir_name) < 0) abort();
+ if (asprintf(&p, "%s/stdcells.genlib", tempdir_name) < 0) log_abort();
f = fopen(p, "wt");
if (f == NULL)
log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -443,7 +528,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
free(p);
if (lut_mode) {
- if (asprintf(&p, "%s/lutdefs.txt", tempdir_name) < 0) abort();
+ if (asprintf(&p, "%s/lutdefs.txt", tempdir_name) < 0) log_abort();
f = fopen(p, "wt");
if (f == NULL)
log_error("Opening %s for writing failed: %s\n", p, strerror(errno));
@@ -457,7 +542,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
int buffer_pos = 0;
if (!liberty_file.empty()) {
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; read_lib %s; ",
+ "%s -s -c 'read_blif %s/input.blif; read_lib %s; ",
exe_file.c_str(), tempdir_name, liberty_file.c_str());
if (!constr_file.empty())
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
@@ -470,21 +555,18 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
} else
if (!script_file.empty())
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; source %s; ",
+ "%s -s -c 'read_blif %s/input.blif; source %s; ",
exe_file.c_str(), tempdir_name, script_file.c_str());
else
if (lut_mode)
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; read_lut %s/lutdefs.txt; strash; balance; dch; if; ",
+ "%s -s -c 'read_blif %s/input.blif; read_lut %s/lutdefs.txt; strash; balance; dch; if; ",
exe_file.c_str(), tempdir_name, tempdir_name);
else
buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos,
- "%s -s -c 'read_verilog %s/input.v; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
+ "%s -s -c 'read_blif %s/input.blif; read_library %s/stdcells.genlib; strash; balance; dch; map; ",
exe_file.c_str(), tempdir_name, tempdir_name);
- if (lut_mode)
- buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
- else
- buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_verilog %s/output.v' 2>&1", tempdir_name);
+ buffer_pos += snprintf(buffer+buffer_pos, 1024-buffer_pos, "write_blif %s/output.blif' 2>&1", tempdir_name);
errno = ENOMEM; // popen does not set errno if memory allocation fails, therefore set it by hand
f = popen(buffer, "r");
@@ -504,16 +586,14 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
}
}
- if (asprintf(&p, "%s/%s", tempdir_name, lut_mode ? "output.blif" : "output.v") < 0) abort();
+ if (asprintf(&p, "%s/%s", tempdir_name, "output.blif") < 0) log_abort();
f = fopen(p, "rt");
if (f == NULL)
log_error("Can't open ABC output file `%s'.\n", p);
-#if 0
- RTLIL::Design *mapped_design = new RTLIL::Design;
- frontend_register["verilog"]->execute(f, p, std::vector<std::string>(), mapped_design);
-#else
- RTLIL::Design *mapped_design = lut_mode ? abc_parse_blif(f) : abc_parse_verilog(f);
-#endif
+
+ bool builtin_lib = liberty_file.empty() && script_file.empty() && !lut_mode;
+ RTLIL::Design *mapped_design = abc_parse_blif(f, builtin_lib ? "\\DFF" : "\\_dff_");
+
fclose(f);
free(p);
@@ -530,11 +610,11 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
}
std::map<std::string, int> cell_stats;
- if (liberty_file.empty() && script_file.empty() && !lut_mode)
+ if (builtin_lib)
{
for (auto &it : mapped_mod->cells) {
RTLIL::Cell *c = it.second;
- cell_stats[c->type.substr(1)]++;
+ cell_stats[RTLIL::unescape_id(c->type)]++;
if (c->type == "\\ZERO" || c->type == "\\ONE") {
RTLIL::SigSig conn;
conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Y"].chunks[0].wire->name)]);
@@ -582,21 +662,46 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
design->select(module, cell);
continue;
}
- assert(0);
+ if (c->type == "\\DFF") {
+ log_assert(clk_sig.width == 1);
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->type = clk_polarity ? "$_DFF_P_" : "$_DFF_N_";
+ cell->name = remap_name(c->name);
+ cell->connections["\\D"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\D"].chunks[0].wire->name)]);
+ cell->connections["\\Q"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Q"].chunks[0].wire->name)]);
+ cell->connections["\\C"] = clk_sig;
+ module->cells[cell->name] = cell;
+ design->select(module, cell);
+ continue;
+ }
+ log_abort();
}
}
else
{
- for (auto &it : mapped_mod->cells) {
+ for (auto &it : mapped_mod->cells)
+ {
RTLIL::Cell *c = it.second;
- cell_stats[c->type.substr(1)]++;
- if (c->type == "$_const0_" || c->type == "$_const1_") {
+ cell_stats[RTLIL::unescape_id(c->type)]++;
+ if (c->type == "\\_const0_" || c->type == "\\_const1_") {
RTLIL::SigSig conn;
- conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Y"].chunks[0].wire->name)]);
- conn.second = RTLIL::SigSpec(c->type == "$_const0_" ? 0 : 1, 1);
+ conn.first = RTLIL::SigSpec(module->wires[remap_name(c->connections.begin()->second.chunks[0].wire->name)]);
+ conn.second = RTLIL::SigSpec(c->type == "\\_const0_" ? 0 : 1, 1);
module->connections.push_back(conn);
continue;
}
+ if (c->type == "\\_dff_") {
+ log_assert(clk_sig.width == 1);
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->type = clk_polarity ? "$_DFF_P_" : "$_DFF_N_";
+ cell->name = remap_name(c->name);
+ cell->connections["\\D"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\D"].chunks[0].wire->name)]);
+ cell->connections["\\Q"] = RTLIL::SigSpec(module->wires[remap_name(c->connections["\\Q"].chunks[0].wire->name)]);
+ cell->connections["\\C"] = clk_sig;
+ module->cells[cell->name] = cell;
+ design->select(module, cell);
+ continue;
+ }
RTLIL::Cell *cell = new RTLIL::Cell;
cell->type = c->type;
cell->parameters = c->parameters;
@@ -663,7 +768,7 @@ static void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std
assert(n >= 0);
for (int i = 0; i < n; i++) {
if (strcmp(namelist[i]->d_name, ".") && strcmp(namelist[i]->d_name, "..")) {
- if (asprintf(&p, "%s/%s", tempdir_name, namelist[i]->d_name) < 0) abort();
+ if (asprintf(&p, "%s/%s", tempdir_name, namelist[i]->d_name) < 0) log_abort();
log("Removing `%s'.\n", p);
remove(p);
free(p);
@@ -708,6 +813,16 @@ struct AbcPass : public Pass {
log(" -lut <width>\n");
log(" generate netlist using luts of (max) the specified width.\n");
log("\n");
+ log(" -dff\n");
+ log(" also pass $_DFF_?_ cells through ABC (only one clock domain, if many\n");
+ log(" clock domains are present in a module, the one with the largest number\n");
+ log(" of $dff cells in it is used)\n");
+ log("\n");
+ log(" -clk [!]<signal-name>\n");
+ log(" use the specified clock domain. (when this option is used in combination\n");
+ log(" with -dff, then it falls back to the automatic dection of clock domain\n");
+ log(" if the specified clock is not found in a module.)\n");
+ log("\n");
log(" -nocleanup\n");
log(" when this option is used, the temporary files created by this pass\n");
log(" are not removed. this is useful for debugging.\n");
@@ -724,8 +839,8 @@ struct AbcPass : public Pass {
log_push();
std::string exe_file = rewrite_yosys_exe("yosys-abc");
- std::string script_file, liberty_file, constr_file;
- bool cleanup = true;
+ std::string script_file, liberty_file, constr_file, clk_str;
+ bool dff_mode = false, cleanup = true;
int lut_mode = 0;
size_t argidx;
@@ -758,6 +873,14 @@ struct AbcPass : public Pass {
lut_mode = atoi(args[++argidx].c_str());
continue;
}
+ if (arg == "-dff") {
+ dff_mode = true;
+ continue;
+ }
+ if (arg == "-clk" && argidx+1 < args.size() && lut_mode == 0) {
+ clk_str = args[++argidx];
+ continue;
+ }
if (arg == "-nocleanup") {
cleanup = false;
continue;
@@ -772,7 +895,7 @@ struct AbcPass : public Pass {
if (mod_it.second->processes.size() > 0)
log("Skipping module %s as it contains processes.\n", mod_it.second->name.c_str());
else
- abc_module(design, mod_it.second, script_file, exe_file, liberty_file, constr_file, cleanup, lut_mode);
+ abc_module(design, mod_it.second, script_file, exe_file, liberty_file, constr_file, cleanup, lut_mode, dff_mode, clk_str);
}
assign_map.clear();
diff --git a/passes/abc/blifparse.cc b/passes/abc/blifparse.cc
index 17acc843b..2d46d1a8e 100644
--- a/passes/abc/blifparse.cc
+++ b/passes/abc/blifparse.cc
@@ -22,29 +22,35 @@
#include <stdio.h>
#include <string.h>
-static bool read_next_line(char *buffer, int &line_count, FILE *f)
+static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, FILE *f)
{
+ int buffer_len = 0;
buffer[0] = 0;
while (1)
{
- int buffer_len = strlen(buffer);
+ buffer_len += strlen(buffer + buffer_len);
while (buffer_len > 0 && (buffer[buffer_len-1] == ' ' || buffer[buffer_len-1] == '\t' ||
buffer[buffer_len-1] == '\r' || buffer[buffer_len-1] == '\n'))
buffer[--buffer_len] = 0;
+ if (buffer_size-buffer_len < 4096) {
+ buffer_size *= 2;
+ buffer = (char*)realloc(buffer, buffer_size);
+ }
+
if (buffer_len == 0 || buffer[buffer_len-1] == '\\') {
if (buffer[buffer_len-1] == '\\')
buffer[--buffer_len] = 0;
line_count++;
- if (fgets(buffer+buffer_len, 4096-buffer_len, f) == NULL)
+ if (fgets(buffer+buffer_len, buffer_size-buffer_len, f) == NULL)
return false;
} else
return true;
}
}
-RTLIL::Design *abc_parse_blif(FILE *f)
+RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name)
{
RTLIL::Design *design = new RTLIL::Design;
RTLIL::Module *module = new RTLIL::Module;
@@ -56,12 +62,13 @@ RTLIL::Design *abc_parse_blif(FILE *f)
module->name = "\\netlist";
design->modules[module->name] = module;
- char buffer[4096];
+ size_t buffer_size = 4096;
+ char *buffer = (char*)malloc(buffer_size);
int line_count = 0;
while (1)
{
- if (!read_next_line(buffer, line_count, f))
+ if (!read_next_line(buffer, buffer_size, line_count, f))
goto error;
continue_without_read:
@@ -83,8 +90,10 @@ RTLIL::Design *abc_parse_blif(FILE *f)
if (!strcmp(cmd, ".model"))
continue;
- if (!strcmp(cmd, ".end"))
+ if (!strcmp(cmd, ".end")) {
+ free(buffer);
return design;
+ }
if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) {
char *p;
@@ -101,6 +110,58 @@ RTLIL::Design *abc_parse_blif(FILE *f)
continue;
}
+ if (!strcmp(cmd, ".latch"))
+ {
+ char *d = strtok(NULL, " \t\r\n");
+ char *q = strtok(NULL, " \t\r\n");
+
+ if (module->wires.count(RTLIL::escape_id(d)) == 0) {
+ RTLIL::Wire *wire = new RTLIL::Wire;
+ wire->name = RTLIL::escape_id(d);
+ module->add(wire);
+ }
+
+ if (module->wires.count(RTLIL::escape_id(q)) == 0) {
+ RTLIL::Wire *wire = new RTLIL::Wire;
+ wire->name = RTLIL::escape_id(q);
+ module->add(wire);
+ }
+
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->name = NEW_ID;
+ cell->type = dff_name;
+ cell->connections["\\D"] = module->wires.at(RTLIL::escape_id(d));
+ cell->connections["\\Q"] = module->wires.at(RTLIL::escape_id(q));
+ module->add(cell);
+ continue;
+ }
+
+ if (!strcmp(cmd, ".gate"))
+ {
+ RTLIL::Cell *cell = new RTLIL::Cell;
+ cell->name = NEW_ID;
+ module->add(cell);
+
+ char *p = strtok(NULL, " \t\r\n");
+ if (p == NULL)
+ goto error;
+ cell->type = RTLIL::escape_id(p);
+
+ while ((p = strtok(NULL, " \t\r\n")) != NULL) {
+ char *q = strchr(p, '=');
+ if (q == NULL || !q[0] || !q[1])
+ goto error;
+ *(q++) = 0;
+ if (module->wires.count(RTLIL::escape_id(q)) == 0) {
+ RTLIL::Wire *wire = new RTLIL::Wire;
+ wire->name = RTLIL::escape_id(q);
+ module->add(wire);
+ }
+ cell->connections[RTLIL::escape_id(p)] = module->wires.at(RTLIL::escape_id(q));
+ }
+ continue;
+ }
+
if (!strcmp(cmd, ".names"))
{
char *p;
@@ -122,7 +183,7 @@ RTLIL::Design *abc_parse_blif(FILE *f)
if (input_sig.width == 0) {
RTLIL::State state = RTLIL::State::Sa;
while (1) {
- if (!read_next_line(buffer, line_count, f))
+ if (!read_next_line(buffer, buffer_size, line_count, f))
goto error;
for (int i = 0; buffer[i]; i++) {
if (buffer[i] == ' ' || buffer[i] == '\t')
diff --git a/passes/abc/blifparse.h b/passes/abc/blifparse.h
index 98afedac5..272e4e645 100644
--- a/passes/abc/blifparse.h
+++ b/passes/abc/blifparse.h
@@ -22,7 +22,7 @@
#include "kernel/rtlil.h"
-extern RTLIL::Design *abc_parse_blif(FILE *f);
+extern RTLIL::Design *abc_parse_blif(FILE *f, std::string dff_name);
#endif
diff --git a/passes/abc/vlparse.cc b/passes/abc/vlparse.cc
deleted file mode 100644
index fe10f57b1..000000000
--- a/passes/abc/vlparse.cc
+++ /dev/null
@@ -1,227 +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 "vlparse.h"
-#include "kernel/log.h"
-#include <stdio.h>
-#include <string>
-
-static int lex_line, lex_tok;
-static std::string lex_str;
-
-static int token(int tok)
-{
- lex_tok = tok;
-#if 0
- if (lex_tok == 256)
- fprintf(stderr, "STR in line %d: >>%s<<\n", lex_line, lex_str.c_str());
- else if (tok >= 32 && tok < 255)
- fprintf(stderr, "CHAR in line %d: >>%c<<\n", lex_line, lex_tok);
- else
- fprintf(stderr, "CHAR in line %d: %d\n", lex_line, lex_tok);
-#endif
- return tok;
-}
-
-static int lex(FILE *f)
-{
- int ch = getc(f);
-
- while (ch == ' ' || ch == '\t' || ch == '\n') {
- if (ch == '\n')
- lex_line++;
- ch = getc(f);
- }
-
- if (ch <= 0 || 255 < ch)
- return token(lex_tok);
-
- if (('a' <= ch && ch <= 'z') || ('A' <= ch && ch <= 'Z') ||
- ('0' <= ch && ch <= '9') || ch == '_' || ch == '\'') {
- lex_str = char(ch);
- while (1) {
- ch = getc(f);
- if (('a' <= ch && ch <= 'z') || ('A' <= ch && ch <= 'Z') ||
- ('0' <= ch && ch <= '9') || ch == '_' || ch == '\'') {
- lex_str += char(ch);
- continue;
- }
- break;
- }
- ungetc(ch, f);
- return token(256);
- }
-
- if (ch == '/') {
- ch = getc(f);
- if (ch == '/') {
- while (ch != '\n')
- ch = getc(f);
- ungetc(ch, f);
- return lex(f);
- }
- ungetc(ch, f);
- return token('/');
- }
-
- return token(ch);
-}
-
-RTLIL::Design *abc_parse_verilog(FILE *f)
-{
- RTLIL::Design *design = new RTLIL::Design;
- RTLIL::Module *module;
- RTLIL::Wire *wire;
- RTLIL::Cell *cell;
-
- int port_count = 1;
- lex_line = 1;
-
- // parse module header
- if (lex(f) != 256 || lex_str != "module")
- goto error;
- if (lex(f) != 256)
- goto error;
-
- module = new RTLIL::Module;
- module->name = "\\" + lex_str;
- design->modules[module->name] = module;
-
- if (lex(f) != '(')
- goto error;
- while (lex(f) != ')') {
- if (lex_tok != 256 && lex_tok != ',')
- goto error;
- }
- if (lex(f) != ';')
- goto error;
-
- // parse module body
- while (1)
- {
- if (lex(f) != 256)
- goto error;
-
- if (lex_str == "endmodule")
- return design;
-
- if (lex_str == "input" || lex_str == "output" || lex_str == "wire")
- {
- std::string mode = lex_str;
- while (lex(f) != ';') {
- if (lex_tok != 256 && lex_tok != ',')
- goto error;
- if (lex_tok == 256) {
- // printf("%s [%s]\n", mode.c_str(), lex_str.c_str());
- wire = new RTLIL::Wire;
- wire->name = "\\" + lex_str;
- if (mode == "input") {
- wire->port_id = port_count++;
- wire->port_input = true;
- }
- if (mode == "output") {
- wire->port_id = port_count++;
- wire->port_output = true;
- }
- module->wires[wire->name] = wire;
- }
- }
- }
- else if (lex_str == "assign")
- {
- std::string lhs, rhs;
-
- if (lex(f) != 256)
- goto error;
- lhs = lex_str;
-
- if (lex(f) != '=')
- goto error;
- if (lex(f) != 256)
- goto error;
- rhs = lex_str;
-
- if (lex(f) != ';')
- goto error;
-
- if (module->wires.count(RTLIL::escape_id(lhs)) == 0)
- goto error;
-
- if (rhs == "1'b0")
- module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), RTLIL::SigSpec(0, 1)));
- else if (rhs == "1'b1")
- module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), RTLIL::SigSpec(1, 1)));
- else if (module->wires.count(RTLIL::escape_id(rhs)) > 0)
- module->connections.push_back(RTLIL::SigSig(module->wires.at(RTLIL::escape_id(lhs)), module->wires.at(RTLIL::escape_id(rhs))));
- else
- goto error;
- }
- else
- {
- std::string cell_type = lex_str;
-
- if (lex(f) != 256)
- goto error;
-
- std::string cell_name = lex_str;
-
- if (lex(f) != '(')
- goto error;
-
- // printf("cell [%s] [%s]\n", cell_type.c_str(), cell_name.c_str());
- cell = new RTLIL::Cell;
- cell->type = "\\" + cell_type;
- cell->name = "\\" + cell_name;
- module->cells[cell->name] = cell;
-
- lex(f);
- while (lex_tok != ')')
- {
- if (lex_tok != '.' || lex(f) != 256)
- goto error;
-
- std::string cell_port = lex_str;
-
- if (lex(f) != '(' || lex(f) != 256)
- goto error;
-
- std::string wire_name = lex_str;
-
- // printf(" [%s] <- [%s]\n", cell_port.c_str(), wire_name.c_str());
- if (module->wires.count("\\" + wire_name) == 0)
- goto error;
- cell->connections["\\" + cell_port] = RTLIL::SigSpec(module->wires["\\" + wire_name]);
-
- if (lex(f) != ')' || (lex(f) != ',' && lex_tok != ')'))
- goto error;
- while (lex_tok == ',')
- lex(f);
- }
-
- if (lex(f) != ';')
- goto error;
- }
- }
-
-error:
- log_error("Syntax error in line %d!\n", lex_line);
- // delete design;
- // return NULL;
-}
-
diff --git a/passes/abc/vlparse.h b/passes/abc/vlparse.h
deleted file mode 100644
index 9514c4190..000000000
--- a/passes/abc/vlparse.h
+++ /dev/null
@@ -1,28 +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.
- *
- */
-
-#ifndef ABC_VLPARSE
-#define ABC_VLPARSE
-
-#include "kernel/rtlil.h"
-
-extern RTLIL::Design *abc_parse_verilog(FILE *f);
-
-#endif
-
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index a582de56d..519dce452 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -69,17 +69,30 @@ struct RenamePass : public Pass {
log("Assign short auto-generated names to all selected wires and cells with private\n");
log("names.\n");
log("\n");
+ log(" rename -hide [selection]\n");
+ log("\n");
+ log("Assign private names (the ones with $-prefix) to all selected wires and cells\n");
+ log("with public names. This ignores all selected ports.\n");
+ log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
bool flag_enumerate = false;
+ bool flag_hide = false;
+ bool got_mode = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
std::string arg = args[argidx];
- if (arg == "-enumerate") {
+ if (arg == "-enumerate" && !got_mode) {
flag_enumerate = true;
+ got_mode = true;
+ continue;
+ }
+ if (arg == "-hide" && !got_mode) {
+ flag_hide = true;
+ got_mode = true;
continue;
}
break;
@@ -117,6 +130,36 @@ struct RenamePass : public Pass {
}
}
else
+ if (flag_hide)
+ {
+ extra_args(args, argidx, design);
+
+ for (auto &mod : design->modules)
+ {
+ RTLIL::Module *module = mod.second;
+ if (!design->selected(module))
+ continue;
+
+ std::map<RTLIL::IdString, RTLIL::Wire*> new_wires;
+ for (auto &it : module->wires) {
+ if (design->selected(module, it.second))
+ if (it.first[0] == '\\' && it.second->port_id == 0)
+ it.second->name = NEW_ID;
+ new_wires[it.second->name] = it.second;
+ }
+ module->wires.swap(new_wires);
+
+ std::map<RTLIL::IdString, RTLIL::Cell*> new_cells;
+ for (auto &it : module->cells) {
+ if (design->selected(module, it.second))
+ if (it.first[0] == '\\')
+ it.second->name = NEW_ID;
+ new_cells[it.second->name] = it.second;
+ }
+ module->cells.swap(new_cells);
+ }
+ }
+ else
{
if (argidx+2 != args.size())
log_cmd_error("Invalid number of arguments!\n");
diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc
index 137f8618a..ec560772e 100644
--- a/passes/cmds/select.cc
+++ b/passes/cmds/select.cc
@@ -272,6 +272,21 @@ static int select_op_expand(RTLIL::Design *design, RTLIL::Selection &lhs, std::v
if (lhs.selected_member(mod_it.first, it.first) && limits.count(it.first) == 0)
selected_wires.insert(it.second);
+ for (auto &conn : mod->connections)
+ {
+ std::vector<RTLIL::SigBit> conn_lhs = conn.first.to_sigbit_vector();
+ std::vector<RTLIL::SigBit> conn_rhs = conn.second.to_sigbit_vector();
+
+ for (size_t i = 0; i < conn_lhs.size(); i++) {
+ if (conn_lhs[i].wire == NULL || conn_rhs[i].wire == NULL)
+ continue;
+ if (mode != 'i' && selected_wires.count(conn_rhs[i].wire) && lhs.selected_members[mod->name].count(conn_lhs[i].wire->name) == 0)
+ lhs.selected_members[mod->name].insert(conn_lhs[i].wire->name), sel_objects++, max_objects--;
+ if (mode != 'o' && selected_wires.count(conn_lhs[i].wire) && lhs.selected_members[mod->name].count(conn_rhs[i].wire->name) == 0)
+ lhs.selected_members[mod->name].insert(conn_rhs[i].wire->name), sel_objects++, max_objects--;
+ }
+ }
+
for (auto &cell : mod->cells)
for (auto &conn : cell.second->connections)
{
@@ -514,7 +529,10 @@ static void select_stmt(RTLIL::Design *design, std::string arg)
} else {
size_t pos = arg.find('/');
if (pos == std::string::npos) {
- arg_mod = arg;
+ if (arg.find(':') == std::string::npos)
+ arg_mod = arg;
+ else
+ arg_mod = "*", arg_memb = arg;
} else {
arg_mod = arg.substr(0, pos);
arg_memb = arg.substr(pos+1);
diff --git a/passes/extract/extract.cc b/passes/extract/extract.cc
index 0c639aeda..aa21e573a 100644
--- a/passes/extract/extract.cc
+++ b/passes/extract/extract.cc
@@ -499,6 +499,8 @@ struct ExtractPass : public Pass {
solver.addSwappablePorts("$xnor", "\\A", "\\B");
solver.addSwappablePorts("$eq", "\\A", "\\B");
solver.addSwappablePorts("$ne", "\\A", "\\B");
+ solver.addSwappablePorts("$eqx", "\\A", "\\B");
+ solver.addSwappablePorts("$nex", "\\A", "\\B");
solver.addSwappablePorts("$add", "\\A", "\\B");
solver.addSwappablePorts("$mul", "\\A", "\\B");
solver.addSwappablePorts("$logic_and", "\\A", "\\B");
diff --git a/passes/memory/memory_collect.cc b/passes/memory/memory_collect.cc
index ca1a3666f..ad4df228e 100644
--- a/passes/memory/memory_collect.cc
+++ b/passes/memory/memory_collect.cc
@@ -20,9 +20,19 @@
#include "kernel/register.h"
#include "kernel/log.h"
#include <sstream>
+#include <algorithm>
#include <stdlib.h>
#include <assert.h>
+static bool memcells_cmp(RTLIL::Cell *a, RTLIL::Cell *b)
+{
+ if (a->type == "$memrd" && b->type == "$memrd")
+ return a->name < b->name;
+ if (a->type == "$memrd" || b->type == "$memrd")
+ return (a->type == "$memrd") < (b->type == "$memrd");
+ return a->parameters.at("\\PRIORITY").as_int() < b->parameters.at("\\PRIORITY").as_int();
+}
+
static void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory)
{
log("Collecting $memrd and $memwr for memory `%s' in module `%s':\n",
@@ -48,11 +58,18 @@ static void handle_memory(RTLIL::Module *module, RTLIL::Memory *memory)
RTLIL::SigSpec sig_rd_data;
std::vector<std::string> del_cell_ids;
+ std::vector<RTLIL::Cell*> memcells;
- for (auto &cell_it : module->cells)
- {
+ for (auto &cell_it : module->cells) {
RTLIL::Cell *cell = cell_it.second;
+ if ((cell->type == "$memwr" || cell->type == "$memrd") && cell->parameters["\\MEMID"].decode_string() == memory->name)
+ memcells.push_back(cell);
+ }
+
+ std::sort(memcells.begin(), memcells.end(), memcells_cmp);
+ for (auto cell : memcells)
+ {
if (cell->type == "$memwr" && cell->parameters["\\MEMID"].decode_string() == memory->name)
{
wr_ports++;
diff --git a/passes/opt/opt_const.cc b/passes/opt/opt_const.cc
index b7b361e95..0ead97b4e 100644
--- a/passes/opt/opt_const.cc
+++ b/passes/opt/opt_const.cc
@@ -17,8 +17,6 @@
*
*/
-#undef MUX_UNDEF_SEL_TO_UNDEF_RESULTS
-
#include "opt_status.h"
#include "kernel/register.h"
#include "kernel/sigtools.h"
@@ -133,18 +131,19 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
ACTION_DO("\\Y", input.extract(2, 1));
if (input.match(" 0")) ACTION_DO("\\Y", input.extract(2, 1));
if (input.match(" 1")) ACTION_DO("\\Y", input.extract(1, 1));
-#ifdef MUX_UNDEF_SEL_TO_UNDEF_RESULTS
if (input.match("01 ")) ACTION_DO("\\Y", input.extract(0, 1));
- // TODO: "10 " -> replace with "!S" gate
- // TODO: "0 " -> replace with "B AND S" gate
- // TODO: " 1 " -> replace with "A OR S" gate
- // TODO: "1 " -> replace with "B OR !S" gate (?)
- // TODO: " 0 " -> replace with "A AND !S" gate (?)
- if (input.match(" *")) ACTION_DO_Y(x);
-#endif
+ if (input.match("10 ")) {
+ cell->type = "$_INV_";
+ cell->connections["\\A"] = input.extract(0, 1);
+ cell->connections.erase("\\B");
+ cell->connections.erase("\\S");
+ goto next_cell;
+ }
+ if (input.match("01*")) ACTION_DO_Y(x);
+ if (input.match("10*")) ACTION_DO_Y(x);
}
- if (cell->type == "$eq" || cell->type == "$ne")
+ if (cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex")
{
RTLIL::SigSpec a = cell->connections["\\A"];
RTLIL::SigSpec b = cell->connections["\\B"];
@@ -160,22 +159,27 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
assert(a.chunks.size() == b.chunks.size());
for (size_t i = 0; i < a.chunks.size(); i++) {
- if (a.chunks[i].wire == NULL && a.chunks[i].data.bits[0] > RTLIL::State::S1)
- continue;
- if (b.chunks[i].wire == NULL && b.chunks[i].data.bits[0] > RTLIL::State::S1)
+ if (a.chunks[i].wire == NULL && b.chunks[i].wire == NULL && a.chunks[i].data.bits[0] != b.chunks[i].data.bits[0] &&
+ a.chunks[i].data.bits[0] <= RTLIL::State::S1 && b.chunks[i].data.bits[0] <= RTLIL::State::S1) {
+ RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ? RTLIL::State::S0 : RTLIL::State::S1);
+ new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
+ replace_cell(module, cell, "empty", "\\Y", new_y);
+ goto next_cell;
+ }
+ if (a.chunks[i] == b.chunks[i])
continue;
new_a.append(a.chunks[i]);
new_b.append(b.chunks[i]);
}
if (new_a.width == 0) {
- RTLIL::SigSpec new_y = RTLIL::SigSpec(cell->type == "$eq" ? RTLIL::State::S1 : RTLIL::State::S0);
+ RTLIL::SigSpec new_y = RTLIL::SigSpec((cell->type == "$eq" || cell->type == "$eqx") ? RTLIL::State::S1 : RTLIL::State::S0);
new_y.extend(cell->parameters["\\Y_WIDTH"].as_int(), false);
replace_cell(module, cell, "empty", "\\Y", new_y);
goto next_cell;
}
- if (new_a.width != a.width) {
+ if (new_a.width < a.width || new_b.width < b.width) {
new_a.optimize();
new_b.optimize();
cell->connections["\\A"] = new_a;
diff --git a/passes/proc/proc_arst.cc b/passes/proc/proc_arst.cc
index 65dc97bdd..571946573 100644
--- a/passes/proc/proc_arst.cc
+++ b/passes/proc/proc_arst.cc
@@ -47,7 +47,7 @@ static bool check_signal(RTLIL::Module *mod, RTLIL::SigSpec signal, RTLIL::SigSp
polarity = !polarity;
return check_signal(mod, cell->connections["\\A"], ref, polarity);
}
- if (cell->type == "$eq" && cell->connections["\\Y"] == signal) {
+ if ((cell->type == "$eq" || cell->type == "$eqx") && cell->connections["\\Y"] == signal) {
if (cell->connections["\\A"].is_fully_const()) {
if (!cell->connections["\\A"].as_bool())
polarity = !polarity;
@@ -59,7 +59,7 @@ static bool check_signal(RTLIL::Module *mod, RTLIL::SigSpec signal, RTLIL::SigSp
return check_signal(mod, cell->connections["\\A"], ref, polarity);
}
}
- if (cell->type == "$ne" && cell->connections["\\Y"] == signal) {
+ if ((cell->type == "$ne" || cell->type == "$nex") && cell->connections["\\Y"] == signal) {
if (cell->connections["\\A"].is_fully_const()) {
if (cell->connections["\\A"].as_bool())
polarity = !polarity;
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 5d0d35b69..5d36b474c 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -148,7 +148,7 @@ struct VlogHammerReporter
ezDefaultSAT ez;
SigMap sigmap(module);
- SatGen satgen(&ez, design, &sigmap);
+ SatGen satgen(&ez, &sigmap);
satgen.model_undef = model_undef;
for (auto &c : module->cells)
diff --git a/passes/sat/freduce.cc b/passes/sat/freduce.cc
index d57fdd321..4b868b3c9 100644
--- a/passes/sat/freduce.cc
+++ b/passes/sat/freduce.cc
@@ -28,337 +28,466 @@
#include <string.h>
#include <algorithm>
-#define NUM_INITIAL_RANDOM_TEST_VECTORS 10
-
namespace {
-struct FreduceHelper
+bool inv_mode;
+int verbose_level;
+typedef std::map<RTLIL::SigBit, std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>>> drivers_t;
+
+struct equiv_bit_t
{
- RTLIL::Design *design;
- RTLIL::Module *module;
- bool try_mode;
+ int depth;
+ bool inverted;
+ RTLIL::Cell *drv;
+ RTLIL::SigBit bit;
+
+ bool operator<(const equiv_bit_t &other) const {
+ if (depth != other.depth)
+ return depth < other.depth;
+ if (inverted != other.inverted)
+ return inverted < other.inverted;
+ if (drv != other.drv)
+ return drv < other.drv;
+ return bit < other.bit;
+ }
+};
+
+struct FindReducedInputs
+{
+ SigMap &sigmap;
+ drivers_t &drivers;
ezDefaultSAT ez;
- SigMap sigmap;
- CellTypes ct;
+ std::set<RTLIL::Cell*> ez_cells;
SatGen satgen;
- ConstEval ce;
- SigPool inputs, nodes;
- RTLIL::SigSpec input_sigs;
-
- SigSet<RTLIL::SigSpec> source_signals;
- std::vector<RTLIL::Const> test_vectors;
- std::map<RTLIL::SigSpec, RTLIL::Const> node_to_data;
- std::map<RTLIL::SigSpec, RTLIL::SigSpec> node_result;
-
- uint32_t xorshift32_state;
-
- uint32_t xorshift32() {
- xorshift32_state ^= xorshift32_state << 13;
- xorshift32_state ^= xorshift32_state >> 17;
- xorshift32_state ^= xorshift32_state << 5;
- return xorshift32_state;
+ FindReducedInputs(SigMap &sigmap, drivers_t &drivers) :
+ sigmap(sigmap), drivers(drivers), satgen(&ez, &sigmap)
+ {
+ satgen.model_undef = true;
}
- FreduceHelper(RTLIL::Design *design, RTLIL::Module *module, bool try_mode) :
- design(design), module(module), try_mode(try_mode),
- sigmap(module), satgen(&ez, design, &sigmap), ce(module)
+ void register_cone_worker(std::set<RTLIL::SigBit> &pi, std::set<RTLIL::SigBit> &sigdone, RTLIL::SigBit out)
{
- ct.setup_internals();
- ct.setup_stdcells();
+ if (out.wire == NULL)
+ return;
+ if (sigdone.count(out) != 0)
+ return;
+ sigdone.insert(out);
+
+ if (drivers.count(out) != 0) {
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+ if (ez_cells.count(drv.first) == 0) {
+ satgen.setContext(&sigmap, "A");
+ if (!satgen.importCell(drv.first))
+ log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+ satgen.setContext(&sigmap, "B");
+ if (!satgen.importCell(drv.first))
+ log_abort();
+ ez_cells.insert(drv.first);
+ }
+ for (auto &bit : drv.second)
+ register_cone_worker(pi, sigdone, bit);
+ } else
+ pi.insert(out);
+ }
- xorshift32_state = 123456789;
- xorshift32();
- xorshift32();
- xorshift32();
+ void register_cone(std::vector<RTLIL::SigBit> &pi, RTLIL::SigBit out)
+ {
+ std::set<RTLIL::SigBit> pi_set, sigdone;
+ register_cone_worker(pi_set, sigdone, out);
+ pi.clear();
+ pi.insert(pi.end(), pi_set.begin(), pi_set.end());
}
- bool run_test(RTLIL::SigSpec test_vec)
+ void analyze(std::vector<RTLIL::SigBit> &reduced_inputs, RTLIL::SigBit output)
{
- ce.clear();
- ce.set(input_sigs, test_vec.as_const());
-
- for (auto &bit : nodes.bits) {
- RTLIL::SigSpec nodesig(bit.first, 1, bit.second), nodeval = nodesig;
- if (!ce.eval(nodeval)) {
- if (!try_mode)
- log_error("Evaluation of node %s failed!\n", log_signal(nodesig));
- log("FAILED: Evaluation of node %s failed!\n", log_signal(nodesig));
- return false;
+ if (verbose_level >= 1)
+ log(" Analyzing input cone for signal %s:\n", log_signal(output));
+
+ std::vector<RTLIL::SigBit> pi;
+ register_cone(pi, output);
+
+ if (verbose_level >= 1)
+ log(" Found %d input signals and %d cells.\n", int(pi.size()), int(ez_cells.size()));
+
+ satgen.setContext(&sigmap, "A");
+ int output_a = satgen.importSigSpec(output).front();
+ int output_undef_a = satgen.importUndefSigSpec(output).front();
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+ satgen.setContext(&sigmap, "B");
+ int output_b = satgen.importSigSpec(output).front();
+ int output_undef_b = satgen.importUndefSigSpec(output).front();
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, satgen.importUndefSigSpec(pi))));
+
+ for (size_t i = 0; i < pi.size(); i++)
+ {
+ RTLIL::SigSpec test_sig(pi[i]);
+ RTLIL::SigSpec rest_sig(pi);
+ rest_sig.remove(i, 1);
+
+ int test_sig_a, test_sig_b;
+ std::vector<int> rest_sig_a, rest_sig_b;
+
+ satgen.setContext(&sigmap, "A");
+ test_sig_a = satgen.importSigSpec(test_sig).front();
+ rest_sig_a = satgen.importSigSpec(rest_sig);
+
+ satgen.setContext(&sigmap, "B");
+ test_sig_b = satgen.importSigSpec(test_sig).front();
+ rest_sig_b = satgen.importSigSpec(rest_sig);
+
+ if (ez.solve(ez.vec_eq(rest_sig_a, rest_sig_b), ez.XOR(output_a, output_b), ez.XOR(test_sig_a, test_sig_b), ez.NOT(output_undef_a), ez.NOT(output_undef_b))) {
+ if (verbose_level >= 2)
+ log(" Result for input %s: pass\n", log_signal(test_sig));
+ reduced_inputs.push_back(pi[i]);
+ } else {
+ if (verbose_level >= 2)
+ log(" Result for input %s: strip\n", log_signal(test_sig));
}
- node_to_data[nodesig].bits.push_back(nodeval.as_const().bits.at(0));
}
- return true;
+ if (verbose_level >= 1)
+ log(" Reduced input cone contains %d inputs.\n", int(reduced_inputs.size()));
}
+};
- void dump_node_data()
- {
- int max_node_len = 20;
- for (auto &it : node_to_data)
- max_node_len = std::max(max_node_len, int(strlen(log_signal(it.first))));
- log(" full node fingerprints:\n");
- for (auto &it : node_to_data)
- log(" %-*s %s\n", max_node_len+5, log_signal(it.first), log_signal(it.second));
- }
+struct PerformReduction
+{
+ SigMap &sigmap;
+ drivers_t &drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> &inv_pairs;
- bool check(RTLIL::SigSpec sig1, RTLIL::SigSpec sig2)
+ ezDefaultSAT ez;
+ SatGen satgen;
+
+ std::vector<int> sat_pi, sat_out, sat_def;
+ std::vector<RTLIL::SigBit> out_bits, pi_bits;
+ std::vector<bool> out_inverted;
+ std::vector<int> out_depth;
+
+ int register_cone_worker(std::set<RTLIL::Cell*> &celldone, std::map<RTLIL::SigBit, int> &sigdepth, RTLIL::SigBit out)
{
- log(" performing SAT proof: %s == %s ->", log_signal(sig1), log_signal(sig2));
-
- std::vector<int> vec1 = satgen.importSigSpec(sig1);
- std::vector<int> vec2 = satgen.importSigSpec(sig2);
- std::vector<int> model = satgen.importSigSpec(input_sigs);
- std::vector<bool> testvect;
-
- if (ez.solve(model, testvect, ez.vec_ne(vec1, vec2))) {
- RTLIL::SigSpec testvect_sig;
- for (int i = 0; i < input_sigs.width; i++)
- testvect_sig.append(testvect.at(i) ? RTLIL::State::S1 : RTLIL::State::S0);
- testvect_sig.optimize();
- log(" failed: %s\n", log_signal(testvect_sig));
- test_vectors.push_back(testvect_sig.as_const());
- if (!run_test(testvect_sig))
- return false;
+ if (out.wire == NULL)
+ return 0;
+ if (sigdepth.count(out) != 0)
+ return sigdepth.at(out);
+ sigdepth[out] = 0;
+
+ if (drivers.count(out) != 0) {
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> &drv = drivers.at(out);
+ if (celldone.count(drv.first) == 0) {
+ if (!satgen.importCell(drv.first))
+ log_error("Can't create SAT model for cell %s (%s)!\n", RTLIL::id2cstr(drv.first->name), RTLIL::id2cstr(drv.first->type));
+ celldone.insert(drv.first);
+ }
+ int max_child_dept = 0;
+ for (auto &bit : drv.second)
+ max_child_dept = std::max(register_cone_worker(celldone, sigdepth, bit), max_child_dept);
+ sigdepth[out] = max_child_dept + 1;
} else {
- log(" success.\n");
- if (!sig1.is_fully_const())
- node_result[sig1].append(sig2);
- if (!sig2.is_fully_const())
- node_result[sig2].append(sig1);
+ pi_bits.push_back(out);
+ sat_pi.push_back(satgen.importSigSpec(out).front());
+ ez.assume(ez.NOT(satgen.importUndefSigSpec(out).front()));
}
- return true;
+
+ return sigdepth[out];
}
- bool analyze_const()
+ 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)
{
- for (auto &it : node_to_data)
- {
- if (node_result.count(it.first))
- continue;
- if (it.second == RTLIL::Const(RTLIL::State::S0, it.second.bits.size()))
- if (!check(it.first, RTLIL::SigSpec(RTLIL::State::S0)))
- return false;
- if (it.second == RTLIL::Const(RTLIL::State::S1, it.second.bits.size()))
- if (!check(it.first, RTLIL::SigSpec(RTLIL::State::S1)))
- return false;
+ satgen.model_undef = true;
+
+ std::set<RTLIL::Cell*> celldone;
+ std::map<RTLIL::SigBit, int> sigdepth;
+
+ for (auto &bit : bits) {
+ out_depth.push_back(register_cone_worker(celldone, sigdepth, bit));
+ sat_out.push_back(satgen.importSigSpec(bit).front());
+ sat_def.push_back(ez.NOT(satgen.importUndefSigSpec(bit).front()));
}
- return true;
+
+ 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);
}
- bool analyze_alias()
+ void analyze(std::vector<std::set<int>> &results, std::map<int, int> &results_map, std::vector<int> &bucket, int level)
{
- restart:
- std::map<RTLIL::Const, RTLIL::SigSpec> reverse_map;
+ if (bucket.size() <= 1)
+ return;
- for (auto &it : node_to_data) {
- if (node_result.count(it.first) && node_result.at(it.first).is_fully_const())
- continue;
- reverse_map[it.second].append(it.first);
+ if (verbose_level == 1)
+ log("%*s Trying to shatter bucket with %d signals.\n", 2*level, "", int(bucket.size()));
+
+ if (verbose_level > 1) {
+ std::vector<RTLIL::SigBit> bucket_sigbits;
+ for (int idx : bucket)
+ bucket_sigbits.push_back(out_bits[idx]);
+ RTLIL::SigSpec bucket_sig(bucket_sigbits);
+ bucket_sig.optimize();
+ log("%*s Trying to shatter bucket with %d signals: %s\n", 2*level, "", int(bucket.size()), log_signal(bucket_sig));
}
- for (auto &it : reverse_map)
- {
- if (it.second.width <= 1)
- continue;
+ std::vector<int> sat_list, sat_inv_list;
+ for (int idx : bucket) {
+ sat_list.push_back(ez.AND(sat_out[idx], sat_def[idx]));
+ sat_inv_list.push_back(ez.AND(ez.NOT(sat_out[idx]), sat_def[idx]));
+ }
- it.second.expand();
- for (int i = 0; i < it.second.width; i++)
- for (int j = i+1; j < it.second.width; j++) {
- RTLIL::SigSpec sig1 = it.second.chunks.at(i), sig2 = it.second.chunks.at(j);
- if (node_result.count(sig1) && node_result.count(sig2))
- continue;
- if (node_to_data.at(sig1) != node_to_data.at(sig2))
- goto restart;
- if (!check(it.second.chunks.at(i), it.second.chunks.at(j)))
- return false;
+ std::vector<int> modelVars = sat_out;
+ std::vector<bool> model;
+
+ modelVars.insert(modelVars.end(), sat_def.begin(), sat_def.end());
+ if (verbose_level >= 2)
+ modelVars.insert(modelVars.end(), sat_pi.begin(), sat_pi.end());
+
+ if (ez.solve(modelVars, model, ez.expression(ezSAT::OpOr, sat_list), ez.expression(ezSAT::OpOr, sat_inv_list)))
+ {
+ if (verbose_level >= 2) {
+ for (size_t i = 0; i < pi_bits.size(); i++)
+ log("%*s -> PI %c == %s\n", 2*level, "", model[2*sat_out.size() + i] ? '1' : '0', log_signal(pi_bits[i]));
+ for (int idx : bucket)
+ log("%*s -> OUT %c == %s%s\n", 2*level, "", model[sat_out.size() + idx] ? model[idx] ? '1' : '0' : 'x',
+ out_inverted.at(idx) ? "~" : "", log_signal(out_bits[idx]));
}
- }
- return true;
- }
- bool toproot_helper(RTLIL::SigSpec cursor, RTLIL::SigSpec stoplist, RTLIL::SigSpec &donelist, int level)
- {
- // log(" %*schecking %s: %s\n", level*2, "", log_signal(cursor), log_signal(stoplist));
+ std::vector<int> buckets_a;
+ std::vector<int> buckets_b;
- if (stoplist.extract(cursor).width != 0) {
- // log(" %*s STOP\n", level*2, "");
- return false;
+ for (int idx : bucket) {
+ if (!model[sat_out.size() + idx] || model[idx])
+ buckets_a.push_back(idx);
+ if (!model[sat_out.size() + idx] || !model[idx])
+ buckets_b.push_back(idx);
+ }
+ analyze(results, results_map, buckets_a, level+1);
+ analyze(results, results_map, buckets_b, level+1);
}
+ else
+ {
+ std::vector<int> undef_slaves;
+
+ for (int idx : bucket) {
+ std::vector<int> sat_def_list;
+ for (int idx2 : bucket)
+ if (idx != idx2)
+ sat_def_list.push_back(sat_def[idx2]);
+ if (ez.solve(ez.NOT(sat_def[idx]), ez.expression(ezSAT::OpOr, sat_def_list)))
+ undef_slaves.push_back(idx);
+ }
+
+ if (undef_slaves.size() == bucket.size()) {
+ if (verbose_level >= 1)
+ log("%*s Complex undef overlap. None of the signals covers the others.\n", 2*level, "");
+ // FIXME: We could try to further shatter a group with complex undef overlaps
+ return;
+ }
- if (donelist.extract(cursor).width != 0)
- return true;
+ for (int idx : undef_slaves)
+ out_depth[idx] = std::numeric_limits<int>::max();
- stoplist.append(cursor);
- std::set<RTLIL::SigSpec> next = source_signals.find(cursor);
+ if (verbose_level >= 1) {
+ log("%*s Found %d equivialent signals:", 2*level, "", int(bucket.size()));
+ for (int idx : bucket)
+ log("%s%s%s", idx == bucket.front() ? " " : ", ", out_inverted[idx] ? "~" : "", log_signal(out_bits[idx]));
+ log("\n");
+ }
- for (auto &it : next)
- if (!toproot_helper(it, stoplist, donelist, level+1))
- return false;
+ int result_idx = -1;
+ for (int idx : bucket) {
+ if (results_map.count(idx) == 0)
+ continue;
+ if (result_idx == -1) {
+ result_idx = results_map.at(idx);
+ continue;
+ }
+ int result_idx2 = results_map.at(idx);
+ results[result_idx].insert(results[result_idx2].begin(), results[result_idx2].end());
+ for (int idx2 : results[result_idx2])
+ results_map[idx2] = result_idx;
+ results[result_idx2].clear();
+ }
- donelist.append(cursor);
- return true;
- }
+ if (result_idx == -1) {
+ result_idx = results.size();
+ results.push_back(std::set<int>());
+ }
- // KISS topological sort of bits in signal. return one element of sig
- // without dependencies to the others (or empty if input is not a DAG).
- RTLIL::SigSpec toproot(RTLIL::SigSpec sig)
- {
- sig.expand();
- // log(" finding topological root in %s:\n", log_signal(sig));
- for (auto &c : sig.chunks) {
- RTLIL::SigSpec stoplist = sig, donelist;
- stoplist.remove(c);
- // log(" testing %s as root:\n", log_signal(c));
- if (toproot_helper(c, stoplist, donelist, 0))
- return c;
+ results[result_idx].insert(bucket.begin(), bucket.end());
}
- return RTLIL::SigSpec();
}
- void update_design_for_group(RTLIL::SigSpec root, RTLIL::SigSpec rest)
+ void analyze(std::vector<std::vector<equiv_bit_t>> &results)
{
- SigPool unlink;
- unlink.add(rest);
+ std::vector<int> bucket;
+ for (size_t i = 0; i < sat_out.size(); i++)
+ bucket.push_back(i);
+
+ std::vector<std::set<int>> results_buf;
+ std::map<int, int> results_map;
+ analyze(results_buf, results_map, bucket, 1);
- for (auto &cell_it : module->cells) {
- RTLIL::Cell *cell = cell_it.second;
- if (!ct.cell_known(cell->type))
+ for (auto &r : results_buf)
+ {
+ if (r.size() <= 1)
continue;
- for (auto &conn : cell->connections)
- if (ct.cell_output(cell->type, conn.first)) {
- RTLIL::SigSpec sig = sigmap(conn.second);
- sig.expand();
- bool did_something = false;
- for (auto &c : sig.chunks) {
- if (c.wire == NULL || !unlink.check_any(c))
- continue;
- c.wire = new RTLIL::Wire;
- c.wire->name = NEW_ID;
- module->add(c.wire);
- assert(c.width == 1);
- c.offset = 0;
- did_something = true;
- }
- if (did_something) {
- sig.optimize();
- conn.second = sig;
- }
- }
- }
- rest.expand();
- for (auto &c : rest.chunks) {
- if (c.wire != NULL && !root.is_fully_const()) {
- source_signals.erase(c);
- source_signals.insert(c, root);
+ std::vector<equiv_bit_t> result;
+
+ for (int idx : r) {
+ equiv_bit_t bit;
+ bit.depth = out_depth[idx];
+ bit.inverted = out_inverted[idx];
+ bit.drv = drivers.count(out_bits[idx]) ? drivers.at(out_bits[idx]).first : NULL;
+ bit.bit = out_bits[idx];
+ result.push_back(bit);
}
- module->connections.push_back(RTLIL::SigSig(c, root));
+
+ std::sort(result.begin(), result.end());
+
+ if (result.front().inverted)
+ for (auto &bit : result)
+ bit.inverted = !bit.inverted;
+
+ 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);
}
}
+};
- void analyze_groups()
+struct FreduceWorker
+{
+ RTLIL::Module *module;
+
+ SigMap sigmap;
+ drivers_t drivers;
+ std::set<std::pair<RTLIL::SigBit, RTLIL::SigBit>> inv_pairs;
+
+ FreduceWorker(RTLIL::Module *module) : module(module), sigmap(module)
{
- SigMap to_group_major;
- for (auto &it : node_result) {
- it.second.expand();
- for (auto &c : it.second.chunks)
- to_group_major.add(it.first, c);
- }
+ }
- std::map<RTLIL::SigSpec, RTLIL::SigSpec> major_to_rest;
- for (auto &it : node_result)
- major_to_rest[to_group_major(it.first)].append(it.first);
+ int run()
+ {
+ log("Running functional reduction on module %s:\n", RTLIL::id2cstr(module->name));
- for (auto &it : major_to_rest)
- {
- RTLIL::SigSig group = it;
+ CellTypes ct;
+ ct.setup_internals();
+ ct.setup_stdcells();
- if (!it.first.is_fully_const()) {
- group.first = toproot(it.second);
- if (group.first.width == 0) {
- log("Operating on non-DAG input: failed to find topological root for `%s'.\n", log_signal(it.second));
- return;
+ std::vector<std::set<RTLIL::SigBit>> batches;
+ for (auto &it : module->wires)
+ if (it.second->port_input)
+ batches.push_back(sigmap(it.second).to_sigbit_set());
+ for (auto &it : module->cells) {
+ if (ct.cell_known(it.second->type)) {
+ std::set<RTLIL::SigBit> inputs, outputs;
+ for (auto &port : it.second->connections) {
+ std::vector<RTLIL::SigBit> bits = sigmap(port.second).to_sigbit_vector();
+ if (ct.cell_output(it.second->type, port.first))
+ outputs.insert(bits.begin(), bits.end());
+ else
+ inputs.insert(bits.begin(), bits.end());
}
- group.second.remove(group.first);
+ std::pair<RTLIL::Cell*, std::set<RTLIL::SigBit>> drv(it.second, inputs);
+ for (auto &bit : outputs)
+ 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;
+ buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S0));
+ buckets[std::vector<RTLIL::SigBit>()].push_back(RTLIL::SigBit(RTLIL::State::S1));
+ for (auto &batch : batches)
+ {
+ RTLIL::SigSpec batch_sig(std::vector<RTLIL::SigBit>(batch.begin(), batch.end()));
+ batch_sig.optimize();
- group.first.optimize();
- group.second.sort_and_unify();
+ log(" Finding reduced input cone for signal batch %s%c\n", log_signal(batch_sig), verbose_level ? ':' : '.');
- log(" found group: %s -> %s\n", log_signal(group.first), log_signal(group.second));
- update_design_for_group(group.first, group.second);
+ FindReducedInputs infinder(sigmap, drivers);
+ for (auto &bit : batch) {
+ std::vector<RTLIL::SigBit> inputs;
+ infinder.analyze(inputs, bit);
+ buckets[inputs].push_back(bit);
+ bits_count++;
+ }
}
- }
+ log(" Sorted %d signal bits into %d buckets.\n", bits_count, int(buckets.size()));
- void run()
- {
- log("\nFunctionally reduce module %s:\n", RTLIL::id2cstr(module->name));
-
- // find inputs and nodes (nets driven by internal cells)
- // add all internal cells to sat solver
-
- for (auto &cell_it : module->cells) {
- RTLIL::Cell *cell = cell_it.second;
- if (!ct.cell_known(cell->type))
+ std::vector<std::vector<equiv_bit_t>> equiv;
+ for (auto &bucket : buckets)
+ {
+ if (bucket.second.size() == 1)
continue;
- RTLIL::SigSpec cell_inputs, cell_outputs;
- for (auto &conn : cell->connections)
- if (ct.cell_output(cell->type, conn.first)) {
- nodes.add(sigmap(conn.second));
- cell_outputs.append(sigmap(conn.second));
- } else {
- inputs.add(sigmap(conn.second));
- cell_inputs.append(sigmap(conn.second));
- }
- cell_inputs.sort_and_unify();
- cell_outputs.sort_and_unify();
- cell_inputs.expand();
- for (auto &c : cell_inputs.chunks)
- if (c.wire != NULL)
- source_signals.insert(cell_outputs, c);
- if (!satgen.importCell(cell))
- log_error("Failed to import cell to SAT solver: %s (%s)\n",
- RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
- }
- inputs.del(nodes);
- nodes.add(inputs);
- log(" found %d nodes (%d inputs).\n", int(nodes.size()), int(inputs.size()));
-
- // initialise input_sigs and add all-zero, all-one and a few random test vectors
-
- input_sigs = inputs.export_all();
- test_vectors.push_back(RTLIL::SigSpec(RTLIL::State::S0, input_sigs.width).as_const());
- test_vectors.push_back(RTLIL::SigSpec(RTLIL::State::S1, input_sigs.width).as_const());
-
- for (int i = 0; i < NUM_INITIAL_RANDOM_TEST_VECTORS; i++) {
- RTLIL::SigSpec sig;
- for (int j = 0; j < input_sigs.width; j++)
- sig.append(xorshift32() % 2 ? RTLIL::State::S1 : RTLIL::State::S0);
- sig.optimize();
- assert(sig.width == input_sigs.width);
- test_vectors.push_back(sig.as_const());
- }
- for (auto &test_vec : test_vectors)
- if (!run_test(test_vec))
- return;
+ RTLIL::SigSpec bucket_sig(bucket.second);
+ bucket_sig.optimize();
- // run the analysis and update design
+ log(" Trying to shatter bucket %s%c\n", log_signal(bucket_sig), verbose_level ? ':' : '.');
+ PerformReduction worker(sigmap, drivers, inv_pairs, bucket.second);
+ worker.analyze(equiv);
+ }
- if (!analyze_const())
- return;
+ log(" Rewiring %d equivialent groups:\n", int(equiv.size()));
+ int rewired_sigbits = 0;
+ for (auto &grp : equiv)
+ {
+ log(" Using as master for group: %s\n", log_signal(grp.front().bit));
+
+ RTLIL::SigSpec inv_sig;
+ for (size_t i = 1; i < grp.size(); i++)
+ {
+ 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)
+ sigmap(port.second).replace(grp[i].bit, dummy_wire, &port.second);
+
+ if (grp[i].inverted)
+ {
+ if (inv_sig.width == 0)
+ {
+ inv_sig = module->new_wire(1, NEW_ID);
+
+ RTLIL::Cell *inv_cell = new RTLIL::Cell;
+ inv_cell->name = NEW_ID;
+ inv_cell->type = "$_INV_";
+ inv_cell->connections["\\A"] = grp[0].bit;
+ inv_cell->connections["\\Y"] = inv_sig;
+ module->add(inv_cell);
+ }
- if (!analyze_alias())
- return;
+ module->connections.push_back(RTLIL::SigSig(grp[i].bit, inv_sig));
+ }
+ else
+ module->connections.push_back(RTLIL::SigSig(grp[i].bit, grp[0].bit));
- log(" input vector: %s\n", log_signal(input_sigs));
- for (auto &test_vec : test_vectors)
- log(" test vector: %s\n", log_signal(test_vec));
+ rewired_sigbits++;
+ }
+ }
- dump_node_data();
- analyze_groups();
+ log(" Rewired a total of %d signal bits in module %s.\n", rewired_sigbits, RTLIL::id2cstr(module->name));
+ return rewired_sigbits;
}
};
@@ -374,43 +503,51 @@ struct FreducePass : public Pass {
log("\n");
log("This pass performs functional reduction in the circuit. I.e. if two nodes are\n");
log("equivialent, they are merged to one node and one of the redundant drivers is\n");
- log("removed.\n");
+ log("unconnected. A subsequent call to 'clean' will remove the redundant drivers.\n");
+ log("\n");
+ log("This pass is undef-aware, i.e. it considers don't-care values for detecting\n");
+ log("equivialent nodes.\n");
log("\n");
- log(" -try\n");
- log(" do not issue an error when the analysis fails.\n");
- log(" (usually beacause of logic loops in the design)\n");
+ log(" -v, -vv\n");
+ log(" enable verbose or very verbose output\n");
+ log("\n");
+ log(" -inv\n");
+ log(" enable explicit handling of inverted signals\n");
log("\n");
- // log(" -enable_invert\n");
- // log(" also detect nodes that are inverse to each other.\n");
- // log("\n");
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
- bool enable_invert = false;
- bool try_mode = false;
+ verbose_level = 0;
+ inv_mode = false;
log_header("Executing FREDUCE pass (perform functional reduction).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
- if (args[argidx] == "-enable_invert") {
- enable_invert = true;
+ if (args[argidx] == "-v") {
+ verbose_level = 1;
continue;
}
- if (args[argidx] == "-try") {
- try_mode = true;
+ if (args[argidx] == "-vv") {
+ verbose_level = 2;
+ continue;
+ }
+ if (args[argidx] == "-inv") {
+ inv_mode = true;
continue;
}
break;
}
extra_args(args, argidx, design);
- for (auto &mod_it : design->modules)
- {
+ int bitcount = 0;
+ for (auto &mod_it : design->modules) {
RTLIL::Module *module = mod_it.second;
if (design->selected(module))
- FreduceHelper(design, module, try_mode).run();
+ bitcount += FreduceWorker(module).run();
}
+
+ log("Rewired a total of %d signal bits.\n", bitcount);
}
} FreducePass;
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index e330dfa6d..fef99dfc0 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -44,14 +44,14 @@ struct SatHelper
SatGen satgen;
// additional constraints
- std::vector<std::pair<std::string, std::string>> sets, prove, sets_init;
+ std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
std::map<int, std::vector<std::string>> unsets_at;
// undef constraints
bool enable_undef, set_init_undef;
- std::vector<std::string> sets_def, sets_undef, sets_all_undef;
- std::map<int, std::vector<std::string>> sets_def_at, sets_undef_at, sets_all_undef_at;
+ std::vector<std::string> sets_def, sets_any_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> sets_def_at, sets_any_undef_at, sets_all_undef_at;
// model variables
std::vector<std::string> shows;
@@ -61,7 +61,7 @@ struct SatHelper
bool gotTimeout;
SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef) :
- design(design), module(module), sigmap(module), ct(design), satgen(&ez, design, &sigmap)
+ design(design), module(module), sigmap(module), ct(design), satgen(&ez, &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
@@ -202,6 +202,71 @@ struct SatHelper
check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
ez.assume(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ // 0 = sets_def
+ // 1 = sets_any_undef
+ // 2 = sets_all_undef
+ std::set<RTLIL::SigSpec> sets_def_undef[3];
+
+ for (auto &s : sets_def) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ }
+
+ for (auto &s : sets_any_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[1].insert(sig);
+ }
+
+ for (auto &s : sets_all_undef) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (auto &s : sets_def_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].insert(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_any_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].insert(sig);
+ sets_def_undef[2].erase(sig);
+ }
+
+ for (auto &s : sets_all_undef_at[timestep]) {
+ RTLIL::SigSpec sig;
+ if (!RTLIL::SigSpec::parse(sig, module, s))
+ log_cmd_error("Failed to parse set-def expression `%s'.\n", s.c_str());
+ sets_def_undef[0].erase(sig);
+ sets_def_undef[1].erase(sig);
+ sets_def_undef[2].insert(sig);
+ }
+
+ for (int t = 0; t < 3; t++)
+ for (auto &sig : sets_def_undef[t]) {
+ log("Import %s constraint for timestep: %s\n", t == 0 ? "def" : t == 1 ? "any_undef" : "all_undef", log_signal(sig));
+ std::vector<int> undef_sig = satgen.importUndefSigSpec(sig, timestep);
+ if (t == 0)
+ ez.assume(ez.NOT(ez.expression(ezSAT::OpOr, undef_sig)));
+ if (t == 1)
+ ez.assume(ez.expression(ezSAT::OpOr, undef_sig));
+ if (t == 2)
+ ez.assume(ez.expression(ezSAT::OpAnd, undef_sig));
+ }
+
int import_cell_counter = 0;
for (auto &c : module->cells)
if (design->selected(module, c.second)) {
@@ -219,34 +284,75 @@ struct SatHelper
int setup_proof(int timestep = -1)
{
- assert(prove.size() > 0);
+ assert(prove.size() + prove_x.size() > 0);
RTLIL::SigSpec big_lhs, big_rhs;
+ std::vector<int> prove_bits;
- for (auto &s : prove)
+ if (prove.size() > 0)
{
- RTLIL::SigSpec lhs, rhs;
+ for (auto &s : prove)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.width != rhs.width)
+ log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+ log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
- if (!RTLIL::SigSpec::parse(lhs, module, s.first))
- log_cmd_error("Failed to parse lhs proof expression `%s'.\n", s.first.c_str());
- if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
- log_cmd_error("Failed to parse rhs proof expression `%s'.\n", s.second.c_str());
- show_signal_pool.add(sigmap(lhs));
- show_signal_pool.add(sigmap(rhs));
+ log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+ check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
+ prove_bits.push_back(satgen.signals_eq(big_lhs, big_rhs, timestep));
+ }
- if (lhs.width != rhs.width)
- log_cmd_error("Proof expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
- s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+ if (prove_x.size() > 0)
+ {
+ for (auto &s : prove_x)
+ {
+ RTLIL::SigSpec lhs, rhs;
+
+ if (!RTLIL::SigSpec::parse(lhs, module, s.first))
+ log_cmd_error("Failed to parse lhs proof-x expression `%s'.\n", s.first.c_str());
+ if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
+ log_cmd_error("Failed to parse rhs proof-x expression `%s'.\n", s.second.c_str());
+ show_signal_pool.add(sigmap(lhs));
+ show_signal_pool.add(sigmap(rhs));
+
+ if (lhs.width != rhs.width)
+ log_cmd_error("Proof-x expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
+ s.first.c_str(), log_signal(lhs), lhs.width, s.second.c_str(), log_signal(rhs), rhs.width);
+
+ log("Import proof-x-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
+ big_lhs.remove2(lhs, &big_rhs);
+ big_lhs.append(lhs);
+ big_rhs.append(rhs);
+ }
- log("Import proof-constraint: %s = %s\n", log_signal(lhs), log_signal(rhs));
- big_lhs.remove2(lhs, &big_rhs);
- big_lhs.append(lhs);
- big_rhs.append(rhs);
+ log("Final proof-x equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
+
+ std::vector<int> value_lhs = satgen.importDefSigSpec(big_lhs, timestep);
+ std::vector<int> value_rhs = satgen.importDefSigSpec(big_rhs, timestep);
+
+ std::vector<int> undef_lhs = satgen.importUndefSigSpec(big_lhs, timestep);
+ std::vector<int> undef_rhs = satgen.importUndefSigSpec(big_rhs, timestep);
+
+ for (size_t i = 0; i < value_lhs.size(); i++)
+ prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
}
- log("Final proof equation: %s = %s\n", log_signal(big_lhs), log_signal(big_rhs));
- check_undef_enabled(big_lhs), check_undef_enabled(big_rhs);
- return satgen.signals_eq(big_lhs, big_rhs, timestep);
+ return ez.expression(ezSAT::OpAnd, prove_bits);
}
void force_unique_state(int timestep_from, int timestep_to)
@@ -567,17 +673,18 @@ struct SatPass : public Pass {
log(" -set <signal> <value>\n");
log(" set the specified signal to the specified value.\n");
log("\n");
- #if 0
log(" -set-def <signal>\n");
log(" add a constraint that all bits of the given signal must be defined\n");
log("\n");
- log(" -set-undef <signal>\n");
+ log(" -set-any-undef <signal>\n");
log(" add a constraint that at least one bit of the given signal is undefined\n");
log("\n");
log(" -set-all-undef <signal>\n");
log(" add a constraint that all bits of the given signal are undefined\n");
log("\n");
- #endif
+ log(" -set-def-inputs\n");
+ log(" add -set-def constraints for all module inputs\n");
+ log("\n");
log(" -show <signal>\n");
log(" show the model for the specified signal. if no -show option is\n");
log(" passed then a set of signals to be shown is automatically selected.\n");
@@ -596,13 +703,11 @@ struct SatPass : public Pass {
log(" set or unset the specified signal to the specified value in the\n");
log(" given timestep. this has priority over a -set for the same signal.\n");
log("\n");
- #if 0
- log(" -set-def <N> <signal>\n");
- log(" -set-undef <N> <signal>\n");
- log(" -set-all-undef <N> <signal>\n");
+ log(" -set-def-at <N> <signal>\n");
+ log(" -set-any-undef-at <N> <signal>\n");
+ log(" -set-all-undef-at <N> <signal>\n");
log(" add undef contraints in the given timestep.\n");
log("\n");
- #endif
log(" -set-init <signal> <value>\n");
log(" set the initial value for the register driving the signal to the value\n");
log("\n");
@@ -617,6 +722,10 @@ struct SatPass : public Pass {
log(" induction proof it is proven that the condition holds forever after\n");
log(" the number of time steps passed using -seq.\n");
log("\n");
+ log(" -prove-x <signal> <value>\n");
+ log(" Like -prove, but an undef (x) bit in the lhs matches any value on\n");
+ log(" the right hand side. Useful for equivialence checking.\n");
+ log("\n");
log(" -maxsteps <N>\n");
log(" Set a maximum length for the induction.\n");
log("\n");
@@ -632,13 +741,13 @@ struct SatPass : public Pass {
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
{
- std::vector<std::pair<std::string, std::string>> sets, sets_init, prove;
+ std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
- std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_undef_at, sets_all_undef_at;
- std::vector<std::string> shows, sets_def, sets_undef, sets_all_undef;
+ std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
+ std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
- bool verify = false, fail_on_timeout = false, enable_undef = false;
- bool ignore_div_by_zero = false, set_init_undef = false, max_undef = true;
+ bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
+ bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
@@ -682,23 +791,28 @@ struct SatPass : public Pass {
max_undef = true;
continue;
}
+ if (args[argidx] == "-set-def-inputs") {
+ enable_undef = true;
+ set_def_inputs = true;
+ continue;
+ }
if (args[argidx] == "-set" && argidx+2 < args.size()) {
std::string lhs = args[++argidx];
std::string rhs = args[++argidx];
sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
continue;
}
- if (args[argidx] == "-set-def" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
sets_def.push_back(args[++argidx]);
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-undef" && argidx+2 < args.size()) {
- sets_undef.push_back(args[++argidx]);
+ if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
+ sets_any_undef.push_back(args[++argidx]);
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-all-undef" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
sets_all_undef.push_back(args[++argidx]);
enable_undef = true;
continue;
@@ -709,6 +823,13 @@ struct SatPass : public Pass {
prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
continue;
}
+ if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
+ std::string lhs = args[++argidx];
+ std::string rhs = args[++argidx];
+ prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
+ enable_undef = true;
+ continue;
+ }
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
seq_len = atoi(args[++argidx].c_str());
continue;
@@ -731,9 +852,9 @@ struct SatPass : public Pass {
enable_undef = true;
continue;
}
- if (args[argidx] == "-set-undef-at" && argidx+2 < args.size()) {
+ if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
int timestep = atoi(args[++argidx].c_str());
- sets_undef_at[timestep].push_back(args[++argidx]);
+ sets_any_undef_at[timestep].push_back(args[++argidx]);
enable_undef = true;
continue;
}
@@ -773,10 +894,16 @@ struct SatPass : public Pass {
if (module == NULL)
log_cmd_error("Can't perform SAT on an empty selection!\n");
- if (prove.size() == 0 && verify)
+ if (prove.size() + prove_x.size() == 0 && verify)
log_cmd_error("Got -verify but nothing to prove!\n");
- if (prove.size() > 0 && seq_len > 0)
+ if (set_def_inputs) {
+ for (auto &it : module->wires)
+ if (it.second->port_input)
+ sets_def.push_back(it.second->name);
+ }
+
+ if (prove.size() + prove_x.size() > 0 && seq_len > 0)
{
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -786,15 +913,16 @@ struct SatPass : public Pass {
basecase.sets = sets;
basecase.prove = prove;
+ basecase.prove_x = prove_x;
basecase.sets_at = sets_at;
basecase.unsets_at = unsets_at;
basecase.shows = shows;
basecase.timeout = timeout;
basecase.sets_def = sets_def;
- basecase.sets_undef = sets_undef;
+ basecase.sets_any_undef = sets_any_undef;
basecase.sets_all_undef = sets_all_undef;
basecase.sets_def_at = sets_def_at;
- basecase.sets_undef_at = sets_undef_at;
+ basecase.sets_any_undef_at = sets_any_undef_at;
basecase.sets_all_undef_at = sets_all_undef_at;
basecase.sets_init = sets_init;
basecase.set_init_undef = set_init_undef;
@@ -806,16 +934,12 @@ struct SatPass : public Pass {
inductstep.sets = sets;
inductstep.prove = prove;
+ inductstep.prove_x = prove_x;
inductstep.shows = shows;
inductstep.timeout = timeout;
inductstep.sets_def = sets_def;
- inductstep.sets_undef = sets_undef;
+ inductstep.sets_any_undef = sets_any_undef;
inductstep.sets_all_undef = sets_all_undef;
- inductstep.sets_def_at = sets_def_at;
- inductstep.sets_undef_at = sets_undef_at;
- inductstep.sets_all_undef_at = sets_all_undef_at;
- inductstep.sets_init = sets_init;
- inductstep.set_init_undef = set_init_undef;
inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
inductstep.setup(1);
@@ -896,15 +1020,16 @@ struct SatPass : public Pass {
sathelper.sets = sets;
sathelper.prove = prove;
+ sathelper.prove_x = prove_x;
sathelper.sets_at = sets_at;
sathelper.unsets_at = unsets_at;
sathelper.shows = shows;
sathelper.timeout = timeout;
sathelper.sets_def = sets_def;
- sathelper.sets_undef = sets_undef;
+ sathelper.sets_any_undef = sets_any_undef;
sathelper.sets_all_undef = sets_all_undef;
sathelper.sets_def_at = sets_def_at;
- sathelper.sets_undef_at = sets_undef_at;
+ sathelper.sets_any_undef_at = sets_any_undef_at;
sathelper.sets_all_undef_at = sets_all_undef_at;
sathelper.sets_init = sets_init;
sathelper.set_init_undef = set_init_undef;
@@ -912,7 +1037,7 @@ struct SatPass : public Pass {
if (seq_len == 0) {
sathelper.setup();
- if (sathelper.prove.size() > 0)
+ if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
} else {
for (int timestep = 1; timestep <= seq_len; timestep++)
@@ -939,7 +1064,7 @@ struct SatPass : public Pass {
sathelper.maximize_undefs();
}
- if (prove.size() == 0) {
+ if (prove.size() + prove_x.size() == 0) {
log("SAT solving finished - model found:\n");
} else {
log("SAT proof finished - model found: FAIL!\n");
@@ -965,7 +1090,7 @@ struct SatPass : public Pass {
goto timeout;
if (rerun_counter)
log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
- else if (prove.size() == 0)
+ else if (prove.size() + prove_x.size() == 0)
log("SAT solving finished - no model found.\n");
else {
log("SAT proof finished - no model found: SUCCESS!\n");
diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index 0324afa84..40caf7801 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -106,6 +106,7 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
LibertyAst *best_cell = NULL;
std::map<std::string, char> best_cell_ports;
int best_cell_pins = 0;
+ float best_cell_area = 0;
if (ast->id != "library")
log_error("Format error in liberty file.\n");
@@ -141,6 +142,11 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
this_cell_ports[cell_rst_pin] = 'R';
this_cell_ports[cell_next_pin] = 'D';
+ float area = 0;
+ LibertyAst *ar = cell->find("area");
+ if (ar != NULL && !ar->value.empty())
+ area = atof(ar->value.c_str());
+
int num_pins = 0;
bool found_output = false;
for (auto pin : cell->children)
@@ -174,14 +180,18 @@ static void find_cell(LibertyAst *ast, std::string cell_type, bool clkpol, bool
if (!found_output || (best_cell != NULL && num_pins > best_cell_pins))
continue;
+ if (best_cell != NULL && num_pins == best_cell_pins && area > best_cell_area)
+ continue;
+
best_cell = cell;
best_cell_pins = num_pins;
+ best_cell_area = area;
best_cell_ports.swap(this_cell_ports);
continue_cell_loop:;
}
if (best_cell != NULL) {
- log(" cell %s is a direct match for cell type %s.\n", best_cell->args[0].c_str(), cell_type.substr(1).c_str());
+ log(" cell %s (pins=%d, area=%.2f) is a direct match for cell type %s.\n", best_cell->args[0].c_str(), best_cell_pins, best_cell_area, cell_type.substr(1).c_str());
cell_mappings[cell_type].cell_name = best_cell->args[0];
cell_mappings[cell_type].ports = best_cell_ports;
}
@@ -192,6 +202,7 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
LibertyAst *best_cell = NULL;
std::map<std::string, char> best_cell_ports;
int best_cell_pins = 0;
+ float best_cell_area = 0;
if (ast->id != "library")
log_error("Format error in liberty file.\n");
@@ -223,6 +234,11 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
this_cell_ports[cell_clr_pin] = 'R';
this_cell_ports[cell_next_pin] = 'D';
+ float area = 0;
+ LibertyAst *ar = cell->find("area");
+ if (ar != NULL && !ar->value.empty())
+ area = atof(ar->value.c_str());
+
int num_pins = 0;
bool found_output = false;
for (auto pin : cell->children)
@@ -256,14 +272,18 @@ static void find_cell_sr(LibertyAst *ast, std::string cell_type, bool clkpol, bo
if (!found_output || (best_cell != NULL && num_pins > best_cell_pins))
continue;
+ if (best_cell != NULL && num_pins == best_cell_pins && area > best_cell_area)
+ continue;
+
best_cell = cell;
best_cell_pins = num_pins;
+ best_cell_area = area;
best_cell_ports.swap(this_cell_ports);
continue_cell_loop:;
}
if (best_cell != NULL) {
- log(" cell %s is a direct match for cell type %s.\n", best_cell->args[0].c_str(), cell_type.substr(1).c_str());
+ log(" cell %s (pins=%d, area=%.2f) is a direct match for cell type %s.\n", best_cell->args[0].c_str(), best_cell_pins, best_cell_area, cell_type.substr(1).c_str());
cell_mappings[cell_type].cell_name = best_cell->args[0];
cell_mappings[cell_type].ports = best_cell_ports;
}
@@ -399,6 +419,7 @@ static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module)
if (port.second == '0' || port.second == '1') {
sig = RTLIL::SigSpec(port.second == '0' ? 0 : 1, 1);
} else
+ if (port.second != 0)
log_abort();
new_cell->connections["\\" + port.first] = sig;
}
@@ -473,16 +494,26 @@ struct DfflibmapPass : public Pass {
find_cell_sr(libparser.ast, "$_DFFSR_PPN_", true, true, false);
find_cell_sr(libparser.ast, "$_DFFSR_PPP_", true, true, true);
- bool keep_running = true;
- while (keep_running) {
- keep_running = false;
- keep_running |= expand_cellmap("$_DFF_*_", "C");
- keep_running |= expand_cellmap("$_DFF_*??_", "C");
- keep_running |= expand_cellmap("$_DFF_?*?_", "R");
- keep_running |= expand_cellmap("$_DFF_??*_", "DQ");
- keep_running |= expand_cellmap("$_DFFSR_*??_", "C");
- keep_running |= expand_cellmap("$_DFFSR_?*?_", "S");
- keep_running |= expand_cellmap("$_DFFSR_??*_", "R");
+ // try to implement as many cells as possible just by inverting
+ // the SET and RESET pins. If necessary, implement cell types
+ // by inverting both D and Q. Only invert clock pins if there
+ // is no other way of implementing the cell.
+ while (1)
+ {
+ if (expand_cellmap("$_DFF_?*?_", "R") ||
+ expand_cellmap("$_DFFSR_?*?_", "S") ||
+ expand_cellmap("$_DFFSR_??*_", "R"))
+ continue;
+
+ if (expand_cellmap("$_DFF_??*_", "DQ"))
+ continue;
+
+ if (expand_cellmap("$_DFF_*_", "C") ||
+ expand_cellmap("$_DFF_*??_", "C") ||
+ expand_cellmap("$_DFFSR_*??_", "C"))
+ continue;
+
+ break;
}
map_sr_to_arst("$_DFFSR_NNN_", "$_DFF_NN0_");
diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc
index fbd86d591..e06a80bbd 100644
--- a/passes/techmap/simplemap.cc
+++ b/passes/techmap/simplemap.cc
@@ -60,16 +60,28 @@ static void simplemap_pos(RTLIL::Module *module, RTLIL::Cell *cell)
module->connections.push_back(RTLIL::SigSig(sig_y, sig_a));
}
+static void simplemap_bu0(RTLIL::Module *module, RTLIL::Cell *cell)
+{
+ int width = cell->parameters.at("\\Y_WIDTH").as_int();
+
+ RTLIL::SigSpec sig_a = cell->connections.at("\\A");
+ sig_a.extend_u0(width, cell->parameters.at("\\A_SIGNED").as_bool());
+
+ RTLIL::SigSpec sig_y = cell->connections.at("\\Y");
+
+ module->connections.push_back(RTLIL::SigSig(sig_y, sig_a));
+}
+
static void simplemap_bitop(RTLIL::Module *module, RTLIL::Cell *cell)
{
int width = cell->parameters.at("\\Y_WIDTH").as_int();
RTLIL::SigSpec sig_a = cell->connections.at("\\A");
- sig_a.extend(width, cell->parameters.at("\\A_SIGNED").as_bool());
+ sig_a.extend_u0(width, cell->parameters.at("\\A_SIGNED").as_bool());
sig_a.expand();
RTLIL::SigSpec sig_b = cell->connections.at("\\B");
- sig_b.extend(width, cell->parameters.at("\\B_SIGNED").as_bool());
+ sig_b.extend_u0(width, cell->parameters.at("\\B_SIGNED").as_bool());
sig_b.expand();
RTLIL::SigSpec sig_y = cell->connections.at("\\Y");
@@ -454,6 +466,7 @@ void simplemap_get_mappers(std::map<std::string, void(*)(RTLIL::Module*, RTLIL::
{
mappers["$not"] = simplemap_not;
mappers["$pos"] = simplemap_pos;
+ mappers["$bu0"] = simplemap_bu0;
mappers["$and"] = simplemap_bitop;
mappers["$or"] = simplemap_bitop;
mappers["$xor"] = simplemap_bitop;
@@ -485,7 +498,7 @@ struct SimplemapPass : public Pass {
log("This pass maps a small selection of simple coarse-grain cells to yosys gate\n");
log("primitives. The following internal cell types are mapped by this pass:\n");
log("\n");
- log(" $not, $pos, $and, $or, $xor, $xnor\n");
+ log(" $not, $pos, $bu0, $and, $or, $xor, $xnor\n");
log(" $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n");
log(" $logic_not, $logic_and, $logic_or, $mux\n");
log(" $sr, $dff, $dffsr, $adff, $dlatch\n");
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-04 10:11:55 +0000