aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-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
6 files changed, 621 insertions, 23 deletions
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;
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-19 15:59:09 +0000