aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/rename.cc137
-rw-r--r--passes/cmds/setundef.cc24
-rw-r--r--passes/cmds/show.cc1
-rw-r--r--passes/cmds/stat.cc147
-rw-r--r--passes/fsm/fsm_detect.cc1
-rw-r--r--passes/hierarchy/hierarchy.cc23
-rw-r--r--passes/hierarchy/submod.cc1
-rw-r--r--passes/memory/memory_libmap.cc7
-rw-r--r--passes/memory/memory_map.cc225
-rw-r--r--passes/opt/opt_clean.cc2
-rw-r--r--passes/opt/opt_dff.cc22
-rw-r--r--passes/opt/opt_reduce.cc6
-rw-r--r--passes/opt/wreduce.cc8
-rw-r--r--passes/sat/Makefile.inc1
-rw-r--r--passes/sat/async2sync.cc3
-rw-r--r--passes/sat/clk2fflogic.cc5
-rw-r--r--passes/sat/formalff.cc549
-rw-r--r--passes/sat/qbfsat.cc2
-rw-r--r--passes/sat/sim.cc84
-rw-r--r--passes/techmap/abc.cc16
-rw-r--r--passes/techmap/abc9_exe.cc12
21 files changed, 1110 insertions, 166 deletions
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index 81da35ffe..45576c91c 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -20,6 +20,7 @@
#include "kernel/register.h"
#include "kernel/rtlil.h"
#include "kernel/log.h"
+#include "kernel/hashlib.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -105,6 +106,60 @@ static IdString derive_name_from_cell_output_wire(const RTLIL::Cell *cell, strin
return name + suffix;
}
+static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &cache, RTLIL::Module *module)
+{
+ auto cached = cache.find(module);
+ if (cached != cache.end()) {
+ if (cached->second == -1)
+ log_error("Cannot rename witness signals in a design containing recursive instantiations.\n");
+ return cached->second;
+ }
+ cache.emplace(module, -1);
+
+ bool has_witness_signals = false;
+ for (auto cell : module->cells())
+ {
+ RTLIL::Module *impl = design->module(cell->type);
+ if (impl != nullptr) {
+ bool witness_in_cell = rename_witness(design, cache, impl);
+ has_witness_signals |= witness_in_cell;
+ if (witness_in_cell && !cell->name.isPublic()) {
+ std::string name = cell->name.c_str() + 1;
+ for (auto &c : name)
+ if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
+ c = '_';
+ auto new_id = module->uniquify("\\_witness_." + name);
+ cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
+ module->rename(cell, new_id);
+ }
+ }
+
+ if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
+ has_witness_signals = true;
+ auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
+ auto sig_out = cell->getPort(QY);
+
+ for (auto chunk : sig_out.chunks()) {
+ if (chunk.is_wire() && !chunk.wire->name.isPublic()) {
+ std::string name = stringf("%s_%s", cell->type.c_str() + 1, cell->name.c_str() + 1);
+ for (auto &c : name)
+ if ((c < 'a' || c > 'z') && (c < 'A' || c > 'Z') && (c < '0' || c > '9') && c != '_')
+ c = '_';
+ auto new_id = module->uniquify("\\_witness_." + name);
+ auto new_wire = module->addWire(new_id, GetSize(sig_out));
+ new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
+ module->connect({sig_out, new_wire});
+ cell->setPort(QY, new_wire);
+ break;
+ }
+ }
+ }
+ }
+
+ cache[module] = has_witness_signals;
+ return has_witness_signals;
+}
+
struct RenamePass : public Pass {
RenamePass() : Pass("rename", "rename object in the design") { }
void help() override
@@ -146,6 +201,14 @@ struct RenamePass : public Pass {
log("pattern is '_%%_'.\n");
log("\n");
log("\n");
+ log(" rename -witness\n");
+ log("\n");
+ log("Assigns auto-generated names to all $any*/$all* output wires and containing\n");
+ log("cells that do not have a public name. This ensures that, during formal\n");
+ log("verification, a solver-found trace can be fully specified using a public\n");
+ log("hierarchical names.\n");
+ log("\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");
@@ -156,6 +219,13 @@ struct RenamePass : public Pass {
log("\n");
log("Rename top module.\n");
log("\n");
+ log("\n");
+ log(" rename -scramble-name [-seed <seed>] [selection]\n");
+ log("\n");
+ log("Assign randomly-generated names to all selected wires and cells. The seed option\n");
+ log("can be used to change the random number generator seed from the default, but it\n");
+ log("must be non-zero.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
@@ -164,10 +234,13 @@ struct RenamePass : public Pass {
bool flag_src = false;
bool flag_wire = false;
bool flag_enumerate = false;
+ bool flag_witness = false;
bool flag_hide = false;
bool flag_top = false;
bool flag_output = false;
+ bool flag_scramble_name = false;
bool got_mode = false;
+ unsigned int seed = 1;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
@@ -193,6 +266,11 @@ struct RenamePass : public Pass {
got_mode = true;
continue;
}
+ if (arg == "-witness" && !got_mode) {
+ flag_witness = true;
+ got_mode = true;
+ continue;
+ }
if (arg == "-hide" && !got_mode) {
flag_hide = true;
got_mode = true;
@@ -203,6 +281,11 @@ struct RenamePass : public Pass {
got_mode = true;
continue;
}
+ if (arg == "-scramble-name" && !got_mode) {
+ flag_scramble_name = true;
+ got_mode = true;
+ continue;
+ }
if (arg == "-pattern" && argidx+1 < args.size() && args[argidx+1].find('%') != std::string::npos) {
int pos = args[++argidx].find('%');
pattern_prefix = args[argidx].substr(0, pos);
@@ -211,6 +294,11 @@ struct RenamePass : public Pass {
}
if (arg == "-suffix" && argidx + 1 < args.size()) {
cell_suffix = args[++argidx];
+ continue;
+ }
+ if (arg == "-seed" && argidx+1 < args.size()) {
+ seed = std::stoi(args[++argidx]);
+ continue;
}
break;
}
@@ -289,6 +377,19 @@ struct RenamePass : public Pass {
}
}
else
+ if (flag_witness)
+ {
+ extra_args(args, argidx, design, false);
+
+ RTLIL::Module *module = design->top_module();
+
+ if (module == nullptr)
+ log_cmd_error("No top module found!\n");
+
+ dict<RTLIL::Module *, int> cache;
+ rename_witness(design, cache, module);
+ }
+ else
if (flag_hide)
{
extra_args(args, argidx, design);
@@ -329,6 +430,42 @@ struct RenamePass : public Pass {
design->rename(module, new_name);
}
else
+ if (flag_scramble_name)
+ {
+ extra_args(args, argidx, design);
+
+ if (seed == 0)
+ log_error("Seed for -scramble-name cannot be zero.\n");
+
+ for (auto module : design->selected_modules())
+ {
+ if (module->memories.size() != 0 || module->processes.size() != 0) {
+ log_warning("Skipping module %s with unprocessed memories or processes\n", log_id(module));
+ continue;
+ }
+
+ dict<RTLIL::Wire *, IdString> new_wire_names;
+ dict<RTLIL::Cell *, IdString> new_cell_names;
+
+ for (auto wire : module->selected_wires())
+ if (wire->port_id == 0) {
+ seed = mkhash_xorshift(seed);
+ new_wire_names[wire] = stringf("$_%u_", seed);
+ }
+
+ for (auto cell : module->selected_cells()) {
+ seed = mkhash_xorshift(seed);
+ new_cell_names[cell] = stringf("$_%u_", seed);
+ }
+
+ for (auto &it : new_wire_names)
+ module->rename(it.first, it.second);
+
+ for (auto &it : new_cell_names)
+ module->rename(it.first, it.second);
+ }
+ }
+ else
{
if (argidx+2 != args.size())
log_cmd_error("Invalid number of arguments!\n");
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index a078b0b1c..590a7eb1d 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -20,6 +20,7 @@
#include "kernel/register.h"
#include "kernel/celltypes.h"
#include "kernel/sigtools.h"
+#include "kernel/mem.h"
#include "kernel/rtlil.h"
#include "kernel/log.h"
@@ -478,6 +479,29 @@ struct SetundefPass : public Pass {
log_assert(ffbits.empty());
}
+ if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
+ {
+ // Do not add anyseq / anyconst to unused memory port clocks
+ std::vector<Mem> memories = Mem::get_selected_memories(module);
+ for (auto &mem : memories) {
+ bool changed = false;
+ for (auto &rd_port : mem.rd_ports) {
+ if (!rd_port.clk_enable && rd_port.clk.is_fully_undef()) {
+ changed = true;
+ rd_port.clk = State::S0;
+ }
+ }
+ for (auto &wr_port : mem.rd_ports) {
+ if (!wr_port.clk_enable && wr_port.clk.is_fully_undef()) {
+ changed = true;
+ wr_port.clk = State::S0;
+ }
+ }
+ if (changed)
+ mem.emit();
+ }
+ }
+
module->rewrite_sigspecs(worker);
if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index 43deba47b..4d5605932 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -574,6 +574,7 @@ struct ShowWorker
{
ct.setup_internals();
ct.setup_internals_mem();
+ ct.setup_internals_anyinit();
ct.setup_stdcells();
ct.setup_stdcells_mem();
ct.setup_design(design);
diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index c858c8631..a4984597d 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -17,10 +17,13 @@
*
*/
+#include <iterator>
+
#include "kernel/yosys.h"
#include "kernel/celltypes.h"
#include "passes/techmap/libparse.h"
#include "kernel/cost.h"
+#include "libs/json11/json11.hpp"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -32,14 +35,14 @@ struct statdata_t
#define STAT_NUMERIC_MEMBERS STAT_INT_MEMBERS X(area)
- #define X(_name) int _name;
+ #define X(_name) unsigned int _name;
STAT_INT_MEMBERS
#undef X
double area;
string tech;
std::map<RTLIL::IdString, int> techinfo;
- std::map<RTLIL::IdString, int, RTLIL::sort_by_id_str> num_cells_by_type;
+ std::map<RTLIL::IdString, unsigned int, RTLIL::sort_by_id_str> num_cells_by_type;
std::set<RTLIL::IdString> unknown_cell_area;
statdata_t operator+(const statdata_t &other) const
@@ -53,7 +56,7 @@ struct statdata_t
return sum;
}
- statdata_t operator*(int other) const
+ statdata_t operator*(unsigned int other) const
{
statdata_t sum = *this;
#define X(_name) sum._name *= other;
@@ -148,17 +151,17 @@ struct statdata_t
void log_data(RTLIL::IdString mod_name, bool top_mod)
{
- log(" Number of wires: %6d\n", num_wires);
- log(" Number of wire bits: %6d\n", num_wire_bits);
- log(" Number of public wires: %6d\n", num_pub_wires);
- log(" Number of public wire bits: %6d\n", num_pub_wire_bits);
- log(" Number of memories: %6d\n", num_memories);
- log(" Number of memory bits: %6d\n", num_memory_bits);
- log(" Number of processes: %6d\n", num_processes);
- log(" Number of cells: %6d\n", num_cells);
+ log(" Number of wires: %6u\n", num_wires);
+ log(" Number of wire bits: %6u\n", num_wire_bits);
+ log(" Number of public wires: %6u\n", num_pub_wires);
+ log(" Number of public wire bits: %6u\n", num_pub_wire_bits);
+ log(" Number of memories: %6u\n", num_memories);
+ log(" Number of memory bits: %6u\n", num_memory_bits);
+ log(" Number of processes: %6u\n", num_processes);
+ log(" Number of cells: %6u\n", num_cells);
for (auto &it : num_cells_by_type)
if (it.second)
- log(" %-26s %6d\n", log_id(it.first), it.second);
+ log(" %-26s %6u\n", log_id(it.first), it.second);
if (!unknown_cell_area.empty()) {
log("\n");
@@ -173,13 +176,13 @@ struct statdata_t
if (tech == "xilinx")
{
- int lut6_cnt = num_cells_by_type[ID(LUT6)];
- int lut5_cnt = num_cells_by_type[ID(LUT5)];
- int lut4_cnt = num_cells_by_type[ID(LUT4)];
- int lut3_cnt = num_cells_by_type[ID(LUT3)];
- int lut2_cnt = num_cells_by_type[ID(LUT2)];
- int lut1_cnt = num_cells_by_type[ID(LUT1)];
- int lc_cnt = 0;
+ unsigned int lut6_cnt = num_cells_by_type[ID(LUT6)];
+ unsigned int lut5_cnt = num_cells_by_type[ID(LUT5)];
+ unsigned int lut4_cnt = num_cells_by_type[ID(LUT4)];
+ unsigned int lut3_cnt = num_cells_by_type[ID(LUT3)];
+ unsigned int lut2_cnt = num_cells_by_type[ID(LUT2)];
+ unsigned int lut1_cnt = num_cells_by_type[ID(LUT1)];
+ unsigned int lc_cnt = 0;
lc_cnt += lut6_cnt;
@@ -221,12 +224,12 @@ struct statdata_t
lc_cnt += (lut2_cnt + lut1_cnt + 1) / 2;
log("\n");
- log(" Estimated number of LCs: %10d\n", lc_cnt);
+ log(" Estimated number of LCs: %10u\n", lc_cnt);
}
if (tech == "cmos")
{
- int tran_cnt = 0;
+ unsigned int tran_cnt = 0;
bool tran_cnt_exact = true;
auto &gate_costs = CellCosts::cmos_gate_cost();
@@ -243,20 +246,48 @@ struct statdata_t
}
log("\n");
- log(" Estimated number of transistors: %10d%s\n", tran_cnt, tran_cnt_exact ? "" : "+");
+ log(" Estimated number of transistors: %10u%s\n", tran_cnt, tran_cnt_exact ? "" : "+");
}
}
+
+ void log_data_json(const char *mod_name, bool first_module)
+ {
+ if (!first_module)
+ log(",\n");
+ log(" %s: {\n", json11::Json(mod_name).dump().c_str());
+ log(" \"num_wires\": %u,\n", num_wires);
+ log(" \"num_wire_bits\": %u,\n", num_wire_bits);
+ log(" \"num_pub_wires\": %u,\n", num_pub_wires);
+ log(" \"num_pub_wire_bits\": %u,\n", num_pub_wire_bits);
+ log(" \"num_memories\": %u,\n", num_memories);
+ log(" \"num_memory_bits\": %u,\n", num_memory_bits);
+ log(" \"num_processes\": %u,\n", num_processes);
+ log(" \"num_cells\": %u,\n", num_cells);
+ log(" \"num_cells_by_type\": {\n");
+ bool first_line = true;
+ for (auto &it : num_cells_by_type)
+ if (it.second) {
+ if (!first_line)
+ log(",\n");
+ log(" %s: %u", json11::Json(log_id(it.first)).dump().c_str(), it.second);
+ first_line = false;
+ }
+ log("\n");
+ log(" }\n");
+ log(" }");
+ }
};
-statdata_t hierarchy_worker(std::map<RTLIL::IdString, statdata_t> &mod_stat, RTLIL::IdString mod, int level)
+statdata_t hierarchy_worker(std::map<RTLIL::IdString, statdata_t> &mod_stat, RTLIL::IdString mod, int level, bool quiet = false)
{
statdata_t mod_data = mod_stat.at(mod);
- std::map<RTLIL::IdString, int, RTLIL::sort_by_id_str> num_cells_by_type;
+ std::map<RTLIL::IdString, unsigned int, RTLIL::sort_by_id_str> num_cells_by_type;
num_cells_by_type.swap(mod_data.num_cells_by_type);
for (auto &it : num_cells_by_type)
if (mod_stat.count(it.first) > 0) {
- log(" %*s%-*s %6d\n", 2*level, "", 26-2*level, log_id(it.first), it.second);
+ if (!quiet)
+ log(" %*s%-*s %6u\n", 2*level, "", 26-2*level, log_id(it.first), it.second);
mod_data = mod_data + hierarchy_worker(mod_stat, it.first, level+1) * it.second;
mod_data.num_cells -= it.second;
} else {
@@ -314,12 +345,16 @@ struct StatPass : public Pass {
log(" annotate internal cell types with their word width.\n");
log(" e.g. $add_8 for an 8 bit wide $add cell.\n");
log("\n");
+ log(" -json\n");
+ log(" output the statistics in a machine-readable JSON format.\n");
+ log(" this is output to the console; use \"tee\" to output to a file.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
log_header(design, "Printing statistics.\n");
- bool width_mode = false;
+ bool width_mode = false, json_mode = false;
RTLIL::Module *top_mod = nullptr;
std::map<RTLIL::IdString, statdata_t> mod_stat;
dict<IdString, double> cell_area;
@@ -348,13 +383,27 @@ struct StatPass : public Pass {
top_mod = design->module(RTLIL::escape_id(args[++argidx]));
continue;
}
+ if (args[argidx] == "-json") {
+ json_mode = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
- if (techname != "" && techname != "xilinx" && techname != "cmos")
+ if (techname != "" && techname != "xilinx" && techname != "cmos" && !json_mode)
log_cmd_error("Unsupported technology: '%s'\n", techname.c_str());
+ if (json_mode) {
+ log("{\n");
+ log(" \"creator\": %s,\n", json11::Json(yosys_version_str).dump().c_str());
+ std::stringstream invocation;
+ std::copy(args.begin(), args.end(), std::ostream_iterator<std::string>(invocation, " "));
+ log(" \"invocation\": %s,\n", json11::Json(invocation.str()).dump().c_str());
+ log(" \"modules\": {\n");
+ }
+
+ bool first_module = true;
for (auto mod : design->selected_modules())
{
if (!top_mod && design->full_selection())
@@ -364,23 +413,40 @@ struct StatPass : public Pass {
statdata_t data(design, mod, width_mode, cell_area, techname);
mod_stat[mod->name] = data;
+ if (json_mode) {
+ data.log_data_json(mod->name.c_str(), first_module);
+ first_module = false;
+ } else {
+ log("\n");
+ log("=== %s%s ===\n", log_id(mod->name), design->selected_whole_module(mod->name) ? "" : " (partially selected)");
+ log("\n");
+ data.log_data(mod->name, false);
+ }
+ }
+
+ if (json_mode) {
log("\n");
- log("=== %s%s ===\n", log_id(mod->name), design->selected_whole_module(mod->name) ? "" : " (partially selected)");
- log("\n");
- data.log_data(mod->name, false);
+ log(" },\n");
}
- if (top_mod != nullptr && GetSize(mod_stat) > 1)
+ if (top_mod != nullptr)
{
- log("\n");
- log("=== design hierarchy ===\n");
- log("\n");
+ if (!json_mode && GetSize(mod_stat) > 1) {
+ log("\n");
+ log("=== design hierarchy ===\n");
+ log("\n");
+ log(" %-28s %6d\n", log_id(top_mod->name), 1);
+ }
- log(" %-28s %6d\n", log_id(top_mod->name), 1);
- statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0);
+ statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0, /*quiet=*/json_mode);
+
+ if (json_mode)
+ data.log_data_json("design", true);
+ else if (GetSize(mod_stat) > 1) {
+ log("\n");
+ data.log_data(top_mod->name, true);
+ }
- log("\n");
- data.log_data(top_mod->name, true);
design->scratchpad_set_int("stat.num_wires", data.num_wires);
design->scratchpad_set_int("stat.num_wire_bits", data.num_wire_bits);
design->scratchpad_set_int("stat.num_pub_wires", data.num_pub_wires);
@@ -392,6 +458,11 @@ struct StatPass : public Pass {
design->scratchpad_set_int("stat.area", data.area);
}
+ if (json_mode) {
+ log("\n");
+ log("}\n");
+ }
+
log("\n");
}
} StatPass;
diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc
index a2d38a0bd..f829714c4 100644
--- a/passes/fsm/fsm_detect.cc
+++ b/passes/fsm/fsm_detect.cc
@@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass {
CellTypes ct;
ct.setup_internals();
+ ct.setup_internals_anyinit();
ct.setup_internals_mem();
ct.setup_stdcells();
ct.setup_stdcells_mem();
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index d40d6e59f..d27fddf1c 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -439,7 +439,8 @@ void check_cell_connections(const RTLIL::Module &module, RTLIL::Cell &cell, RTLI
}
}
-bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, std::vector<std::string> &libdirs)
+bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check, bool flag_simcheck, bool flag_smtcheck,
+ std::vector<std::string> &libdirs)
{
bool did_something = false;
std::map<RTLIL::Cell*, std::pair<int, int>> array_cells;
@@ -477,7 +478,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
RTLIL::Module *mod = design->module(cell->type);
if (!mod)
{
- mod = get_module(*design, *cell, *module, flag_check || flag_simcheck, libdirs);
+ mod = get_module(*design, *cell, *module, flag_check || flag_simcheck || flag_smtcheck, libdirs);
// If we still don't have a module, treat the cell as a black box and skip
// it. Otherwise, we either loaded or derived something so should set the
@@ -495,11 +496,11 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
// interfaces.
if_expander.visit_connections(*cell, *mod);
- if (flag_check || flag_simcheck)
+ if (flag_check || flag_simcheck || flag_smtcheck)
check_cell_connections(*module, *cell, *mod);
if (mod->get_blackbox_attribute()) {
- if (flag_simcheck)
+ if (flag_simcheck || (flag_smtcheck && !mod->get_bool_attribute(ID::smtlib2_module)))
log_error("Module `%s' referenced in module `%s' in cell `%s' is a blackbox/whitebox module.\n",
cell->type.c_str(), module->name.c_str(), cell->name.c_str());
continue;
@@ -737,6 +738,9 @@ struct HierarchyPass : public Pass {
log(" like -check, but also throw an error if blackbox modules are\n");
log(" instantiated, and throw an error if the design has no top module.\n");
log("\n");
+ log(" -smtcheck\n");
+ log(" like -simcheck, but allow smtlib2_module modules.\n");
+ log("\n");
log(" -purge_lib\n");
log(" by default the hierarchy command will not remove library (blackbox)\n");
log(" modules. use this option to also remove unused blackbox modules.\n");
@@ -803,6 +807,7 @@ struct HierarchyPass : public Pass {
bool flag_check = false;
bool flag_simcheck = false;
+ bool flag_smtcheck = false;
bool purge_lib = false;
RTLIL::Module *top_mod = NULL;
std::string load_top_mod;
@@ -821,7 +826,7 @@ struct HierarchyPass : public Pass {
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
- if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !top_mod) {
+ if (args[argidx] == "-generate" && !flag_check && !flag_simcheck && !flag_smtcheck && !top_mod) {
generate_mode = true;
log("Entering generate mode.\n");
while (++argidx < args.size()) {
@@ -868,6 +873,10 @@ struct HierarchyPass : public Pass {
flag_simcheck = true;
continue;
}
+ if (args[argidx] == "-smtcheck") {
+ flag_smtcheck = true;
+ continue;
+ }
if (args[argidx] == "-purge_lib") {
purge_lib = true;
continue;
@@ -1013,7 +1022,7 @@ struct HierarchyPass : public Pass {
}
}
- if (flag_simcheck && top_mod == nullptr)
+ if ((flag_simcheck || flag_smtcheck) && top_mod == nullptr)
log_error("Design has no top module.\n");
if (top_mod != NULL) {
@@ -1039,7 +1048,7 @@ struct HierarchyPass : public Pass {
}
for (auto module : used_modules) {
- if (expand_module(design, module, flag_check, flag_simcheck, libdirs))
+ if (expand_module(design, module, flag_check, flag_simcheck, flag_smtcheck, libdirs))
did_something = true;
}
diff --git a/passes/hierarchy/submod.cc b/passes/hierarchy/submod.cc
index 845dc850f..c0c40671d 100644
--- a/passes/hierarchy/submod.cc
+++ b/passes/hierarchy/submod.cc
@@ -260,6 +260,7 @@ struct SubmodWorker
}
ct.setup_internals();
+ ct.setup_internals_anyinit();
ct.setup_internals_mem();
ct.setup_stdcells();
ct.setup_stdcells_mem();
diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc
index 898e0af85..9e147b0bf 100644
--- a/passes/memory/memory_libmap.cc
+++ b/passes/memory/memory_libmap.cc
@@ -837,7 +837,7 @@ void MemMapping::handle_priority() {
if (!port2.priority_mask[p1idx])
continue;
for (auto &cfg: cfgs) {
- auto &p1cfg = cfg.rd_ports[p1idx];
+ auto &p1cfg = cfg.wr_ports[p1idx];
auto &p2cfg = cfg.wr_ports[p2idx];
bool found = false;
for (auto &pgi: p2cfg.def->wrprio) {
@@ -1706,10 +1706,11 @@ void MemMapping::emit_port(const MemConfig &cfg, std::vector<Cell*> &cells, cons
if (pdef.wrbe_separate) {
cell->setPort(stringf("\\PORT_%s_WR_EN", name), State::S0);
cell->setPort(stringf("\\PORT_%s_WR_BE", name), hw_wren);
- cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren));
+ if (cfg.def->width_mode != WidthMode::Single)
+ cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren));
} else {
cell->setPort(stringf("\\PORT_%s_WR_EN", name), hw_wren);
- if (cfg.def->byte != 0)
+ if (cfg.def->byte != 0 && cfg.def->width_mode != WidthMode::Single)
cell->setParam(stringf("\\PORT_%s_WR_EN_WIDTH", name), GetSize(hw_wren));
}
}
diff --git a/passes/memory/memory_map.cc b/passes/memory/memory_map.cc
index ca1ca483d..e2f74c2e1 100644
--- a/passes/memory/memory_map.cc
+++ b/passes/memory/memory_map.cc
@@ -30,6 +30,9 @@ PRIVATE_NAMESPACE_BEGIN
struct MemoryMapWorker
{
bool attr_icase = false;
+ bool rom_only = false;
+ bool keepdc = false;
+ bool formal = false;
dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
RTLIL::Design *design;
@@ -107,11 +110,8 @@ struct MemoryMapWorker
SigSpec init_data = mem.get_init_data();
- // delete unused memory cell
- if (mem.rd_ports.empty()) {
- mem.remove();
+ if (!mem.wr_ports.empty() && rom_only)
return;
- }
// check if attributes allow us to infer FFRAM for this memory
for (const auto &attr : attributes) {
@@ -143,9 +143,17 @@ struct MemoryMapWorker
}
}
+ // delete unused memory cell
+ if (mem.rd_ports.empty()) {
+ mem.remove();
+ return;
+ }
+
// all write ports must share the same clock
RTLIL::SigSpec refclock;
bool refclock_pol = false;
+ bool async_wr = false;
+ bool static_only = true;
for (int i = 0; i < GetSize(mem.wr_ports); i++) {
auto &port = mem.wr_ports[i];
if (port.en.is_fully_const() && !port.en.as_bool()) {
@@ -159,10 +167,20 @@ struct MemoryMapWorker
static_ports.insert(i);
continue;
}
- log("Not mapping memory %s in module %s (write port %d has no clock).\n",
- mem.memid.c_str(), module->name.c_str(), i);
- return;
+ static_only = false;
+ if (GetSize(refclock) != 0)
+ log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n",
+ mem.memid.c_str(), module->name.c_str());
+ if (!formal)
+ log("Not mapping memory %s in module %s (write port %d has no clock).\n",
+ mem.memid.c_str(), module->name.c_str(), i);
+ async_wr = true;
+ continue;
}
+ static_only = false;
+ if (async_wr)
+ log("Not mapping memory %s in module %s (mixed clocked and async write ports).\n",
+ mem.memid.c_str(), module->name.c_str());
if (refclock.size() == 0) {
refclock = port.clk;
refclock_pol = port.clk_polarity;
@@ -180,28 +198,47 @@ struct MemoryMapWorker
std::vector<RTLIL::SigSpec> data_reg_in(1 << abits);
std::vector<RTLIL::SigSpec> data_reg_out(1 << abits);
+ std::vector<RTLIL::SigSpec> &data_read = async_wr ? data_reg_in : data_reg_out;
+
int count_static = 0;
for (int i = 0; i < mem.size; i++)
{
int addr = i + mem.start_offset;
int idx = addr & ((1 << abits) - 1);
+ SigSpec w_init = init_data.extract(i*mem.width, mem.width);
if (static_cells_map.count(addr) > 0)
{
- data_reg_out[idx] = static_cells_map[addr];
+ data_read[idx] = static_cells_map[addr];
count_static++;
}
+ else if (static_only && (!keepdc || w_init.is_fully_def()))
+ {
+ data_read[idx] = w_init;
+ }
else
{
- RTLIL::Cell *c = module->addCell(genid(mem.memid, "", addr), ID($dff));
- c->parameters[ID::WIDTH] = mem.width;
- if (GetSize(refclock) != 0) {
+ RTLIL::Cell *c;
+ auto ff_id = genid(mem.memid, "", addr);
+
+ if (static_only) {
+ // non-static part is a ROM, we only reach this with keepdc
+ if (formal) {
+ c = module->addCell(ff_id, ID($ff));
+ } else {
+ c = module->addCell(ff_id, ID($dff));
+ c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1);
+ c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0));
+ }
+ } else if (async_wr) {
+ log_assert(formal); // General async write not implemented yet, checked against above
+ c = module->addCell(ff_id, ID($ff));
+ } else {
+ c = module->addCell(ff_id, ID($dff));
c->parameters[ID::CLK_POLARITY] = RTLIL::Const(refclock_pol);
c->setPort(ID::CLK, refclock);
- } else {
- c->parameters[ID::CLK_POLARITY] = RTLIL::Const(RTLIL::State::S1);
- c->setPort(ID::CLK, RTLIL::SigSpec(RTLIL::State::S0));
}
+ c->parameters[ID::WIDTH] = mem.width;
RTLIL::Wire *w_in = module->addWire(genid(mem.memid, "", addr, "$d"), mem.width);
data_reg_in[idx] = w_in;
@@ -212,17 +249,28 @@ struct MemoryMapWorker
w_out_name = genid(mem.memid, "", addr, "$q");
RTLIL::Wire *w_out = module->addWire(w_out_name, mem.width);
- SigSpec w_init = init_data.extract(i*mem.width, mem.width);
+
+ if (formal && mem.packed && mem.cell->name.c_str()[0] == '\\') {
+ auto hdlname = mem.cell->get_hdlname_attribute();
+ if (hdlname.empty())
+ hdlname.push_back(mem.cell->name.c_str() + 1);
+ hdlname.push_back(stringf("[%d]", addr));
+ w_out->set_hdlname_attribute(hdlname);
+ }
if (!w_init.is_fully_undef())
w_out->attributes[ID::init] = w_init.as_const();
data_reg_out[idx] = w_out;
c->setPort(ID::Q, w_out);
+
+ if (static_only)
+ module->connect(RTLIL::SigSig(w_in, w_out));
}
}
- log(" created %d $dff cells and %d static cells of width %d.\n", mem.size-count_static, count_static, mem.width);
+ log(" created %d %s cells and %d static cells of width %d.\n",
+ mem.size-count_static, formal && (static_only || async_wr) ? "$ff" : "$dff", count_static, mem.width);
int count_dff = 0, count_mux = 0, count_wrmux = 0;
@@ -260,75 +308,78 @@ struct MemoryMapWorker
}
for (int j = 0; j < (1 << abits); j++)
- if (data_reg_out[j] != SigSpec())
- module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_reg_out[j]));
+ if (data_read[j] != SigSpec())
+ module->connect(RTLIL::SigSig(rd_signals[j >> port.wide_log2].extract((j & ((1 << port.wide_log2) - 1)) * mem.width, mem.width), data_read[j]));
}
log(" read interface: %d $dff and %d $mux cells.\n", count_dff, count_mux);
- for (int i = 0; i < mem.size; i++)
+ if (!static_only)
{
- int addr = i + mem.start_offset;
- int idx = addr & ((1 << abits) - 1);
- if (static_cells_map.count(addr) > 0)
- continue;
-
- RTLIL::SigSpec sig = data_reg_out[idx];
-
- for (int j = 0; j < GetSize(mem.wr_ports); j++)
+ for (int i = 0; i < mem.size; i++)
{
- auto &port = mem.wr_ports[j];
- RTLIL::SigSpec wr_addr = port.addr.extract_end(port.wide_log2);
- RTLIL::Wire *w_seladdr = addr_decode(wr_addr, RTLIL::SigSpec(addr >> port.wide_log2, GetSize(wr_addr)));
+ int addr = i + mem.start_offset;
+ int idx = addr & ((1 << abits) - 1);
+ if (static_cells_map.count(addr) > 0)
+ continue;
- int sub = addr & ((1 << port.wide_log2) - 1);
+ RTLIL::SigSpec sig = data_reg_out[idx];
- int wr_offset = 0;
- while (wr_offset < mem.width)
+ for (int j = 0; j < GetSize(mem.wr_ports); j++)
{
- int wr_width = 1;
- RTLIL::SigSpec wr_bit = port.en.extract(wr_offset + sub * mem.width, 1);
-
- while (wr_offset + wr_width < mem.width) {
- RTLIL::SigSpec next_wr_bit = port.en.extract(wr_offset + wr_width + sub * mem.width, 1);
- if (next_wr_bit != wr_bit)
- break;
- wr_width++;
- }
+ auto &port = mem.wr_ports[j];
+ RTLIL::SigSpec wr_addr = port.addr.extract_end(port.wide_log2);
+ RTLIL::Wire *w_seladdr = addr_decode(wr_addr, RTLIL::SigSpec(addr >> port.wide_log2, GetSize(wr_addr)));
- RTLIL::Wire *w = w_seladdr;
+ int sub = addr & ((1 << port.wide_log2) - 1);
- if (wr_bit != State::S1)
+ int wr_offset = 0;
+ while (wr_offset < mem.width)
{
- RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wren", addr, "", j, "", wr_offset), ID($and));
- c->parameters[ID::A_SIGNED] = RTLIL::Const(0);
- c->parameters[ID::B_SIGNED] = RTLIL::Const(0);
- c->parameters[ID::A_WIDTH] = RTLIL::Const(1);
- c->parameters[ID::B_WIDTH] = RTLIL::Const(1);
- c->parameters[ID::Y_WIDTH] = RTLIL::Const(1);
- c->setPort(ID::A, w);
- c->setPort(ID::B, wr_bit);
-
- w = module->addWire(genid(mem.memid, "$wren", addr, "", j, "", wr_offset, "$y"));
- c->setPort(ID::Y, RTLIL::SigSpec(w));
+ int wr_width = 1;
+ RTLIL::SigSpec wr_bit = port.en.extract(wr_offset + sub * mem.width, 1);
+
+ while (wr_offset + wr_width < mem.width) {
+ RTLIL::SigSpec next_wr_bit = port.en.extract(wr_offset + wr_width + sub * mem.width, 1);
+ if (next_wr_bit != wr_bit)
+ break;
+ wr_width++;
+ }
+
+ RTLIL::Wire *w = w_seladdr;
+
+ if (wr_bit != State::S1)
+ {
+ RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wren", addr, "", j, "", wr_offset), ID($and));
+ c->parameters[ID::A_SIGNED] = RTLIL::Const(0);
+ c->parameters[ID::B_SIGNED] = RTLIL::Const(0);
+ c->parameters[ID::A_WIDTH] = RTLIL::Const(1);
+ c->parameters[ID::B_WIDTH] = RTLIL::Const(1);
+ c->parameters[ID::Y_WIDTH] = RTLIL::Const(1);
+ c->setPort(ID::A, w);
+ c->setPort(ID::B, wr_bit);
+
+ w = module->addWire(genid(mem.memid, "$wren", addr, "", j, "", wr_offset, "$y"));
+ c->setPort(ID::Y, RTLIL::SigSpec(w));
+ }
+
+ RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset), ID($mux));
+ c->parameters[ID::WIDTH] = wr_width;
+ c->setPort(ID::A, sig.extract(wr_offset, wr_width));
+ c->setPort(ID::B, port.data.extract(wr_offset + sub * mem.width, wr_width));
+ c->setPort(ID::S, RTLIL::SigSpec(w));
+
+ w = module->addWire(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset, "$y"), wr_width);
+ c->setPort(ID::Y, w);
+
+ sig.replace(wr_offset, w);
+ wr_offset += wr_width;
+ count_wrmux++;
}
-
- RTLIL::Cell *c = module->addCell(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset), ID($mux));
- c->parameters[ID::WIDTH] = wr_width;
- c->setPort(ID::A, sig.extract(wr_offset, wr_width));
- c->setPort(ID::B, port.data.extract(wr_offset + sub * mem.width, wr_width));
- c->setPort(ID::S, RTLIL::SigSpec(w));
-
- w = module->addWire(genid(mem.memid, "$wrmux", addr, "", j, "", wr_offset, "$y"), wr_width);
- c->setPort(ID::Y, w);
-
- sig.replace(wr_offset, w);
- wr_offset += wr_width;
- count_wrmux++;
}
- }
- module->connect(RTLIL::SigSig(data_reg_in[idx], sig));
+ module->connect(RTLIL::SigSig(data_reg_in[idx], sig));
+ }
}
log(" write interface: %d write mux blocks.\n", count_wrmux);
@@ -366,10 +417,25 @@ struct MemoryMapPass : public Pass {
log(" -iattr\n");
log(" for -attr, ignore case of <value>.\n");
log("\n");
+ log(" -rom-only\n");
+ log(" only perform conversion for ROMs (memories with no write ports).\n");
+ log("\n");
+ log(" -keepdc\n");
+ log(" when mapping ROMs, keep x-bits shared across read ports.\n");
+ log("\n");
+ log(" -formal\n");
+ log(" map memories for a global clock based formal verification flow.\n");
+ log(" This implies -keepdc, uses $ff cells for ROMs and sets hdlname\n");
+ log(" attributes. It also has limited support for async write ports\n");
+ log(" as generated by clk2fflogic.\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
bool attr_icase = false;
+ bool rom_only = false;
+ bool keepdc = false;
+ bool formal = false;
dict<RTLIL::IdString, std::vector<RTLIL::Const>> attributes;
log_header(design, "Executing MEMORY_MAP pass (converting memories to logic and flip-flops).\n");
@@ -406,6 +472,22 @@ struct MemoryMapPass : public Pass {
attr_icase = true;
continue;
}
+ if (args[argidx] == "-rom-only")
+ {
+ rom_only = true;
+ continue;
+ }
+ if (args[argidx] == "-keepdc")
+ {
+ keepdc = true;
+ continue;
+ }
+ if (args[argidx] == "-formal")
+ {
+ formal = true;
+ keepdc = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -414,6 +496,9 @@ struct MemoryMapPass : public Pass {
MemoryMapWorker worker(design, mod);
worker.attr_icase = attr_icase;
worker.attributes = attributes;
+ worker.rom_only = rom_only;
+ worker.keepdc = keepdc;
+ worker.formal = formal;
worker.run();
}
}
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index cb2c261c4..dde7c5299 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -633,6 +633,7 @@ struct OptCleanPass : public Pass {
keep_cache.reset(design);
ct_reg.setup_internals_mem();
+ ct_reg.setup_internals_anyinit();
ct_reg.setup_stdcells_mem();
ct_all.setup(design);
@@ -694,6 +695,7 @@ struct CleanPass : public Pass {
keep_cache.reset(design);
ct_reg.setup_internals_mem();
+ ct_reg.setup_internals_anyinit();
ct_reg.setup_stdcells_mem();
ct_all.setup(design);
diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc
index 0ad4acec2..6ff2d1b4b 100644
--- a/passes/opt/opt_dff.cc
+++ b/passes/opt/opt_dff.cc
@@ -491,12 +491,17 @@ struct OptDffWorker
ff.has_srst = false;
ff.sig_d = ff.val_srst;
changed = true;
- } else {
+ } else if (!opt.keepdc || ff.val_init.is_fully_def()) {
log("Handling never-active EN on %s (%s) from module %s (removing D path).\n",
log_id(cell), log_id(cell->type), log_id(module));
// The D input path is effectively useless, so remove it (this will be a D latch, SR latch, or a const driver).
ff.has_ce = ff.has_clk = ff.has_srst = false;
changed = true;
+ } else {
+ // We need to keep the undefined initival around as such
+ ff.sig_d = ff.sig_q;
+ ff.has_ce = ff.has_srst = false;
+ changed = true;
}
} else if (ff.sig_ce == (ff.pol_ce ? State::S1 : State::S0)) {
// Always-active enable. Just remove it.
@@ -508,13 +513,20 @@ struct OptDffWorker
}
}
- if (ff.has_clk) {
- if (ff.sig_clk.is_fully_const()) {
+ if (ff.has_clk && ff.sig_clk.is_fully_const()) {
+ if (!opt.keepdc || ff.val_init.is_fully_def()) {
// Const clock — the D input path is effectively useless, so remove it (this will be a D latch, SR latch, or a const driver).
log("Handling const CLK on %s (%s) from module %s (removing D path).\n",
log_id(cell), log_id(cell->type), log_id(module));
ff.has_ce = ff.has_clk = ff.has_srst = false;
changed = true;
+ } else {
+ // Const clock, but we need to keep the undefined initval around as such
+ if (ff.has_ce || ff.has_srst || ff.sig_d != ff.sig_q) {
+ ff.sig_d = ff.sig_q;
+ ff.has_ce = ff.has_srst = false;
+ changed = true;
+ }
}
}
@@ -550,7 +562,7 @@ struct OptDffWorker
ff.has_srst = false;
ff.sig_d = ff.val_srst;
changed = true;
- } else {
+ } else if (!opt.keepdc || ff.val_init.is_fully_def()) {
// The D input path is effectively useless, so remove it (this will be a const-input D latch, SR latch, or a const driver).
log("Handling D = Q on %s (%s) from module %s (removing D path).\n",
log_id(cell), log_id(cell->type), log_id(module));
@@ -567,7 +579,7 @@ struct OptDffWorker
}
// The cell has been simplified as much as possible already. Now try to spice it up with enables / sync resets.
- if (ff.has_clk) {
+ if (ff.has_clk && ff.sig_d != ff.sig_q) {
if (!ff.has_arst && !ff.has_sr && (!ff.has_srst || !ff.has_ce || ff.ce_over_srst) && !opt.nosdff) {
// Try to merge sync resets.
std::map<ctrls_t, std::vector<int>> groups;
diff --git a/passes/opt/opt_reduce.cc b/passes/opt/opt_reduce.cc
index 1a7c93fbd..c36a38dae 100644
--- a/passes/opt/opt_reduce.cc
+++ b/passes/opt/opt_reduce.cc
@@ -594,11 +594,9 @@ struct OptReduceWorker
if (cell->type.in(ID($mux), ID($pmux)))
opt_pmux(cell);
-
- if (cell->type == ID($bmux))
+ else if (cell->type == ID($bmux))
opt_bmux(cell);
-
- if (cell->type == ID($demux))
+ else if (cell->type == ID($demux))
opt_demux(cell);
}
}
diff --git a/passes/opt/wreduce.cc b/passes/opt/wreduce.cc
index 08ab6de6f..8fd4c788c 100644
--- a/passes/opt/wreduce.cc
+++ b/passes/opt/wreduce.cc
@@ -166,8 +166,8 @@ struct WreduceWorker
for (int i = GetSize(sig_q)-1; i >= 0; i--)
{
- if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || initval[i] == State::Sx) &&
- (!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || rst_value[i] == State::Sx)) {
+ if (zero_ext && sig_d[i] == State::S0 && (initval[i] == State::S0 || (!config->keepdc && initval[i] == State::Sx)) &&
+ (!has_reset || i >= GetSize(rst_value) || rst_value[i] == State::S0 || (!config->keepdc && rst_value[i] == State::Sx))) {
module->connect(sig_q[i], State::S0);
initvals.remove_init(sig_q[i]);
sig_d.remove(i);
@@ -175,8 +175,8 @@ struct WreduceWorker
continue;
}
- if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] &&
- (!has_reset || i >= GetSize(rst_value) || rst_value[i] == rst_value[i-1])) {
+ if (sign_ext && i > 0 && sig_d[i] == sig_d[i-1] && initval[i] == initval[i-1] && (!config->keepdc || initval[i] != State::Sx) &&
+ (!has_reset || i >= GetSize(rst_value) || (rst_value[i] == rst_value[i-1] && (!config->keepdc || rst_value[i] != State::Sx)))) {
module->connect(sig_q[i], sig_q[i-1]);
initvals.remove_init(sig_q[i]);
sig_d.remove(i);
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index da6d49433..ebe3dc536 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o
OBJS += passes/sat/assertpmux.o
OBJS += passes/sat/clk2fflogic.o
OBJS += passes/sat/async2sync.o
+OBJS += passes/sat/formalff.o
OBJS += passes/sat/supercover.o
OBJS += passes/sat/fmcombine.o
OBJS += passes/sat/mutate.o
diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc
index 46c76eba9..6fdf470b1 100644
--- a/passes/sat/async2sync.cc
+++ b/passes/sat/async2sync.cc
@@ -75,6 +75,9 @@ struct Async2syncPass : public Pass {
if (ff.has_gclk)
continue;
+ if (ff.has_clk && ff.sig_clk.is_fully_const())
+ ff.has_ce = ff.has_clk = ff.has_srst = false;
+
if (ff.has_clk)
{
if (ff.has_sr) {
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index b1b0567a0..2384ffced 100644
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.cc
@@ -233,7 +233,10 @@ struct Clk2fflogicPass : public Pass {
qval = past_q;
}
- if (ff.has_aload) {
+ // The check for a constant sig_aload is also done by opt_dff, but when using verific and running
+ // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
+ // generating a lot of extra logic.
+ if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) {
SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID);
if (!ff.is_fine)
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
new file mode 100644
index 000000000..209486a37
--- /dev/null
+++ b/passes/sat/formalff.cc
@@ -0,0 +1,549 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+#include "kernel/ffinit.h"
+#include "kernel/ff.h"
+#include "kernel/modtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+
+// Finds signal values with known constant or known unused values in the initial state
+struct InitValWorker
+{
+ Module *module;
+
+ ModWalker modwalker;
+ SigMap &sigmap;
+ FfInitVals initvals;
+
+ dict<RTLIL::SigBit, RTLIL::State> initconst_bits;
+ dict<RTLIL::SigBit, bool> used_bits;
+
+ InitValWorker(Module *module) : module(module), modwalker(module->design), sigmap(modwalker.sigmap)
+ {
+ modwalker.setup(module);
+ initvals.set(&modwalker.sigmap, module);
+
+ for (auto wire : module->wires())
+ if (wire->name.isPublic() || wire->get_bool_attribute(ID::keep))
+ for (auto bit : SigSpec(wire))
+ used_bits[sigmap(bit)] = true;
+ }
+
+ // Sign/Zero-extended indexing of individual port bits
+ static SigBit bit_in_port(RTLIL::Cell *cell, RTLIL::IdString port, RTLIL::IdString sign, int index)
+ {
+ auto sig_port = cell->getPort(port);
+ if (index < GetSize(sig_port))
+ return sig_port[index];
+ else if (cell->getParam(sign).as_bool())
+ return GetSize(sig_port) > 0 ? sig_port[GetSize(sig_port) - 1] : State::Sx;
+ else
+ return State::S0;
+ }
+
+ // Has the signal a known constant value in the initial state?
+ //
+ // For sync-only FFs outputs, this is their initval. For logic loops,
+ // multiple drivers or unknown cells this is Sx. For a small number of
+ // handled cells we recurse through their inputs. All results are cached.
+ RTLIL::State initconst(SigBit bit)
+ {
+ sigmap.apply(bit);
+
+ if (!bit.is_wire())
+ return bit.data;
+
+ auto it = initconst_bits.find(bit);
+ if (it != initconst_bits.end())
+ return it->second;
+
+ // Setting this temporarily to x takes care of any logic loops
+ initconst_bits[bit] = State::Sx;
+
+ pool<ModWalker::PortBit> portbits;
+ modwalker.get_drivers(portbits, {bit});
+
+ if (portbits.size() != 1)
+ return State::Sx;
+
+ ModWalker::PortBit portbit = *portbits.begin();
+ RTLIL::Cell *cell = portbit.cell;
+
+ if (RTLIL::builtin_ff_cell_types().count(cell->type))
+ {
+ FfData ff(&initvals, cell);
+
+ if (ff.has_aload || ff.has_sr || ff.has_arst || (!ff.has_clk && !ff.has_gclk)) {
+ for (auto bit_q : ff.sig_q) {
+ initconst_bits[sigmap(bit_q)] = State::Sx;
+ }
+ return State::Sx;
+ }
+
+ for (int i = 0; i < ff.width; i++) {
+ initconst_bits[sigmap(ff.sig_q[i])] = ff.val_init[i];
+ }
+
+ return ff.val_init[portbit.offset];
+ }
+
+ if (cell->type.in(ID($mux), ID($and), ID($or), ID($eq), ID($eqx), ID($initstate)))
+ {
+ if (cell->type == ID($mux))
+ {
+ SigBit sig_s = sigmap(cell->getPort(ID::S));
+ State init_s = initconst(sig_s);
+ State init_y;
+
+ if (init_s == State::S0) {
+ init_y = initconst(cell->getPort(ID::A)[portbit.offset]);
+ } else if (init_s == State::S1) {
+ init_y = initconst(cell->getPort(ID::B)[portbit.offset]);
+ } else {
+ State init_a = initconst(cell->getPort(ID::A)[portbit.offset]);
+ State init_b = initconst(cell->getPort(ID::B)[portbit.offset]);
+ init_y = init_a == init_b ? init_a : State::Sx;
+ }
+ initconst_bits[bit] = init_y;
+ return init_y;
+ }
+
+ if (cell->type.in(ID($and), ID($or)))
+ {
+ State init_a = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, portbit.offset));
+ State init_b = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, portbit.offset));
+ State init_y;
+ if (init_a == init_b)
+ init_y = init_a;
+ else if (cell->type == ID($and) && (init_a == State::S0 || init_b == State::S0))
+ init_y = State::S0;
+ else if (cell->type == ID($or) && (init_a == State::S1 || init_b == State::S1))
+ init_y = State::S1;
+ else
+ init_y = State::Sx;
+
+ initconst_bits[bit] = init_y;
+ return init_y;
+ }
+
+ if (cell->type.in(ID($eq), ID($eqx))) // Treats $eqx as $eq
+ {
+ if (portbit.offset > 0) {
+ initconst_bits[bit] = State::S0;
+ return State::S0;
+ }
+
+ SigSpec sig_a = cell->getPort(ID::A);
+ SigSpec sig_b = cell->getPort(ID::B);
+
+ State init_y = State::S1;
+
+ for (int i = 0; init_y != State::S0 && i < GetSize(sig_a); i++) {
+ State init_ai = initconst(bit_in_port(cell, ID::A, ID::A_SIGNED, i));
+ if (init_ai == State::Sx) {
+ init_y = State::Sx;
+ continue;
+ }
+ State init_bi = initconst(bit_in_port(cell, ID::B, ID::B_SIGNED, i));
+ if (init_bi == State::Sx)
+ init_y = State::Sx;
+ else if (init_ai != init_bi)
+ init_y = State::S0;
+ }
+
+ initconst_bits[bit] = init_y;
+ return init_y;
+ }
+
+ if (cell->type == ID($initstate))
+ {
+ initconst_bits[bit] = State::S1;
+ return State::S1;
+ }
+
+ log_assert(false);
+ }
+
+ return State::Sx;
+ }
+
+ RTLIL::Const initconst(SigSpec sig)
+ {
+ std::vector<RTLIL::State> bits;
+ for (auto bit : sig)
+ bits.push_back(initconst(bit));
+ return bits;
+ }
+
+ // Is the initial value of this signal used?
+ //
+ // An initial value of a signal is considered as used if it a) aliases a
+ // wire with a public name, an output wire or with a keep attribute b)
+ // combinationally drives such a wire or c) drive an input to an unknown
+ // cell.
+ //
+ // This recurses into driven cells for a small number of known handled
+ // celltypes. Results are cached and initconst is used to detect unused
+ // inputs for the handled celltypes.
+ bool is_initval_used(SigBit bit)
+ {
+ if (!bit.is_wire())
+ return false;
+
+ auto it = used_bits.find(bit);
+ if (it != used_bits.end())
+ return it->second;
+
+ used_bits[bit] = true; // Temporarily set to guard against logic loops
+
+ pool<ModWalker::PortBit> portbits;
+ modwalker.get_consumers(portbits, {bit});
+
+ for (auto portbit : portbits) {
+ RTLIL::Cell *cell = portbit.cell;
+ if (!cell->type.in(ID($mux), ID($and), ID($or), ID($mem_v2)) && !RTLIL::builtin_ff_cell_types().count(cell->type)) {
+ return true;
+ }
+ }
+
+ for (auto portbit : portbits)
+ {
+ RTLIL::Cell *cell = portbit.cell;
+ if (RTLIL::builtin_ff_cell_types().count(cell->type))
+ {
+ FfData ff(&initvals, cell);
+ if (ff.has_aload || ff.has_sr || ff.has_arst || ff.has_gclk || !ff.has_clk)
+ return true;
+ if (ff.has_ce && initconst(ff.sig_ce.as_bit()) == (ff.pol_ce ? State::S0 : State::S1))
+ continue;
+ if (ff.has_srst && initconst(ff.sig_ce.as_bit()) == (ff.pol_srst ? State::S1 : State::S0))
+ continue;
+
+ return true;
+ }
+ else if (cell->type == ID($mux))
+ {
+ State init_s = initconst(cell->getPort(ID::S).as_bit());
+ if (init_s == State::S0 && portbit.port == ID::B)
+ continue;
+ if (init_s == State::S1 && portbit.port == ID::A)
+ continue;
+ auto sig_y = cell->getPort(ID::Y);
+
+ if (is_initval_used(sig_y[portbit.offset]))
+ return true;
+ }
+ else if (cell->type.in(ID($and), ID($or)))
+ {
+ auto sig_a = cell->getPort(ID::A);
+ auto sig_b = cell->getPort(ID::B);
+ auto sig_y = cell->getPort(ID::Y);
+ if (GetSize(sig_y) != GetSize(sig_a) || GetSize(sig_y) != GetSize(sig_b))
+ return true; // TODO handle more of this
+ State absorbing = cell->type == ID($and) ? State::S0 : State::S1;
+ if (portbit.port == ID::A && initconst(sig_b[portbit.offset]) == absorbing)
+ continue;
+ if (portbit.port == ID::B && initconst(sig_a[portbit.offset]) == absorbing)
+ continue;
+
+ if (is_initval_used(sig_y[portbit.offset]))
+ return true;
+ }
+ else if (cell->type == ID($mem_v2))
+ {
+ // TODO Use mem.h instead to uniformily cover all cases, most
+ // likely requires processing all memories when initializing
+ // the worker
+ if (!portbit.port.in(ID::WR_DATA, ID::WR_ADDR, ID::RD_ADDR))
+ return true;
+
+ if (portbit.port == ID::WR_DATA)
+ {
+ if (initconst(cell->getPort(ID::WR_EN)[portbit.offset]) == State::S0)
+ continue;
+ }
+ else if (portbit.port == ID::WR_ADDR)
+ {
+ int port = portbit.offset / cell->getParam(ID::ABITS).as_int();
+ auto sig_en = cell->getPort(ID::WR_EN);
+ int width = cell->getParam(ID::WIDTH).as_int();
+
+ for (int i = port * width; i < (port + 1) * width; i++)
+ if (initconst(sig_en[i]) != State::S0)
+ return true;
+
+ continue;
+ }
+ else if (portbit.port == ID::RD_ADDR)
+ {
+ int port = portbit.offset / cell->getParam(ID::ABITS).as_int();
+ auto sig_en = cell->getPort(ID::RD_EN);
+
+ if (initconst(sig_en[port]) != State::S0)
+ return true;
+
+ continue;
+ }
+ else
+ return true;
+ }
+ else
+ log_assert(false);
+ }
+
+ used_bits[bit] = false;
+ return false;
+ }
+};
+
+struct FormalFfPass : public Pass {
+ FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
+ void help() override
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" formalff [options] [selection]\n");
+ log("\n");
+ log("This pass transforms clocked flip-flops to prepare a design for formal\n");
+ log("verification. If a design contains latches and/or multiple different clocks run\n");
+ log("the async2sync or clk2fflogic passes before using this pass.\n");
+ log("\n");
+ log(" -clk2ff\n");
+ log(" Replace all clocked flip-flops with $ff cells that use the implicit\n");
+ log(" global clock. This assumes, without checking, that the design uses a\n");
+ log(" single global clock. If that is not the case, the clk2fflogic pass\n");
+ log(" should be used instead.\n");
+ log("\n");
+ log(" -ff2anyinit\n");
+ log(" Replace uninitialized bits of $ff cells with $anyinit cells. An\n");
+ log(" $anyinit cell behaves exactly like an $ff cell with an undefined\n");
+ log(" initialization value. The difference is that $anyinit inhibits\n");
+ log(" don't-care optimizations and is used to track solver-provided values\n");
+ log(" in witness traces.\n");
+ log("\n");
+ log(" If combined with -clk2ff this also affects newly created $ff cells.\n");
+ log("\n");
+ log(" -anyinit2ff\n");
+ log(" Replaces $anyinit cells with uninitialized $ff cells. This performs the\n");
+ log(" reverse of -ff2anyinit and can be used, before running a backend pass\n");
+ log(" (or similar) that is not yet aware of $anyinit cells.\n");
+ log("\n");
+ log(" Note that after running -anyinit2ff, in general, performing don't-care\n");
+ log(" optimizations is not sound in a formal verification setting.\n");
+ log("\n");
+ log(" -fine\n");
+ log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n");
+ log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n");
+ log("\n");
+ log(" -setundef\n");
+ log(" Find FFs with undefined initialization values for which changing the\n");
+ log(" initialization does not change the observable behavior and initialize\n");
+ log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
+ log(" cells that drive wires with private names.\n");
+ log("\n");
+
+ // TODO: An option to check whether all FFs use the same clock before changing it to the global clock
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) override
+ {
+ bool flag_clk2ff = false;
+ bool flag_ff2anyinit = false;
+ bool flag_anyinit2ff = false;
+ bool flag_fine = false;
+ bool flag_setundef = false;
+
+ log_header(design, "Executing FORMALFF pass.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ if (args[argidx] == "-clk2ff") {
+ flag_clk2ff = true;
+ continue;
+ }
+ if (args[argidx] == "-ff2anyinit") {
+ flag_ff2anyinit = true;
+ continue;
+ }
+ if (args[argidx] == "-anyinit2ff") {
+ flag_anyinit2ff = true;
+ continue;
+ }
+ if (args[argidx] == "-fine") {
+ flag_fine = true;
+ continue;
+ }
+ if (args[argidx] == "-setundef") {
+ flag_setundef = true;
+ continue;
+ }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
+ log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
+
+ if (flag_ff2anyinit && flag_anyinit2ff)
+ log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
+
+ if (flag_fine && !flag_anyinit2ff)
+ log_cmd_error("The option -fine requries the -anyinit2ff option.\n");
+
+ if (flag_fine && flag_clk2ff)
+ log_cmd_error("The options -fine and -clk2ff are exclusive.\n");
+
+ for (auto module : design->selected_modules())
+ {
+ if (flag_setundef)
+ {
+ InitValWorker worker(module);
+
+ for (auto cell : module->selected_cells())
+ {
+ if (RTLIL::builtin_ff_cell_types().count(cell->type))
+ {
+ FfData ff(&worker.initvals, cell);
+ if (ff.has_aload || ff.has_sr || ff.has_arst || ff.val_init.is_fully_def())
+ continue;
+
+ if (ff.has_ce && // CE can make the initval stick around
+ worker.initconst(ff.sig_ce.as_bit()) != (ff.pol_ce ? State::S1 : State::S0) && // unless it's known active
+ (!ff.has_srst || ff.ce_over_srst ||
+ worker.initconst(ff.sig_srst.as_bit()) != (ff.pol_srst ? State::S1 : State::S0))) // or a srst with priority is known active
+ continue;
+
+ auto before = ff.val_init;
+ for (int i = 0; i < ff.width; i++)
+ if (ff.val_init[i] == State::Sx && !worker.is_initval_used(ff.sig_q[i]))
+ ff.val_init[i] = State::S0;
+
+ if (ff.val_init != before) {
+ log("Setting unused undefined initial value of %s.%s (%s) from %s to %s\n",
+ log_id(module), log_id(cell), log_id(cell->type),
+ log_const(before), log_const(ff.val_init));
+ worker.initvals.set_init(ff.sig_q, ff.val_init);
+ }
+ }
+ }
+ }
+ SigMap sigmap(module);
+ FfInitVals initvals(&sigmap, module);
+
+
+ for (auto cell : module->selected_cells())
+ {
+ if (flag_anyinit2ff && cell->type == ID($anyinit))
+ {
+ FfData ff(&initvals, cell);
+ ff.remove();
+ ff.is_anyinit = false;
+ ff.is_fine = flag_fine;
+ if (flag_fine)
+ for (int i = 0; i < ff.width; i++)
+ ff.slice({i}).emit();
+ else
+ ff.emit();
+
+ continue;
+ }
+
+ if (!RTLIL::builtin_ff_cell_types().count(cell->type))
+ continue;
+
+ FfData ff(&initvals, cell);
+ bool emit = false;
+
+ if (flag_clk2ff && ff.has_clk) {
+ if (ff.sig_clk.is_fully_const())
+ log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n",
+ log_id(cell), log_id(cell->type), log_id(module));
+
+ auto clk_wire = ff.sig_clk.is_wire() ? ff.sig_clk.as_wire() : nullptr;
+
+ if (clk_wire == nullptr) {
+ clk_wire = module->addWire(NEW_ID);
+ module->connect(RTLIL::SigBit(clk_wire), ff.sig_clk);
+ }
+
+ auto clk_polarity = ff.pol_clk ? State::S1 : State::S0;
+
+ std::string attribute = clk_wire->get_string_attribute(ID::replaced_by_gclk);
+
+ auto &attr = clk_wire->attributes[ID::replaced_by_gclk];
+
+ if (!attr.empty() && attr != clk_polarity)
+ log_error("CLK %s on %s (%s) from module %s also used with opposite polarity, run clk2fflogic instead.\n",
+ log_id(clk_wire), log_id(cell), log_id(cell->type), log_id(module));
+
+ attr = clk_polarity;
+ clk_wire->set_bool_attribute(ID::keep);
+
+ // TODO propagate the replaced_by_gclk attribute upwards throughout the hierarchy
+
+ ff.unmap_ce_srst();
+ ff.has_clk = false;
+ ff.has_gclk = true;
+ emit = true;
+ }
+
+ if (!ff.has_gclk) {
+ continue;
+ }
+
+ if (flag_ff2anyinit && !ff.val_init.is_fully_def())
+ {
+ ff.remove();
+ emit = false;
+
+ int cursor = 0;
+ while (cursor < ff.val_init.size())
+ {
+ bool is_anyinit = ff.val_init[cursor] == State::Sx;
+ std::vector<int> bits;
+ bits.push_back(cursor++);
+ while (cursor < ff.val_init.size() && (ff.val_init[cursor] == State::Sx) == is_anyinit)
+ bits.push_back(cursor++);
+
+ if ((int)bits.size() == ff.val_init.size()) {
+ // This check is only to make the private names more helpful for debugging
+ ff.is_anyinit = true;
+ emit = true;
+ break;
+ }
+
+ auto slice = ff.slice(bits);
+ slice.is_anyinit = is_anyinit;
+ slice.emit();
+ }
+ }
+
+ if (emit)
+ ff.emit();
+ }
+ }
+ }
+} FormalFfPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index 864d6f05d..1302b3383 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -216,7 +216,7 @@ QbfSolutionType call_qbf_solver(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 std::string smtbmc_cmd = stringf("%s -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1",
+ const std::string smtbmc_cmd = stringf("\"%s\" -s %s %s -t 1 -g --binary %s %s/problem%d.smt2 2>&1",
yosys_smtbmc_exe.c_str(), opt.get_solver_name().c_str(),
(opt.timeout != 0? stringf("--timeout %d", opt.timeout) : "").c_str(),
(opt.dump_final_smt2? "--dump-smt2 " + opt.dump_final_smt2_file : "").c_str(),
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index d085fab2d..18a25a097 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -81,6 +81,7 @@ struct SimShared
bool hide_internal = true;
bool writeback = false;
bool zinit = false;
+ bool hdlname = false;
int rstlen = 1;
FstData *fst = nullptr;
double start_time = 0;
@@ -157,6 +158,7 @@ struct SimInstance
dict<Wire*, pair<int, Const>> signal_database;
dict<Wire*, fstHandle> fst_handles;
+ dict<Wire*, fstHandle> fst_inputs;
dict<IdString, dict<int,fstHandle>> fst_memories;
SimInstance(SimShared *shared, std::string scope, Module *module, Cell *instance = nullptr, SimInstance *parent = nullptr) :
@@ -230,7 +232,7 @@ struct SimInstance
}
}
- if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
+ if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) {
FfData ff_data(nullptr, cell);
ff_state_t ff;
ff.past_d = Const(State::Sx, ff_data.width);
@@ -737,9 +739,17 @@ struct SimInstance
child.second->register_signals(id);
}
- void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(Wire*, int, bool)> register_signal)
+ void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, Wire*, int, bool)> register_signal)
{
- enter_scope(name());
+ int exit_scopes = 1;
+ if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) {
+ auto hdlname = instance->get_hdlname_attribute();
+ log_assert(!hdlname.empty());
+ for (auto name : hdlname)
+ enter_scope("\\" + name);
+ exit_scopes = hdlname.size();
+ } else
+ enter_scope(name());
dict<Wire*,bool> registers;
for (auto cell : module->cells())
@@ -755,13 +765,25 @@ struct SimInstance
for (auto signal : signal_database)
{
- register_signal(signal.first, signal.second.first, registers.count(signal.first)!=0);
+ if (shared->hdlname && signal.first->name.isPublic() && signal.first->has_attribute(ID::hdlname)) {
+ auto hdlname = signal.first->get_hdlname_attribute();
+ log_assert(!hdlname.empty());
+ auto signal_name = std::move(hdlname.back());
+ hdlname.pop_back();
+ for (auto name : hdlname)
+ enter_scope("\\" + name);
+ register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ for (auto name : hdlname)
+ exit_scope();
+ } else
+ register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0);
}
for (auto child : children)
child.second->write_output_header(enter_scope, exit_scope, register_signal);
- exit_scope();
+ for (int i = 0; i < exit_scopes; i++)
+ exit_scope();
}
void register_output_step_values(std::map<int,Const> *data)
@@ -820,7 +842,7 @@ struct SimInstance
return did_something;
}
- void addAdditionalInputs(std::map<Wire*,fstHandle> &inputs)
+ void addAdditionalInputs()
{
for (auto cell : module->cells())
{
@@ -831,7 +853,7 @@ struct SimInstance
for(auto &item : fst_handles) {
if (item.second==0) continue; // Ignore signals not found
if (sig_y == sigmap(item.first)) {
- inputs[sig_y.as_wire()] = item.second;
+ fst_inputs[sig_y.as_wire()] = item.second;
found = true;
break;
}
@@ -842,7 +864,21 @@ struct SimInstance
}
}
for (auto child : children)
- child.second->addAdditionalInputs(inputs);
+ child.second->addAdditionalInputs();
+ }
+
+ bool setInputs()
+ {
+ bool did_something = false;
+ for(auto &item : fst_inputs) {
+ std::string v = shared->fst->valueOf(item.second);
+ did_something |= set_state(item.first, Const::from_string(v));
+ }
+
+ for (auto child : children)
+ did_something |= child.second->setInputs();
+
+ return did_something;
}
void setState(dict<int, std::pair<SigBit,bool>> bits, std::string values)
@@ -1095,18 +1131,17 @@ struct SimWorker : SimShared
}
SigMap sigmap(topmod);
- std::map<Wire*,fstHandle> inputs;
for (auto wire : topmod->wires()) {
if (wire->port_input) {
fstHandle id = fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
if (id==0)
log_error("Unable to find required '%s' signal in file\n",(scope + "." + RTLIL::unescape_id(wire->name)).c_str());
- inputs[wire] = id;
+ top->fst_inputs[wire] = id;
}
}
- top->addAdditionalInputs(inputs);
+ top->addAdditionalInputs();
uint64_t startCount = 0;
uint64_t stopCount = 0;
@@ -1152,11 +1187,7 @@ struct SimWorker : SimShared
fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
if (verbose)
log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString());
- bool did_something = false;
- for(auto &item : inputs) {
- std::string v = fst->valueOf(item.second);
- did_something |= top->set_state(item.first, Const::from_string(v));
- }
+ bool did_something = top->setInputs();
if (initial) {
did_something |= top->setInitState();
@@ -1702,7 +1733,11 @@ struct VCDWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
[this]() { vcdfile << stringf("$upscope $end\n");},
- [this,use_signal](Wire *wire, int id, bool is_reg) { if (use_signal.at(id)) vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, wire->name[0] == '$' ? "\\" : "", log_id(wire)); }
+ [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
+ if (use_signal.at(id)) {
+ vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name);
+ }
+ }
);
vcdfile << stringf("$enddefinitions $end\n");
@@ -1760,11 +1795,10 @@ struct FSTWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
[this]() { fstWriterSetUpscope(fstfile); },
- [this,use_signal](Wire *wire, int id, bool is_reg) {
+ [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
if (!use_signal.at(id)) return;
fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
- stringf("%s%s", wire->name[0] == '$' ? "\\" : "", log_id(wire)).c_str(), 0);
-
+ name, 0);
mapping.emplace(id, fst_id);
}
);
@@ -1846,7 +1880,7 @@ struct AIWWriter : public OutputWriter
worker->top->write_output_header(
[](IdString) {},
[]() {},
- [this](Wire *wire, int id, bool) { mapping[wire] = id; }
+ [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; }
);
std::map<int, Yosys::RTLIL::Const> current;
@@ -1935,6 +1969,10 @@ struct SimPass : public Pass {
log(" write the simulation results to an AIGER witness file\n");
log(" (requires a *.aim file via -map)\n");
log("\n");
+ log(" -hdlname\n");
+ log(" use the hdlname attribute when writing simulation results\n");
+ log(" (preserves hierarchy in a flattened design)\n");
+ log("\n");
log(" -x\n");
log(" ignore constant x outputs in simulation file.\n");
log("\n");
@@ -2047,6 +2085,10 @@ struct SimPass : public Pass {
worker.outputfiles.emplace_back(std::unique_ptr<AIWWriter>(new AIWWriter(&worker, aiw_filename.c_str())));
continue;
}
+ if (args[argidx] == "-hdlname") {
+ worker.hdlname = true;
+ continue;
+ }
if (args[argidx] == "-n" && argidx+1 < args.size()) {
numcycles = atoi(args[++argidx].c_str());
worker.cycles_set = true;
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 61ee99ee7..656c36b84 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -65,7 +65,9 @@
#include "frontends/blif/blifparse.h"
#ifdef YOSYS_LINK_ABC
-extern "C" int Abc_RealMain(int argc, char *argv[]);
+namespace abc {
+ int Abc_RealMain(int argc, char *argv[]);
+}
#endif
USING_YOSYS_NAMESPACE
@@ -787,15 +789,15 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n",
module->name.c_str(), replace_tempdir(tempdir_name, tempdir_name, show_tempdir).c_str());
- std::string abc_script = stringf("read_blif %s/input.blif; ", tempdir_name.c_str());
+ std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", tempdir_name.c_str());
if (!liberty_files.empty() || !genlib_files.empty()) {
for (std::string liberty_file : liberty_files)
- abc_script += stringf("read_lib -w %s; ", liberty_file.c_str());
+ abc_script += stringf("read_lib -w \"%s\"; ", liberty_file.c_str());
for (std::string liberty_file : genlib_files)
- abc_script += stringf("read_library %s; ", liberty_file.c_str());
+ abc_script += stringf("read_library \"%s\"; ", liberty_file.c_str());
if (!constr_file.empty())
- abc_script += stringf("read_constr -v %s; ", constr_file.c_str());
+ abc_script += stringf("read_constr -v \"%s\"; ", constr_file.c_str());
} else
if (!lut_costs.empty())
abc_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str());
@@ -1083,7 +1085,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
fclose(f);
}
- buffer = stringf("%s -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str());
+ buffer = stringf("\"%s\" -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str());
log("Running ABC command: %s\n", replace_tempdir(buffer, tempdir_name, show_tempdir).c_str());
#ifndef YOSYS_LINK_ABC
@@ -1098,7 +1100,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
abc_argv[2] = strdup("-f");
abc_argv[3] = strdup(tmp_script_name.c_str());
abc_argv[4] = 0;
- int ret = Abc_RealMain(4, abc_argv);
+ int ret = abc::Abc_RealMain(4, abc_argv);
free(abc_argv[0]);
free(abc_argv[1]);
free(abc_argv[2]);
diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc
index a66e95e21..2f46c89f4 100644
--- a/passes/techmap/abc9_exe.cc
+++ b/passes/techmap/abc9_exe.cc
@@ -31,7 +31,9 @@
#endif
#ifdef YOSYS_LINK_ABC
-extern "C" int Abc_RealMain(int argc, char *argv[]);
+namespace abc {
+ int Abc_RealMain(int argc, char *argv[]);
+}
#endif
std::string fold_abc9_cmd(std::string str)
@@ -173,12 +175,12 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
if (!lut_costs.empty())
abc9_script += stringf("read_lut %s/lutdefs.txt; ", tempdir_name.c_str());
else if (!lut_file.empty())
- abc9_script += stringf("read_lut %s; ", lut_file.c_str());
+ abc9_script += stringf("read_lut \"%s\"; ", lut_file.c_str());
else
log_abort();
log_assert(!box_file.empty());
- abc9_script += stringf("read_box %s; ", box_file.c_str());
+ abc9_script += stringf("read_box \"%s\"; ", box_file.c_str());
abc9_script += stringf("&read %s/input.xaig; &ps; ", tempdir_name.c_str());
if (!script_file.empty()) {
@@ -262,7 +264,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
fclose(f);
}
- buffer = stringf("%s -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str());
+ buffer = stringf("\"%s\" -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str());
log("Running ABC command: %s\n", replace_tempdir(buffer, tempdir_name, show_tempdir).c_str());
#ifndef YOSYS_LINK_ABC
@@ -277,7 +279,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
abc9_argv[2] = strdup("-f");
abc9_argv[3] = strdup(tmp_script_name.c_str());
abc9_argv[4] = 0;
- int ret = Abc_RealMain(4, abc9_argv);
+ int ret = abc::Abc_RealMain(4, abc9_argv);
free(abc9_argv[0]);
free(abc9_argv[1]);
free(abc9_argv[2]);
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-19 10:47:27 +0000