aboutsummaryrefslogtreecommitdiffstats
path: root/passes
diff options
context:
space:
mode:
Diffstat (limited to 'passes')
-rw-r--r--passes/cmds/rename.cc81
-rw-r--r--passes/cmds/setundef.cc24
-rw-r--r--passes/cmds/show.cc1
-rw-r--r--passes/fsm/fsm_detect.cc1
-rw-r--r--passes/hierarchy/submod.cc1
-rw-r--r--passes/memory/memory_map.cc84
-rw-r--r--passes/opt/opt_clean.cc2
-rw-r--r--passes/opt/wreduce.cc8
-rw-r--r--passes/sat/Makefile.inc1
-rw-r--r--passes/sat/clk2fflogic.cc5
-rw-r--r--passes/sat/formalff.cc549
-rw-r--r--passes/sat/sim.cc52
12 files changed, 777 insertions, 32 deletions
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index b49d5cdc2..45576c91c 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -106,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
@@ -147,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");
@@ -172,6 +234,7 @@ 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;
@@ -203,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;
@@ -309,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);
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/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/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_map.cc b/passes/memory/memory_map.cc
index fd5b1f1ad..e2f74c2e1 100644
--- a/passes/memory/memory_map.cc
+++ b/passes/memory/memory_map.cc
@@ -32,6 +32,7 @@ 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;
@@ -151,6 +152,8 @@ struct MemoryMapWorker
// 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()) {
@@ -164,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;
@@ -185,6 +198,8 @@ 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++)
@@ -194,24 +209,36 @@ struct MemoryMapWorker
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 (mem.wr_ports.empty() && (!keepdc || w_init.is_fully_def()))
+ else if (static_only && (!keepdc || w_init.is_fully_def()))
{
- data_reg_out[idx] = w_init;
+ 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;
@@ -223,18 +250,27 @@ struct MemoryMapWorker
RTLIL::Wire *w_out = module->addWire(w_out_name, 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 (mem.wr_ports.empty())
+ 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;
@@ -272,13 +308,13 @@ 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);
- if (!mem.wr_ports.empty())
+ if (!static_only)
{
for (int i = 0; i < mem.size; i++)
{
@@ -387,12 +423,19 @@ struct MemoryMapPass : public Pass {
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");
@@ -439,6 +482,12 @@ struct MemoryMapPass : public Pass {
keepdc = true;
continue;
}
+ if (args[argidx] == "-formal")
+ {
+ formal = true;
+ keepdc = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -449,6 +498,7 @@ struct MemoryMapPass : public Pass {
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/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/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/sim.cc b/passes/sat/sim.cc
index 53644c6b7..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;
@@ -231,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);
@@ -738,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())
@@ -756,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)
@@ -1712,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");
@@ -1770,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);
}
);
@@ -1856,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;
@@ -1945,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");
@@ -2057,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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-15 02:58:06 +0000