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;