Merge pull request #3624 from jix/sim_yw

Changes to support SBY trace generation with the sim command

15 files changed, 1722 insertions, 113 deletions

diff --git a/Makefile b/Makefile
index 2a05fcc50..dbaf9e2b0 100644
--- a/Makefile
+++ b/Makefile
@@ -653,7 +653,7 @@ ifneq ($(ABCEXTERNAL),)
 kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"'
 endif
 endif
-OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o
+OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o
 ifeq ($(ENABLE_ZLIB),1)
 OBJS += kernel/fstdata.o
 endif
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 513f9d95a..4ef28be9f 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -19,6 +19,8 @@
 
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
+#include "kernel/json.h"
+#include "kernel/yw.h"
 #include "libs/json11/json11.hpp"
 
 USING_YOSYS_NAMESPACE
@@ -709,30 +711,19 @@ struct AigerWriter
 			f << it.second;
 	}
 
-	template<class T> static std::vector<std::string> witness_path(T *obj) {
-		std::vector<std::string> path;
-		if (obj->name.isPublic()) {
-			auto hdlname = obj->get_string_attribute(ID::hdlname);
-			for (auto token : split_tokens(hdlname))
-				path.push_back("\\" + token);
-		}
-		if (path.empty())
-			path.push_back(obj->name.str());
-		return path;
-	}
-
-	void write_ywmap(std::ostream &f)
+	void write_ywmap(PrettyJson &json)
 	{
-		f << "{\n";
-		f << "  \"version\": \"Yosys Witness Aiger Map\",\n";
-		f << stringf("  \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str());
-		f << stringf("  \"latch_count\": %d,\n", aig_l);
-		f << stringf("  \"input_count\": %d,\n", aig_i);
+		json.begin_object();
+		json.entry("version", "Yosys Witness Aiger map");
+		json.entry("gennerator", yosys_version_str);
 
-		dict<int, string> clock_lines;
-		dict<int, string> input_lines;
-		dict<int, string> init_lines;
-		dict<int, string> seq_lines;
+		json.entry("latch_count", aig_l);
+		json.entry("input_count", aig_i);
+
+		dict<int, Json> clock_lines;
+		dict<int, Json> input_lines;
+		dict<int, Json> init_lines;
+		dict<int, Json> seq_lines;
 
 		for (auto cell : module->cells())
 		{
@@ -751,21 +742,21 @@ struct AigerWriter
 					if (init_inputs.count(sig[i])) {
 						int a = init_inputs.at(sig[i]);
 						log_assert((a & 1) == 0);
-						init_lines[a] += json11::Json(json11::Json::object {
+						init_lines[a] = json11::Json(json11::Json::object {
 							{ "path", witness_path(wire) },
 							{ "input", (a >> 1) - 1 },
 							{ "offset", sig_qy[i].offset },
-						}).dump();
+						});
 					}
 
 					if (input_bits.count(sig[i])) {
 						int a = aig_map.at(sig[i]);
 						log_assert((a & 1) == 0);
-						seq_lines[a] += json11::Json(json11::Json::object {
+						seq_lines[a] = json11::Json(json11::Json::object {
 							{ "path", witness_path(wire) },
 							{ "input", (a >> 1) - 1 },
 							{ "offset", sig_qy[i].offset },
-						}).dump();
+						});
 					}
 				}
 			}
@@ -783,60 +774,55 @@ struct AigerWriter
 
 					int a = aig_map.at(sig[i]);
 					log_assert((a & 1) == 0);
-					input_lines[a] += json11::Json(json11::Json::object {
+					input_lines[a] = json11::Json(json11::Json::object {
 						{ "path", path },
 						{ "input", (a >> 1) - 1 },
 						{ "offset", i },
-					}).dump();
+					});
 
 					if (ywmap_clocks.count(sig[i])) {
 						int clock_mode = ywmap_clocks[sig[i]];
 						if (clock_mode != 3) {
-							clock_lines[a] += json11::Json(json11::Json::object {
+							clock_lines[a] = json11::Json(json11::Json::object {
 								{ "path", path },
 								{ "input", (a >> 1) - 1 },
 								{ "offset", i },
 								{ "edge", clock_mode == 1 ? "posedge" : "negedge" },
-							}).dump();
+							});
 						}
 					}
 				}
 			}
 		}
 
-		f << "  \"clocks\": [";
+		json.name("clocks");
+		json.begin_array();
 		clock_lines.sort();
-		const char *sep = "\n    ";
-		for (auto &it : clock_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ],\n";
+		for (auto &it : clock_lines)
+			json.value(it.second);
+		json.end_array();
 
-		f << "  \"inputs\": [";
+		json.name("inputs");
+		json.begin_array();
 		input_lines.sort();
-		sep = "\n    ";
-		for (auto &it : input_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ],\n";
+		for (auto &it : input_lines)
+			json.value(it.second);
+		json.end_array();
 
-		f << "  \"seqs\": [";
-		sep = "\n    ";
-		for (auto &it : seq_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ],\n";
+		json.name("seqs");
+		json.begin_array();
+		input_lines.sort();
+		for (auto &it : seq_lines)
+			json.value(it.second);
+		json.end_array();
 
-		f << "  \"inits\": [";
-		sep = "\n    ";
-		for (auto &it : init_lines) {
-			f << sep << it.second;
-			sep = ",\n    ";
-		}
-		f << "\n  ]\n}\n";
+		json.name("inits");
+		json.begin_array();
+		input_lines.sort();
+		for (auto &it : init_lines)
+			json.value(it.second);
+		json.end_array();
+		json.end_object();
 	}
 
 };
@@ -991,9 +977,12 @@ struct AigerBackend : public Backend {
 		if (!yw_map_filename.empty()) {
 			std::ofstream mapf;
 			mapf.open(yw_map_filename.c_str(), std::ofstream::trunc);
-			if (mapf.fail())
-				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
-			writer.write_ywmap(mapf);
+
+			PrettyJson json;
+
+			if (!json.write_to_file(yw_map_filename))
+				log_error("Can't open file `%s' for writing: %s\n", yw_map_filename.c_str(), strerror(errno));
+			writer.write_ywmap(json);
 		}
 	}
 } AigerBackend;
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 8368ab82d..4c43e91e7 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -28,6 +28,8 @@
 #include "kernel/celltypes.h"
 #include "kernel/log.h"
 #include "kernel/mem.h"
+#include "kernel/json.h"
+#include "kernel/yw.h"
 #include <string>
 
 USING_YOSYS_NAMESPACE
@@ -83,6 +85,22 @@ struct BtorWorker
 	vector<string> info_lines;
 	dict<int, int> info_clocks;
 
+	struct ywmap_btor_sig {
+		SigSpec sig;
+		Cell *cell = nullptr;
+
+		ywmap_btor_sig(const SigSpec &sig) : sig(sig) {}
+		ywmap_btor_sig(Cell *cell) : cell(cell) {}
+	};
+
+	vector<ywmap_btor_sig> ywmap_inputs;
+	vector<ywmap_btor_sig> ywmap_states;
+	dict<SigBit, int> ywmap_clock_bits;
+	dict<SigBit, int> ywmap_clock_inputs;
+
+
+	PrettyJson ywmap_json;
+
 	void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3))
 	{
 		va_list ap;
@@ -126,6 +144,50 @@ struct BtorWorker
 		return " " + infostr;
 	}
 
+	void ywmap_state(const SigSpec &sig) {
+		if (ywmap_json.active())
+			ywmap_states.emplace_back(sig);
+	}
+
+	void ywmap_state(Cell *cell) {
+		if (ywmap_json.active())
+			ywmap_states.emplace_back(cell);
+	}
+
+	void ywmap_input(const SigSpec &sig) {
+		if (ywmap_json.active())
+			ywmap_inputs.emplace_back(sig);
+	}
+
+	void emit_ywmap_btor_sig(const ywmap_btor_sig &btor_sig) {
+		if (btor_sig.cell == nullptr) {
+			if (btor_sig.sig.empty()) {
+				ywmap_json.value(nullptr);
+				return;
+			}
+			ywmap_json.begin_array();
+			ywmap_json.compact();
+			for (auto &chunk : btor_sig.sig.chunks()) {
+				log_assert(chunk.is_wire());
+
+				ywmap_json.begin_object();
+				ywmap_json.entry("path", witness_path(chunk.wire));
+				ywmap_json.entry("width", chunk.width);
+				ywmap_json.entry("offset", chunk.offset);
+				ywmap_json.end_object();
+			}
+			ywmap_json.end_array();
+		} else {
+			ywmap_json.begin_object();
+			ywmap_json.compact();
+			ywmap_json.entry("path", witness_path(btor_sig.cell));
+			Mem *mem = mem_cells[btor_sig.cell];
+			ywmap_json.entry("width", mem->width);
+			ywmap_json.entry("size", mem->size);
+			ywmap_json.end_object();
+		}
+	}
+
 	void btorf_push(const string &id)
 	{
 		if (verbose) {
@@ -617,7 +679,7 @@ struct BtorWorker
 			SigSpec sig_d = sigmap(cell->getPort(ID::D));
 			SigSpec sig_q = sigmap(cell->getPort(ID::Q));
 
-			if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
+			if ((!info_filename.empty() || ywmap_json.active()) && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
 			{
 				SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C));
 				int nid = get_sig_nid(sig_c);
@@ -629,7 +691,11 @@ struct BtorWorker
 				if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool())
 					negedge = true;
 
-				info_clocks[nid] |= negedge ? 2 : 1;
+				if (!info_filename.empty())
+					info_clocks[nid] |= negedge ? 2 : 1;
+
+				if (ywmap_json.active())
+					ywmap_clock_bits[sig_c] |= negedge ? 2 : 1;
 			}
 
 			IdString symbol;
@@ -662,6 +728,8 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(symbol));
 
+			ywmap_state(sig_q);
+
 			if (nid_init_val >= 0) {
 				int nid_init = next_nid++;
 				if (verbose)
@@ -683,6 +751,8 @@ struct BtorWorker
 
 			btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
 
+			ywmap_state(sig_y);
+
 			if (cell->type == ID($anyconst)) {
 				int nid2 = next_nid++;
 				btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
@@ -705,6 +775,8 @@ struct BtorWorker
 				btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
 				btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
 				btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
+
+				ywmap_state(sig_y);
 			}
 
 			add_nid_sig(initstate_nid, sig_y);
@@ -768,6 +840,8 @@ struct BtorWorker
 					nid_init_val = next_nid++;
 					btorf("%d state %d\n", nid_init_val, sid);
 
+					ywmap_state(nullptr);
+
 					for (int i = 0; i < mem->size; i++) {
 						Const thisword = initdata.extract(i*mem->width, mem->width);
 						if (thisword.is_fully_undef())
@@ -793,6 +867,8 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(mem->memid));
 
+			ywmap_state(cell);
+
 			if (nid_init_val >= 0)
 			{
 				int nid_init = next_nid++;
@@ -915,10 +991,13 @@ struct BtorWorker
 				int sid = get_bv_sid(GetSize(sig));
 
 				int nid_input = next_nid++;
-				if (is_init)
+				if (is_init) {
 					btorf("%d state %d\n", nid_input, sid);
-				else
+					ywmap_state(sig);
+				} else {
 					btorf("%d input %d\n", nid_input, sid);
+					ywmap_input(sig);
+				}
 
 				int nid_masked_input;
 				if (sig_mask_undef.is_fully_ones()) {
@@ -993,6 +1072,7 @@ struct BtorWorker
 							int sid = get_bv_sid(GetSize(s));
 							int nid = next_nid++;
 							btorf("%d input %d\n", nid, sid);
+							ywmap_input(s);
 							nid_width[nid] = GetSize(s);
 
 							for (int j = 0; j < GetSize(s); j++)
@@ -1075,12 +1155,15 @@ struct BtorWorker
 		return nid;
 	}
 
-	BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename) :
+	BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename, string ywmap_filename) :
 			f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), print_internal_names(print_internal_names), info_filename(info_filename)
 	{
 		if (!info_filename.empty())
 			infof("name %s\n", log_id(module));
 
+		if (!ywmap_filename.empty())
+			ywmap_json.write_to_file(ywmap_filename);
+
 		memories = Mem::get_all_memories(module);
 
 		dict<IdString, Mem*> mem_dict;
@@ -1094,6 +1177,20 @@ struct BtorWorker
 
 		btorf_push("inputs");
 
+		if (ywmap_json.active()) {
+			for (auto wire : module->wires())
+			{
+				auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+				if (gclk_attr == wire->attributes.end())
+					continue;
+				SigSpec sig = sigmap(wire);
+				if (gclk_attr->second == State::S1)
+					ywmap_clock_bits[sig] |= 1;
+				else if (gclk_attr->second == State::S0)
+					ywmap_clock_bits[sig] |= 2;
+			}
+		}
+
 		for (auto wire : module->wires())
 		{
 			if (wire->attributes.count(ID::init)) {
@@ -1111,6 +1208,7 @@ struct BtorWorker
 			int nid = next_nid++;
 
 			btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str());
+			ywmap_input(wire);
 			add_nid_sig(nid, sig);
 
 			if (!info_filename.empty()) {
@@ -1122,6 +1220,16 @@ struct BtorWorker
 						info_clocks[nid] |= 2;
 				}
 			}
+
+			if (ywmap_json.active()) {
+				for (int i = 0; i < GetSize(sig); i++) {
+					auto input_bit = SigBit(wire, i);
+					auto bit = sigmap(input_bit);
+					if (!ywmap_clock_bits.count(bit))
+						continue;
+					ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit];
+				}
+			}
 		}
 
 		btorf_pop("inputs");
@@ -1378,6 +1486,42 @@ struct BtorWorker
 				f << it;
 			f.close();
 		}
+
+		if (ywmap_json.active())
+		{
+			ywmap_json.begin_object();
+			ywmap_json.entry("version", "Yosys Witness BTOR map");
+			ywmap_json.entry("generator", yosys_version_str);
+
+			ywmap_json.name("clocks");
+			ywmap_json.begin_array();
+			for (auto &entry : ywmap_clock_inputs) {
+				if (entry.second != 1 && entry.second != 2)
+					continue;
+				log_assert(entry.first.is_wire());
+				ywmap_json.begin_object();
+				ywmap_json.compact();
+				ywmap_json.entry("path", witness_path(entry.first.wire));
+				ywmap_json.entry("offset", entry.first.offset);
+				ywmap_json.entry("edge", entry.second == 1 ? "posedge" : "negedge");
+				ywmap_json.end_object();
+			}
+			ywmap_json.end_array();
+
+			ywmap_json.name("inputs");
+			ywmap_json.begin_array();
+			for (auto &entry : ywmap_inputs)
+				emit_ywmap_btor_sig(entry);
+			ywmap_json.end_array();
+
+			ywmap_json.name("states");
+			ywmap_json.begin_array();
+			for (auto &entry : ywmap_states)
+				emit_ywmap_btor_sig(entry);
+			ywmap_json.end_array();
+
+			ywmap_json.end_object();
+		}
 	}
 };
 
@@ -1406,11 +1550,15 @@ struct BtorBackend : public Backend {
 		log("  -x\n");
 		log("    Output symbols for internal netnames (starting with '$')\n");
 		log("\n");
+		log("  -ywmap <filename>\n");
+		log("    Create a map file for conversion to and from Yosys witness traces\n");
+		log("\n");
 	}
 	void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
 	{
 		bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false;
 		string info_filename;
+		string ywmap_filename;
 
 		log_header(design, "Executing BTOR backend.\n");
 
@@ -1443,6 +1591,10 @@ struct BtorBackend : public Backend {
 				print_internal_names = true;
 				continue;
 			}
+			if (args[argidx] == "-ywmap" && argidx+1 < args.size()) {
+				ywmap_filename = args[++argidx];
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
@@ -1455,7 +1607,7 @@ struct BtorBackend : public Backend {
 		*f << stringf("; BTOR description generated by %s for module %s.\n",
 				yosys_version_str, log_id(topmod));
 
-		BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename);
+		BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename, ywmap_filename);
 
 		*f << stringf("; end of yosys output\n");
 	}
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index fe50ca7f6..1ab39a405 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -458,7 +458,7 @@ struct Smt2Worker
 	{
 		RTLIL::SigSpec sig_a, sig_b;
 		RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
-		bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
+		bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool();
 		int width = GetSize(sig_y);
 
 		if (type == 's' || type == 'S' || type == 'd' || type == 'b') {
@@ -483,6 +483,7 @@ struct Smt2Worker
 			if (ch == 'A') processed_expr += get_bv(sig_a);
 			else if (ch == 'B') processed_expr += get_bv(sig_b);
 			else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B));
+			else if (ch == 'S') processed_expr += get_bv(cell->getPort(ID::S));
 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
 			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
 			else processed_expr += ch;
@@ -639,6 +640,9 @@ struct Smt2Worker
 			if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)");
 			if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)");
 
+			if (cell->type == ID($bweqx)) return export_bvop(cell, "(bvxnor A B)", 'U');
+			if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U');
+
 			if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's');
 			if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's');
 			if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's');
@@ -994,7 +998,7 @@ struct Smt2Worker
 				if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
 					comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
 							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
-				if (contains_clock) {
+				if (wire->port_input && contains_clock) {
 					for (int i = 0; i < GetSize(sig); i++) {
 						bool is_posedge = clock_posedge.count(sig[i]);
 						bool is_negedge = clock_negedge.count(sig[i]);
@@ -1744,7 +1748,6 @@ struct Smt2Backend : public Backend {
 		log_push();
 		Pass::call(design, "bmuxmap");
 		Pass::call(design, "demuxmap");
-		Pass::call(design, "bwmuxmap");
 		log_pop();
 
 		size_t argidx;
diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py
index a1e65569d..8d0cc8112 100644
--- a/backends/smt2/witness.py
+++ b/backends/smt2/witness.py
@@ -110,6 +110,10 @@ class AigerMap:
     def __init__(self, mapfile):
         data = json.load(mapfile)
 
+        version = data.get("version") if isinstance(data, dict) else {}
+        if version != "Yosys Witness Aiger map":
+            raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}")
+
         self.latch_count = data["latch_count"]
         self.input_count = data["input_count"]
 
@@ -250,5 +254,157 @@ def yw2aiw(input, mapfile, output):
 
     click.echo(f"Converted {len(inyw)} time steps.")
 
+class BtorMap:
+    def __init__(self, mapfile):
+        self.data = data = json.load(mapfile)
+
+        version = data.get("version") if isinstance(data, dict) else {}
+        if version != "Yosys Witness BTOR map":
+            raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}")
+
+        self.sigmap = WitnessSigMap()
+
+        for mode in ("states", "inputs"):
+            for btor_signal_def in data[mode]:
+                if btor_signal_def is None:
+                    continue
+                if isinstance(btor_signal_def, dict):
+                    btor_signal_def["path"] = tuple(btor_signal_def["path"])
+                else:
+                    for chunk in btor_signal_def:
+                        chunk["path"] = tuple(chunk["path"])
+
+
+@cli.command(help="""
+Convert a BTOR witness trace into a Yosys witness trace.
+
+This requires a Yosys witness BTOR map file as generated by 'write_btor -ywmap'.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("mapfile", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def wit2yw(input, mapfile, output):
+    input_name = input.name
+    click.echo(f"Converting BTOR witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
+    click.echo(f"Using Yosys witness BTOR map file {mapfile.name!r}")
+    btor_map = BtorMap(mapfile)
+
+    input = filter(None, (line.split(';', 1)[0].strip() for line in input))
+
+    sat = next(input, None)
+    if sat != "sat":
+        raise click.ClickException(f"{input_name}: not a BTOR witness file")
+
+    props = next(input, None)
+
+    t = -1
+
+    line = next(input, None)
+
+    frames = []
+    bits = {}
+
+    while line and not line.startswith('.'):
+        current_t = int(line[1:].strip())
+        if line[0] == '#':
+            mode = "states"
+        elif line[0] == '@':
+            mode = "inputs"
+        else:
+            raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file")
+
+        if current_t > t:
+            t = current_t
+            values = WitnessValues()
+            array_inits = set()
+            frames.append(values)
+
+        line = next(input, None)
+        while line and line[0] not in "#@.":
+            if current_t > 0 and mode == "states":
+                line = next(input, None)
+                continue
+            tokens = line.split()
+            line = next(input, None)
+
+            btor_sig = btor_map.data[mode][int(tokens[0])]
+            btor_sigs = [btor_sig]
+
+            if btor_sig is None:
+                continue
+
+            if isinstance(btor_sig, dict):
+                addr = tokens[1]
+                if not addr.startswith('['):
+                    addr = '[*]'
+                    value = tokens[1]
+                else:
+                    value = tokens[2]
+                if not addr.endswith(']'):
+                    raise click.ClickException(f"{input_name}: expected address in BTOR witness file")
+                path = btor_sig["path"]
+                width = btor_sig["width"]
+                size = btor_sig["size"]
+                if addr == '[*]':
+                    btor_sigs = [
+                        [{
+                            "path": (*path, f"\\[{addr}]"),
+                            "width": width,
+                            "offset": 0,
+                        }]
+                        for addr in range(size)
+                        if (path, addr) not in array_inits
+                    ]
+                    array_inits.update((path, addr) for addr in range(size))
+                else:
+                    addr = int(addr[1:-1], 2)
+
+                    if addr < 0 or addr >= size:
+                        raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file")
+
+                    array_inits.add((path, addr))
+                    btor_sig = [{
+                        "path": (*path, f"\\[{addr}]"),
+                        "width": width,
+                        "offset": 0,
+                    }]
+                    btor_sigs = [btor_sig]
+            else:
+                value = tokens[1]
+
+            for btor_sig in btor_sigs:
+                value_bits = iter(reversed(value))
+
+                for chunk in btor_sig:
+                    offset = chunk["offset"]
+                    path = chunk["path"]
+                    for i in range(offset, offset + chunk["width"]):
+                        key = (path, i)
+                        bits[key] = mode == "inputs"
+                        values[key] = next(value_bits)
+
+                if next(value_bits, None) is not None:
+                    raise click.ClickException(f"{input_name}: excess bits in BTOR witness file")
+
+
+    if line is None:
+        raise click.ClickException(f"{input_name}: unexpected end of BTOR witness file")
+    if line.strip() != '.':
+        raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file")
+    if next(input, None) is not None:
+        raise click.ClickException(f"{input_name}: unexpected trailing data in BTOR witness file")
+
+    outyw = WriteWitness(output, 'yosys-witness wit2yw')
+
+    outyw.signals = coalesce_signals((), bits)
+    for clock in btor_map.data["clocks"]:
+        outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+    for values in frames:
+        outyw.step(values)
+
+    outyw.end_trace()
+    click.echo(f"Converted {outyw.t} time steps.")
+
 if __name__ == "__main__":
     cli()
diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py
index 8469b4162..39cfac41e 100644
--- a/backends/smt2/ywio.py
+++ b/backends/smt2/ywio.py
@@ -175,8 +175,9 @@ class WitnessSig:
         return self.sort_key < other.sort_key
 
 
-def coalesce_signals(signals):
-    bits = {}
+def coalesce_signals(signals, bits=None):
+    if bits is None:
+        bits = {}
     for sig in signals:
         for bit in sig.bits():
             if sig.init_only:
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 239381f85..39211d0c7 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -259,5 +259,6 @@ X(WR_PORTS)
 X(WR_PRIORITY_MASK)
 X(WR_WIDE_CONTINUATION)
 X(X)
+X(xprop_decoder)
 X(Y)
 X(Y_WIDTH)
diff --git a/kernel/json.cc b/kernel/json.cc
new file mode 100644
index 000000000..738746267
--- /dev/null
+++ b/kernel/json.cc
@@ -0,0 +1,172 @@
+/*
+ *  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/json.h"
+
+USING_YOSYS_NAMESPACE
+
+void PrettyJson::emit_to_log()
+{
+    struct LogTarget : public Target {
+        void emit(const char *data) override { log("%s", data); }
+    };
+
+    targets.push_back(std::unique_ptr<Target>(new LogTarget));
+}
+
+void PrettyJson::append_to_string(std::string &target)
+{
+    struct AppendStringTarget : public Target {
+        std::string &target;
+        AppendStringTarget(std::string &target) : target(target) {}
+        void emit(const char *data) override { target += data; }
+    };
+
+    targets.push_back(std::unique_ptr<Target>(new AppendStringTarget(target)));
+}
+
+bool PrettyJson::write_to_file(const std::string &path)
+{
+    struct WriteFileTarget : public Target {
+        std::ofstream target;
+        void emit(const char *data) override { target << data; }
+        void flush() override { target.flush(); }
+    };
+
+    auto target = std::unique_ptr<WriteFileTarget>(new WriteFileTarget);
+    target->target.open(path);
+    if (target->target.fail())
+        return false;
+    targets.push_back(std::unique_ptr<Target>(target.release()));
+    return true;
+}
+
+void PrettyJson::line(bool space_if_inline)
+{
+    if (compact_depth != INT_MAX) {
+        if (space_if_inline)
+            raw(" ");
+        return;
+    }
+    int indent = state.size() - (state.empty() ? 0 : state.back() == VALUE);
+    newline_indent.resize(1 + 2 * indent, ' ');
+    raw(newline_indent.c_str());
+}
+
+void PrettyJson::raw(const char *raw_json)
+{
+    for (auto &target : targets)
+        target->emit(raw_json);
+}
+
+void PrettyJson::flush()
+{
+    for (auto &target : targets)
+        target->flush();
+}
+
+void PrettyJson::begin_object()
+{
+    begin_value();
+    raw("{");
+    state.push_back(OBJECT_FIRST);
+}
+
+void PrettyJson::begin_array()
+{
+    begin_value();
+    raw("[");
+    state.push_back(ARRAY_FIRST);
+}
+
+void PrettyJson::end_object()
+{
+    Scope top_scope = state.back();
+    state.pop_back();
+    if (top_scope == OBJECT)
+        line(false);
+    else
+        log_assert(top_scope == OBJECT_FIRST);
+    raw("}");
+    end_value();
+}
+
+void PrettyJson::end_array()
+{
+    Scope top_scope = state.back();
+    state.pop_back();
+    if (top_scope == ARRAY)
+        line(false);
+    else
+        log_assert(top_scope == ARRAY_FIRST);
+    raw("]");
+    end_value();
+}
+
+void PrettyJson::name(const char *name)
+{
+    if (state.back() == OBJECT_FIRST) {
+        state.back() = OBJECT;
+        line(false);
+    } else {
+        raw(",");
+        line();
+    }
+    raw(Json(name).dump().c_str());
+    raw(": ");
+    state.push_back(VALUE);
+}
+
+void PrettyJson::begin_value()
+{
+    if (state.back() == ARRAY_FIRST) {
+        line(false);
+        state.back() = ARRAY;
+    } else if (state.back() == ARRAY) {
+        raw(",");
+        line();
+    } else {
+        log_assert(state.back() == VALUE);
+        state.pop_back();
+    }
+}
+
+void PrettyJson::end_value()
+{
+    if (state.empty()) {
+        raw("\n");
+        flush();
+    }
+    if (GetSize(state) < compact_depth)
+        compact_depth = INT_MAX;
+}
+
+void PrettyJson::value_json(const Json &value)
+{
+    begin_value();
+    raw(value.dump().c_str());
+    end_value();
+}
+
+void PrettyJson::entry_json(const char *name, const Json &value)
+{
+    this->name(name);
+    this->value(value);
+}
+
diff --git a/kernel/json.h b/kernel/json.h
new file mode 100644
index 000000000..c9aa0e045
--- /dev/null
+++ b/kernel/json.h
@@ -0,0 +1,104 @@
+/*
+ *  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.
+ *
+ */
+
+#ifndef JSON_H
+#define JSON_H
+
+#include "kernel/yosys.h"
+#include "libs/json11/json11.hpp"
+#include <functional>
+
+YOSYS_NAMESPACE_BEGIN
+
+using json11::Json;
+
+class PrettyJson
+{
+    enum Scope {
+        VALUE,
+        OBJECT_FIRST,
+        OBJECT,
+        ARRAY_FIRST,
+        ARRAY,
+    };
+
+    struct Target {
+        virtual void emit(const char *data) = 0;
+        virtual void flush() {};
+        virtual ~Target() {};
+    };
+
+    std::string newline_indent = "\n";
+    std::vector<std::unique_ptr<Target>> targets;
+    std::vector<Scope> state = {VALUE};
+    int compact_depth = INT_MAX;
+public:
+
+    void emit_to_log();
+    void append_to_string(std::string &target);
+    bool write_to_file(const std::string &path);
+
+    bool active() { return !targets.empty(); }
+
+    void compact() { compact_depth = GetSize(state); }
+
+    void line(bool space_if_inline = true);
+    void raw(const char *raw_json);
+    void flush();
+    void begin_object();
+    void begin_array();
+    void end_object();
+    void end_array();
+    void name(const char *name);
+    void begin_value();
+    void end_value();
+    void value_json(const Json &value);
+    void value(unsigned int value) { value_json(Json((int)value)); }
+    template<typename T>
+    void value(T &&value) { value_json(Json(std::forward<T>(value))); };
+
+    void entry_json(const char *name, const Json &value);
+    void entry(const char *name, unsigned int value) { entry_json(name, Json((int)value)); }
+    template<typename T>
+    void entry(const char *name, T &&value) { entry_json(name, Json(std::forward<T>(value))); };
+
+    template<typename T>
+    void object(const T &&values)
+    {
+        begin_object();
+        for (auto &item : values)
+            entry(item.first, item.second);
+        end_object();
+    }
+
+    template<typename T>
+    void array(const T &&values)
+    {
+        begin_object();
+        for (auto &item : values)
+            value(item);
+        end_object();
+    }
+};
+
+
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/yw.cc b/kernel/yw.cc
new file mode 100644
index 000000000..73e7710db
--- /dev/null
+++ b/kernel/yw.cc
@@ -0,0 +1,209 @@
+/*
+ *  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/yw.h"
+#include "libs/json11/json11.hpp"
+
+USING_YOSYS_NAMESPACE
+
+// Use the same formatting as witness.py uses
+static const char *pretty_name(IdString id)
+{
+	const char *c_str = id.c_str();
+	const char *p = c_str;
+
+	if (*p != '\\')
+		return c_str;
+	p++;
+
+	if (*p == '[') {
+		p++;
+		while (*p >= '0' && *p <= '9')
+			p++;
+		if (p[0] != ']' || p[1] != 0)
+			return c_str;
+		return c_str + 1;
+	}
+
+	if (!(*p >= 'a' && *p <= 'z') && !(*p >= 'A' && *p <= 'Z') && *p != '_')
+		return c_str;
+	p++;
+	while ((*p >= '0' && *p <= '9') || (*p >= 'a' && *p <= 'z') || (*p >= 'A' && *p <= 'Z') || *p == '_')
+		p++;
+
+	if (*p != 0)
+		return c_str;
+	return c_str + 1;
+}
+
+std::string IdPath::str() const
+{
+	std::string result;
+
+	for (auto &item : *this) {
+		const char *pretty = pretty_name(item);
+		if (pretty[0] == '[') {
+			result += pretty;
+			continue;
+		}
+		if (!result.empty())
+			result += '.';
+		result += pretty;
+		if (pretty[0] == '\\' || pretty[0] == '$')
+			result += ' ';
+	}
+
+	return result;
+}
+
+bool IdPath::get_address(int &addr) const
+{
+	if (empty())
+		return false;
+	auto &last = back();
+	if (!last.begins_with("\\["))
+		return false;
+	if (last == "\\[0]") {
+		addr = 0;
+		return true;
+	}
+	char first = last.c_str()[2];
+	if (first < '1' || first > '9')
+		return false;
+	char *endptr;
+	addr = std::strtol(last.c_str() + 2, &endptr, 10);
+	return endptr[0] == ']' && endptr[1] == 0;
+}
+
+static std::vector<IdString> get_path(const json11::Json &json)
+{
+	std::vector<IdString> result;
+	for (auto &path_item : json.array_items()) {
+		auto const &path_item_str = path_item.string_value();
+		if (path_item_str.empty())
+			return {};;
+		result.push_back(path_item_str);
+	}
+	return result;
+}
+
+ReadWitness::ReadWitness(const std::string &filename) :
+	filename(filename)
+{
+	std::ifstream f(filename.c_str());
+	if (f.fail() || GetSize(filename) == 0)
+		log_error("Cannot open file `%s`\n", filename.c_str());
+	std::stringstream buf;
+	buf << f.rdbuf();
+	std::string err;
+	json11::Json json = json11::Json::parse(buf.str(), err);
+	if (!err.empty())
+		log_error("Failed to parse `%s`: %s\n", filename.c_str(), err.c_str());
+
+	std::string format = json["format"].string_value();
+
+	if (format.empty())
+		log_error("Failed to parse `%s`: Unknown format\n", filename.c_str());
+	if (format != "Yosys Witness Trace")
+		log_error("Failed to parse `%s`: Unsupported format `%s`\n", filename.c_str(), format.c_str());
+
+	for (auto &clock_json : json["clocks"].array_items()) {
+		Clock clock;
+		clock.path = get_path(clock_json["path"]);
+		if (clock.path.empty())
+			log_error("Failed to parse `%s`: Missing path for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+		auto edge_str = clock_json["edge"];
+		if (edge_str.string_value() == "posedge")
+			clock.is_posedge = true;
+		else if (edge_str.string_value() == "negedge")
+			clock.is_negedge = true;
+		else
+			log_error("Failed to parse `%s`: Unknown edge type for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+		if (!clock_json["offset"].is_number())
+			log_error("Failed to parse `%s`: Unknown offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+		clock.offset = clock_json["offset"].int_value();
+		if (clock.offset < 0)
+			log_error("Failed to parse `%s`: Invalid offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+		clocks.push_back(clock);
+	}
+
+	int bits_offset = 0;
+	for (auto &signal_json : json["signals"].array_items()) {
+		Signal signal;
+		signal.bits_offset = bits_offset;
+		signal.path = get_path(signal_json["path"]);
+		if (signal.path.empty())
+			log_error("Failed to parse `%s`: Missing path for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+		if (!signal_json["width"].is_number())
+			log_error("Failed to parse `%s`: Unknown width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+		signal.width = signal_json["width"].int_value();
+		if (signal.width < 0)
+			log_error("Failed to parse `%s`: Invalid width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+		bits_offset += signal.width;
+		if (!signal_json["offset"].is_number())
+			log_error("Failed to parse `%s`: Unknown offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+		signal.offset = signal_json["offset"].int_value();
+		if (signal.offset < 0)
+			log_error("Failed to parse `%s`: Invalid offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+		signal.init_only = signal_json["init_only"].bool_value();
+		signals.push_back(signal);
+	}
+
+	for (auto &step_json : json["steps"].array_items()) {
+		Step step;
+		if (!step_json["bits"].is_string())
+			log_error("Failed to parse `%s`: Expected string as bits value for step %d\n", filename.c_str(), GetSize(steps));
+		step.bits = step_json["bits"].string_value();
+		for (char c : step.bits) {
+			if (c != '0' && c != '1' && c != 'x' && c != '?')
+				log_error("Failed to parse `%s`: Invalid bit '%c' value for step %d\n", filename.c_str(), c, GetSize(steps));
+		}
+		steps.push_back(step);
+	}
+}
+
+RTLIL::Const ReadWitness::get_bits(int t, int bits_offset, int width) const
+{
+	log_assert(t >= 0 && t < GetSize(steps));
+
+	const std::string &bits = steps[t].bits;
+
+	RTLIL::Const result(State::Sa, width);
+	result.bits.reserve(width);
+
+	int read_begin = GetSize(bits) - 1 - bits_offset;
+	int read_end = max(-1, read_begin - width);
+
+	min(width, GetSize(bits) - bits_offset);
+
+	for (int i = read_begin, j = 0; i > read_end; i--, j++) {
+		RTLIL::State bit = State::Sa;
+		switch (bits[i]) {
+			case '0': bit = State::S0; break;
+			case '1': bit = State::S1; break;
+			case 'x': bit = State::Sx; break;
+			case '?': bit = State::Sa; break;
+			default:
+				log_abort();
+		}
+		result.bits[j] = bit;
+	}
+
+	return result;
+}
diff --git a/kernel/yw.h b/kernel/yw.h
new file mode 100644
index 000000000..c2f5921b1
--- /dev/null
+++ b/kernel/yw.h
@@ -0,0 +1,182 @@
+/*
+ *  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.
+ *
+ */
+
+#ifndef YW_H
+#define YW_H
+
+#include "kernel/yosys.h"
+#include "kernel/mem.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct IdPath : public std::vector<RTLIL::IdString>
+{
+	template<typename... T>
+	IdPath(T&&... args) : std::vector<RTLIL::IdString>(std::forward<T>(args)...) { }
+	IdPath prefix() const { return {begin(), end() - !empty()}; }
+	std::string str() const;
+
+	bool has_address() const { int tmp; return get_address(tmp); };
+	bool get_address(int &addr) const;
+
+	int hash() const { return hashlib::hash_ops<std::vector<RTLIL::IdString>>::hash(*this); }
+};
+
+struct WitnessHierarchyItem {
+	RTLIL::Module *module;
+	RTLIL::Wire *wire = nullptr;
+	RTLIL::Cell *cell = nullptr;
+	Mem *mem = nullptr;
+
+	WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Wire *wire) : module(module), wire(wire) {}
+	WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Cell *cell) : module(module), cell(cell) {}
+	WitnessHierarchyItem(RTLIL::Module *module, Mem *mem) : module(module), mem(mem) {}
+};
+
+template<typename D, typename T>
+void witness_hierarchy(RTLIL::Module *module, D data, T callback);
+
+template<class T> static std::vector<std::string> witness_path(T *obj) {
+	std::vector<std::string> path;
+	if (obj->name.isPublic()) {
+		auto hdlname = obj->get_string_attribute(ID::hdlname);
+		for (auto token : split_tokens(hdlname))
+			path.push_back("\\" + token);
+	}
+	if (path.empty())
+		path.push_back(obj->name.str());
+	return path;
+}
+
+struct ReadWitness
+{
+	struct Clock {
+		IdPath path;
+		int offset;
+		bool is_posedge = false;
+		bool is_negedge = false;
+	};
+
+	struct Signal {
+		IdPath path;
+		int offset;
+		int width;
+		bool init_only;
+
+		int bits_offset;
+	};
+
+	struct Step {
+		std::string bits;
+	};
+
+	std::string filename;
+	std::vector<Clock> clocks;
+	std::vector<Signal> signals;
+	std::vector<Step> steps;
+
+	ReadWitness(const std::string &filename);
+
+	RTLIL::Const get_bits(int t, int bits_offset, int width) const;
+};
+
+template<typename D, typename T>
+void witness_hierarchy_recursion(IdPath &path, int hdlname_mode, RTLIL::Module *module, D data, T &callback)
+{
+	auto const &const_path = path;
+	size_t path_size = path.size();
+	for (auto wire : module->wires())
+	{
+		auto hdlname = hdlname_mode < 0 ? std::vector<std::string>() : wire->get_hdlname_attribute();
+		for (auto item : hdlname)
+			path.push_back("\\" + item);
+		if (hdlname.size() == 1 && path.back() == wire->name)
+			hdlname.clear();
+		if (!hdlname.empty())
+			callback(const_path, WitnessHierarchyItem(module, wire), data);
+		path.resize(path_size);
+		if (hdlname.empty() || hdlname_mode <= 0) {
+			path.push_back(wire->name);
+			callback(const_path, WitnessHierarchyItem(module, wire), data);
+			path.pop_back();
+		}
+	}
+
+	for (auto cell : module->cells())
+	{
+		Module *child = module->design->module(cell->type);
+		if (child == nullptr)
+			continue;
+
+		auto hdlname = hdlname_mode < 0 ? std::vector<std::string>() : cell->get_hdlname_attribute();
+		for (auto item : hdlname)
+			path.push_back("\\" + item);
+		if (hdlname.size() == 1 && path.back() == cell->name)
+			hdlname.clear();
+		if (!hdlname.empty()) {
+			D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data);
+			witness_hierarchy_recursion<D, T>(path, 1, child, child_data, callback);
+		}
+		path.resize(path_size);
+		if (hdlname.empty() || hdlname_mode <= 0) {
+			path.push_back(cell->name);
+			D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data);
+			witness_hierarchy_recursion<D, T>(path, hdlname.empty() ? hdlname_mode : -1, child, child_data, callback);
+			path.pop_back();
+		}
+	}
+
+	for (auto mem : Mem::get_all_memories(module)) {
+		std::vector<std::string> hdlname;
+
+		if (hdlname_mode >= 0 && mem.cell != nullptr)
+			hdlname = mem.cell->get_hdlname_attribute();
+		for (auto item : hdlname)
+			path.push_back("\\" + item);
+		if (hdlname.size() == 1 && path.back() == mem.cell->name)
+			hdlname.clear();
+		if (!hdlname.empty()) {
+			callback(const_path, WitnessHierarchyItem(module, &mem), data);
+		}
+		path.resize(path_size);
+
+		if (hdlname.empty() || hdlname_mode <= 0) {
+			path.push_back(mem.memid);
+			callback(const_path, WitnessHierarchyItem(module, &mem), data);
+			path.pop_back();
+
+			if (mem.cell != nullptr && mem.cell->name != mem.memid) {
+				path.push_back(mem.cell->name);
+				callback(const_path, WitnessHierarchyItem(module, &mem), data);
+				path.pop_back();
+			}
+		}
+	}
+}
+
+template<typename D, typename T>
+void witness_hierarchy(RTLIL::Module *module, D data, T callback)
+{
+	IdPath path;
+	witness_hierarchy_recursion<D, T>(path, 0, module, data, callback);
+}
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index 590a7eb1d..7293002f3 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -502,7 +502,15 @@ struct SetundefPass : public Pass {
 				}
 			}
 
-			module->rewrite_sigspecs(worker);
+			for (auto &it : module->cells_)
+				if (!it.second->get_bool_attribute(ID::xprop_decoder))
+					it.second->rewrite_sigspecs(worker);
+			for (auto &it : module->processes)
+				it.second->rewrite_sigspecs(worker);
+			for (auto &it : module->connections_) {
+				worker(it.first);
+				worker(it.second);
+			}
 
 			if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
 			{
diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
index 5dee72e1b..5e78ff9fc 100644
--- a/passes/cmds/xprop.cc
+++ b/passes/cmds/xprop.cc
@@ -252,7 +252,8 @@ struct XpropWorker
 		}
 
 		if (!driven_orig.empty()) {
-			module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+			auto decoder = module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+			decoder->set_bool_attribute(ID::xprop_decoder);
 		}
 		if (!driven_never_x.first.empty()) {
 			module->connect(driven_never_x);
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index e36379096..099df4be9 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -317,6 +317,172 @@ struct InitValWorker
 	}
 };
 
+struct ReplacedPort {
+	IdString name;
+	int offset;
+	bool clk_pol;
+};
+
+struct HierarchyWorker
+{
+	Design *design;
+	pool<Module *> pending;
+
+	dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs;
+
+	HierarchyWorker(Design *design) :
+		design(design)
+	{
+		for (auto module : design->modules())
+			pending.insert(module);
+	}
+
+	void propagate();
+
+	const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type);
+};
+
+// Propagates replaced clock signals
+struct PropagateWorker
+{
+	HierarchyWorker &hierarchy;
+
+	Module *module;
+	SigMap sigmap;
+
+	dict<SigBit, bool> replaced_clk_bits;
+	dict<SigBit, SigBit> not_drivers;
+
+	std::vector<ReplacedPort> replaced_clk_inputs;
+	std::vector<std::pair<SigBit, bool>> pending;
+
+	PropagateWorker(Module *module, HierarchyWorker &hierarchy) :
+		hierarchy(hierarchy), module(module), sigmap(module)
+	{
+		hierarchy.pending.erase(module);
+
+		for (auto wire : module->wires())
+			if (wire->has_attribute(ID::replaced_by_gclk))
+				replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false);
+
+		for (auto cell : module->cells()) {
+			if (cell->type.in(ID($not), ID($_NOT_))) {
+				auto sig_a = cell->getPort(ID::A);
+				auto &sig_y = cell->getPort(ID::Y);
+				sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
+
+				for (int i = 0; i < GetSize(sig_a); i++)
+					if (sig_a[i].is_wire())
+						not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i]));
+			} else {
+				for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type))
+					replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true);
+			}
+		}
+
+		while (!pending.empty()) {
+			auto current = pending.back();
+			pending.pop_back();
+			auto it = not_drivers.find(current.first);
+			if (it == not_drivers.end())
+				continue;
+
+			replace_clk_bit(it->second, !current.second, true);
+		}
+
+		for (auto cell : module->cells()) {
+			if (cell->type.in(ID($not), ID($_NOT_)))
+				continue;
+			for (auto &conn : cell->connections()) {
+				if (!cell->output(conn.first))
+					continue;
+				for (SigBit bit : conn.second) {
+					sigmap.apply(bit);
+					if (replaced_clk_bits.count(bit))
+						log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n",
+								log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module));
+				}
+			}
+		}
+
+		for (auto port : module->ports) {
+			auto wire = module->wire(port);
+			if (!wire->port_input)
+				continue;
+			for (int i = 0; i < GetSize(wire); i++) {
+				SigBit bit(wire, i);
+				sigmap.apply(bit);
+				auto it = replaced_clk_bits.find(bit);
+				if (it == replaced_clk_bits.end())
+					continue;
+				replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second});
+
+				if (it->second) {
+					bit = module->Not(NEW_ID, bit);
+				}
+			}
+		}
+	}
+
+	void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute)
+	{
+		sigmap.apply(bit);
+		if (!bit.is_wire())
+			log_error("XXX todo\n");
+
+		auto it = replaced_clk_bits.find(bit);
+		if (it != replaced_clk_bits.end()) {
+			if (it->second != polarity)
+				log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n",
+						log_signal(bit), log_id(module));
+			return;
+		}
+
+		replaced_clk_bits.emplace(bit, polarity);
+
+		if (add_attribute) {
+			Wire *clk_wire = bit.wire;
+			if (bit.offset != 0 || GetSize(bit.wire) != 1) {
+				clk_wire = module->addWire(NEW_ID);
+				module->connect(RTLIL::SigBit(clk_wire), bit);
+			}
+			clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0;
+			clk_wire->set_bool_attribute(ID::keep);
+		}
+
+		pending.emplace_back(bit, polarity);
+	}
+};
+
+const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type)
+{
+	static const std::vector<ReplacedPort> empty;
+	if (!cell_type.isPublic())
+		return empty;
+
+	Module *module = design->module(cell_type);
+	if (module == nullptr)
+		return empty;
+
+	auto it = replaced_clk_inputs.find(module);
+	if (it != replaced_clk_inputs.end())
+		return it->second;
+
+	if (pending.count(module)) {
+		PropagateWorker worker(module, *this);
+		return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second;
+	}
+
+	return empty;
+}
+
+
+void HierarchyWorker::propagate()
+{
+	while (!pending.empty())
+		PropagateWorker worker(pending.pop(), *this);
+}
+
 struct FormalFfPass : public Pass {
 	FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
 	void help() override
@@ -362,6 +528,15 @@ struct FormalFfPass : public Pass {
 		log("        them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
 		log("        cells that drive wires with private names.\n");
 		log("\n");
+		log("    -hierarchy\n");
+		log("        Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n");
+		log("        through the design hierarchy towards the toplevel inputs. This option\n");
+		log("        works on the whole design and ignores the selection.\n");
+		log("\n");
+		log("    -assume\n");
+		log("        Add assumptions that constrain wires with the 'replaced_by_gclk'\n");
+		log("        attribute to the value they would have before an active clock edge.\n");
+		log("\n");
 
 		// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
 	}
@@ -372,6 +547,8 @@ struct FormalFfPass : public Pass {
 		bool flag_anyinit2ff = false;
 		bool flag_fine = false;
 		bool flag_setundef = false;
+		bool flag_hierarchy = false;
+		bool flag_assume = false;
 
 		log_header(design, "Executing FORMALFF pass.\n");
 
@@ -398,12 +575,20 @@ struct FormalFfPass : public Pass {
 				flag_setundef = true;
 				continue;
 			}
+			if (args[argidx] == "-hierarchy") {
+				flag_hierarchy = true;
+				continue;
+			}
+			if (args[argidx] == "-assume") {
+				flag_assume = 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_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
+			log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
 
 		if (flag_ff2anyinit && flag_anyinit2ff)
 			log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
@@ -548,6 +733,33 @@ struct FormalFfPass : public Pass {
 					ff.emit();
 			}
 		}
+
+		if (flag_hierarchy) {
+			HierarchyWorker worker(design);
+			worker.propagate();
+		}
+
+		if (flag_assume) {
+			for (auto module : design->selected_modules()) {
+				std::vector<pair<SigBit, bool>> found;
+				for (auto wire : module->wires()) {
+					if (!wire->has_attribute(ID::replaced_by_gclk))
+						continue;
+					bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1;
+
+					found.emplace_back(SigSpec(wire), clk_pol);
+				}
+				for (auto pair : found) {
+					SigBit clk = pair.first;
+
+					if (pair.second)
+						clk = module->Not(NEW_ID, clk);
+
+					module->addAssume(NEW_ID, clk, State::S1);
+
+				}
+			}
+		}
 	}
 } FormalFfPass;
 
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 0084a1f28..cfe31968d 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -23,6 +23,8 @@
 #include "kernel/mem.h"
 #include "kernel/fstdata.h"
 #include "kernel/ff.h"
+#include "kernel/yw.h"
+#include "kernel/json.h"
 
 #include <ctime>
 
@@ -74,6 +76,17 @@ struct OutputWriter
 	SimWorker *worker;
 };
 
+struct SimInstance;
+struct TriggeredAssertion {
+	int step;
+	SimInstance *instance;
+	Cell *cell;
+
+	TriggeredAssertion(int step, SimInstance *instance, Cell *cell) :
+		step(step), instance(instance), cell(cell)
+	{ }
+};
+
 struct SimShared
 {
 	bool debug = false;
@@ -93,6 +106,9 @@ struct SimShared
 	bool ignore_x = false;
 	bool date = false;
 	bool multiclock = false;
+	int next_output_id = 0;
+	int step = 0;
+	std::vector<TriggeredAssertion> triggered_assertions;
 };
 
 void zinit(State &v)
@@ -152,11 +168,14 @@ struct SimInstance
 	dict<Cell*, ff_state_t> ff_database;
 	dict<IdString, mem_state_t> mem_database;
 	pool<Cell*> formal_database;
+	pool<Cell*> initstate_database;
 	dict<Cell*, IdString> mem_cells;
 
 	std::vector<Mem> memories;
 
 	dict<Wire*, pair<int, Const>> signal_database;
+	dict<IdString, std::map<int, pair<int, Const>>> trace_mem_database;
+	dict<std::pair<IdString, int>, Const> trace_mem_init_database;
 	dict<Wire*, fstHandle> fst_handles;
 	dict<Wire*, fstHandle> fst_inputs;
 	dict<IdString, dict<int,fstHandle>> fst_memories;
@@ -254,6 +273,8 @@ struct SimInstance
 			if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
 				formal_database.insert(cell);
 			}
+			if (cell->type == ID($initstate))
+				initstate_database.insert(cell);
 		}
 
 		if (shared->zinit)
@@ -300,6 +321,21 @@ struct SimInstance
 		return log_id(module->name);
 	}
 
+	vector<std::string> witness_full_path() const
+	{
+		if (instance != nullptr)
+			return parent->witness_full_path(instance);
+		return vector<std::string>();
+	}
+
+	vector<std::string> witness_full_path(Cell *cell) const
+	{
+		auto result = witness_full_path();
+		auto cell_path = witness_path(cell);
+		result.insert(result.end(), cell_path.begin(), cell_path.end());
+		return result;
+	}
+
 	Const get_state(SigSpec sig)
 	{
 		Const value;
@@ -325,7 +361,7 @@ struct SimInstance
 		log_assert(GetSize(sig) <= GetSize(value));
 
 		for (int i = 0; i < GetSize(sig); i++)
-			if (state_nets.at(sig[i]) != value[i]) {
+			if (value[i] != State::Sa && state_nets.at(sig[i]) != value[i]) {
 				state_nets.at(sig[i]) = value[i];
 				dirty_bits.insert(sig[i]);
 				did_something = true;
@@ -338,12 +374,23 @@ struct SimInstance
 
 	void set_memory_state(IdString memid, Const addr, Const data)
 	{
+		set_memory_state(memid, addr.as_int(), data);
+	}
+
+	void set_memory_state(IdString memid, int addr, Const data)
+	{
 		auto &state = mem_database[memid];
 
-		int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
+		bool dirty = false;
+
+		int offset = (addr - state.mem->start_offset) * state.mem->width;
 		for (int i = 0; i < GetSize(data); i++)
-			if (0 <= i+offset && i+offset < state.mem->size * state.mem->width)
-				state.data.bits[i+offset] = data.bits[i];
+			if (0 <= i+offset && i+offset < state.mem->size * state.mem->width && data.bits[i] != State::Sa)
+				if (state.data.bits[i+offset] != data.bits[i])
+					dirty = true, state.data.bits[i+offset] = data.bits[i];
+
+		if (dirty)
+			dirty_memories.insert(memid);
 	}
 
 	void set_memory_state_bit(IdString memid, int offset, State data)
@@ -351,7 +398,10 @@ struct SimInstance
 		auto &state = mem_database[memid];
 		if (offset >= state.mem->size * state.mem->width)
 			log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid));
-		state.data.bits[offset] = data;
+		if (state.data.bits[offset] != data) {
+			state.data.bits[offset] = data;
+			dirty_memories.insert(memid);
+		}
 	}
 
 	void update_cell(Cell *cell)
@@ -447,9 +497,14 @@ struct SimInstance
 				log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid));
 
 			if (addr.is_fully_def()) {
-				int index = addr.as_int() - mem.start_offset;
+				int addr_int = addr.as_int();
+				int index = addr_int - mem.start_offset;
 				if (index >= 0 && index < mem.size)
 					data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2);
+
+				for (int offset = 0; offset < 1 << port.wide_log2; offset++) {
+					register_memory_addr(id, addr_int + offset);
+				}
 			}
 
 			set_state(port.data, data);
@@ -604,7 +659,8 @@ struct SimInstance
 
 				if (addr.is_fully_def())
 				{
-					int index = addr.as_int() - mem.start_offset;
+					int addr_int = addr.as_int();
+					int index = addr_int - mem.start_offset;
 					if (index >= 0 && index < mem.size)
 						for (int i = 0; i < (mem.width << port.wide_log2); i++)
 							if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) {
@@ -612,6 +668,9 @@ struct SimInstance
 								dirty_memories.insert(mem.memid);
 								did_something = true;
 							}
+
+					for (int i = 0; i < 1 << port.wide_log2; i++)
+						register_memory_addr(it.first, addr_int + i);
 				}
 			}
 		}
@@ -625,7 +684,7 @@ struct SimInstance
 		return did_something;
 	}
 
-	void update_ph3()
+	void update_ph3(bool check_assertions)
 	{
 		for (auto &it : ff_database)
 		{
@@ -660,27 +719,42 @@ struct SimInstance
 			}
 		}
 
-		for (auto cell : formal_database)
+		if (check_assertions)
 		{
-			string label = log_id(cell);
-			if (cell->attributes.count(ID::src))
-				label = cell->attributes.at(ID::src).decode_string();
+			for (auto cell : formal_database)
+			{
+				string label = log_id(cell);
+				if (cell->attributes.count(ID::src))
+					label = cell->attributes.at(ID::src).decode_string();
+
+				State a = get_state(cell->getPort(ID::A))[0];
+				State en = get_state(cell->getPort(ID::EN))[0];
 
-			State a = get_state(cell->getPort(ID::A))[0];
-			State en = get_state(cell->getPort(ID::EN))[0];
+				if (en == State::S1 && (cell->type == ID($cover) ? a == State::S1 : a != State::S1)) {
+					shared->triggered_assertions.emplace_back(shared->step, this, cell);
+				}
 
-			if (cell->type == ID($cover) && en == State::S1 && a != State::S1)
-				log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
+				if (cell->type == ID($cover) && en == State::S1 && a == State::S1)
+					log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
 
-			if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
-				log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+				if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
+					log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
 
-			if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
-				log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+				if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
+					log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+			}
 		}
 
 		for (auto it : children)
-			it.second->update_ph3();
+			it.second->update_ph3(check_assertions);
+	}
+
+	void set_initstate_outputs(State state)
+	{
+		for (auto cell : initstate_database)
+			set_state(cell->getPort(ID::Y), state);
+		for (auto child : children)
+			child.second->set_initstate_outputs(state);
 	}
 
 	void writeback(pool<Module*> &wbmods)
@@ -741,7 +815,7 @@ 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(const char*, 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*, int, Wire*, int, bool)> register_signal)
 	{
 		int exit_scopes = 1;
 		if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) {
@@ -774,11 +848,45 @@ struct SimInstance
 				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);
+				register_signal(signal_name.c_str(), GetSize(signal.first), 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);
+				register_signal(log_id(signal.first->name), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0);
+		}
+
+		for (auto &trace_mem : trace_mem_database)
+		{
+			auto memid = trace_mem.first;
+			auto &mdb = mem_database.at(memid);
+			Cell *cell = mdb.mem->cell;
+
+			std::vector<std::string> hdlname;
+			std::string signal_name;
+			bool has_hdlname = shared->hdlname && cell != nullptr && cell->name.isPublic() && cell->has_attribute(ID::hdlname);
+
+			if (has_hdlname) {
+				hdlname = cell->get_hdlname_attribute();
+				log_assert(!hdlname.empty());
+				signal_name = std::move(hdlname.back());
+				hdlname.pop_back();
+				for (auto name : hdlname)
+					enter_scope("\\" + name);
+			} else {
+				signal_name = log_id(memid);
+			}
+
+			for (auto &trace_index : trace_mem.second) {
+				int output_id = trace_index.second.first;
+				int index = trace_index.first;
+				register_signal(
+						stringf("%s[%d]", signal_name.c_str(), (index + mdb.mem->start_offset)).c_str(),
+						mdb.mem->width, nullptr, output_id, true);
+			}
+
+			if (has_hdlname)
+				for (auto name : hdlname)
+					exit_scope();
 		}
 
 		for (auto child : children)
@@ -788,6 +896,30 @@ struct SimInstance
 			exit_scope();
 	}
 
+	void register_memory_addr(IdString memid, int addr)
+	{
+		auto &mdb = mem_database.at(memid);
+		auto &mem = *mdb.mem;
+		int index = addr - mem.start_offset;
+		if (index < 0 || index >= mem.size)
+			return;
+		auto it = trace_mem_database.find(memid);
+		if (it != trace_mem_database.end() && it->second.count(index))
+			return;
+		int output_id = shared->next_output_id++;
+		Const data;
+		if (!shared->output_data.empty()) {
+			auto init_it = trace_mem_init_database.find(std::make_pair(memid, addr));
+			if (init_it != trace_mem_init_database.end())
+				data = init_it->second;
+			else
+				data = mem.get_init_data().extract(index * mem.width, mem.width);
+			shared->output_data.front().second.emplace(output_id, data);
+		}
+		trace_mem_database[memid].emplace(index, make_pair(output_id, data));
+
+	}
+
 	void register_output_step_values(std::map<int,Const> *data)
 	{
 		for (auto &it : signal_database)
@@ -803,6 +935,26 @@ struct SimInstance
 			data->emplace(id, value);
 		}
 
+		for (auto &trace_mem : trace_mem_database)
+		{
+			auto memid = trace_mem.first;
+			auto &mdb = mem_database.at(memid);
+			auto &mem = *mdb.mem;
+			for (auto &trace_index : trace_mem.second)
+			{
+				int output_id = trace_index.second.first;
+				int index = trace_index.first;
+
+				auto value = mdb.data.extract(index * mem.width, mem.width);
+
+				if (trace_index.second.second == value)
+					continue;
+
+				trace_index.second.second = value;
+				data->emplace(output_id, value);
+			}
+		}
+
 		for (auto child : children)
 			child.second->register_output_step_values(data);
 	}
@@ -946,6 +1098,7 @@ struct SimWorker : SimShared
 	std::string timescale;
 	std::string sim_filename;
 	std::string map_filename;
+	std::string summary_filename;
 	std::string scope;
 
 	~SimWorker()
@@ -956,8 +1109,8 @@ struct SimWorker : SimShared
 
 	void register_signals()
 	{
-		int id = 1;
-		top->register_signals(id);
+		next_output_id = 1;
+		top->register_signals(top->shared->next_output_id);
 	}
 
 	void register_output_step(int t)
@@ -989,6 +1142,9 @@ struct SimWorker : SimShared
 
 	void update(bool gclk)
 	{
+		if (gclk)
+			step += 1;
+
 		while (1)
 		{
 			if (debug)
@@ -1006,7 +1162,7 @@ struct SimWorker : SimShared
 		if (debug)
 			log("\n-- ph3 --\n");
 
-		top->update_ph3();
+		top->update_ph3(gclk);
 	}
 
 	void initialize_stable_past()
@@ -1016,7 +1172,7 @@ struct SimWorker : SimShared
 		top->update_ph1();
 		if (debug)
 			log("\n-- ph3 (initialize) --\n");
-		top->update_ph3();
+		top->update_ph3(true);
 	}
 
 	void set_inports(pool<IdString> ports, State value)
@@ -1490,6 +1646,242 @@ struct SimWorker : SimShared
 		write_output_files();
 	}
 
+	struct FoundYWPath
+	{
+		SimInstance *instance;
+		Wire *wire;
+		IdString memid;
+		int addr;
+	};
+
+	struct YwHierarchy {
+		dict<IdPath, FoundYWPath> paths;
+	};
+
+	YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw)
+	{
+		YwHierarchy hierarchy;
+		pool<IdPath> paths;
+		dict<IdPath, pool<IdString>> mem_paths;
+
+		for (auto &signal : yw.signals)
+			paths.insert(signal.path);
+
+		for (auto &clock : yw.clocks)
+			paths.insert(clock.path);
+
+		for (auto &path : paths)
+			if (path.has_address())
+				mem_paths[path.prefix()].insert(path.back());
+
+		witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) {
+			if (item.cell != nullptr)
+				return instance->children.at(item.cell);
+			if (item.wire != nullptr) {
+				if (paths.count(path)) {
+					if (debug)
+						log("witness hierarchy: found wire %s\n", path.str().c_str());
+					bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
+					if (!inserted)
+						log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
+				}
+			} else if (item.mem) {
+				auto it = mem_paths.find(path);
+				if (it != mem_paths.end()) {
+					if (debug)
+						log("witness hierarchy: found mem %s\n", path.str().c_str());
+					IdPath word_path = path;
+					word_path.emplace_back();
+					for (auto addr_part : it->second) {
+						word_path.back() = addr_part;
+						int addr;
+						word_path.get_address(addr);
+						if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size)
+							continue;
+						bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
+						if (!inserted)
+							log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
+					}
+				}
+			}
+			return instance;
+		});
+
+		for (auto &path : paths)
+			if (!hierarchy.paths.count(path))
+				log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str());
+
+		dict<IdPath, dict<int, bool>> clock_inputs;
+
+		for (auto &clock : yw.clocks) {
+			if (clock.is_negedge == clock.is_posedge)
+				continue;
+			clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge);
+		}
+		for (auto &signal : yw.signals) {
+			auto it = clock_inputs.find(signal.path);
+			if (it == clock_inputs.end())
+				continue;
+
+			for (auto &clock_input : it->second) {
+				int offset = clock_input.first;
+				if (offset >= signal.offset && (offset - signal.offset) < signal.width) {
+					int clock_bits_offset = signal.bits_offset + (offset - signal.offset);
+
+					State expected = clock_input.second ? State::S0 : State::S1;
+
+					for (int t = 0; t < GetSize(yw.steps); t++) {
+						if (yw.get_bits(t, clock_bits_offset, 1) != expected)
+							log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t);
+					}
+				}
+			}
+		}
+		// TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file
+
+		return hierarchy;
+	}
+
+	void set_yw_state(const ReadWitness &yw, const YwHierarchy &hierarchy, int t)
+	{
+		log_assert(t >= 0 && t < GetSize(yw.steps));
+
+		for (auto &signal : yw.signals) {
+			if (signal.init_only && t >= 1)
+				continue;
+			auto found_path_it = hierarchy.paths.find(signal.path);
+			if (found_path_it == hierarchy.paths.end())
+				continue;
+			auto &found_path = found_path_it->second;
+
+			Const value = yw.get_bits(t, signal.bits_offset, signal.width);
+
+			if (debug)
+				log("yw: set %s to %s\n", signal.path.str().c_str(), log_const(value));
+
+			if (found_path.wire != nullptr) {
+				found_path.instance->set_state(
+						SigChunk(found_path.wire, signal.offset, signal.width),
+						value);
+			} else if (!found_path.memid.empty()) {
+				if (t >= 1)
+					found_path.instance->register_memory_addr(found_path.memid, found_path.addr);
+				else
+					found_path.instance->trace_mem_init_database.emplace(make_pair(found_path.memid, found_path.addr), value);
+				found_path.instance->set_memory_state(
+						found_path.memid, found_path.addr,
+						value);
+			}
+		}
+	}
+
+	void set_yw_clocks(const ReadWitness &yw, const YwHierarchy &hierarchy, bool active_edge)
+	{
+		for (auto &clock : yw.clocks) {
+			if (clock.is_negedge == clock.is_posedge)
+				continue;
+			auto found_path_it = hierarchy.paths.find(clock.path);
+			if (found_path_it == hierarchy.paths.end())
+				continue;
+			auto &found_path = found_path_it->second;
+
+			if (found_path.wire != nullptr) {
+				found_path.instance->set_state(
+						SigChunk(found_path.wire, clock.offset, 1),
+						active_edge == clock.is_posedge ? State::S1 : State::S0);
+			}
+		}
+	}
+
+	void run_cosim_yw_witness(Module *topmod, int append)
+	{
+		if (!clock.empty())
+			log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n");
+		if (!reset.empty())
+			log_cmd_error("The -reset option is not required nor supported when reading a Yosys witness file.\n");
+		if (multiclock)
+			log_warning("The -multiclock option is not required and ignored when reading a Yosys witness file.\n");
+
+		ReadWitness yw(sim_filename);
+
+		top = new SimInstance(this, scope, topmod);
+		register_signals();
+
+		YwHierarchy hierarchy = prepare_yw_hierarchy(yw);
+
+		if (yw.steps.empty()) {
+			log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str());
+		} else {
+			top->set_initstate_outputs(State::S1);
+			set_yw_state(yw, hierarchy, 0);
+			set_yw_clocks(yw, hierarchy, true);
+			initialize_stable_past();
+			register_output_step(0);
+
+			if (!yw.clocks.empty()) {
+				if (debug)
+					log("Simulating non-active clock edge.\n");
+				set_yw_clocks(yw, hierarchy, false);
+				update(false);
+				register_output_step(5);
+			}
+			top->set_initstate_outputs(State::S0);
+		}
+
+		for (int cycle = 1; cycle < GetSize(yw.steps) + append; cycle++)
+		{
+			if (verbose)
+				log("Simulating cycle %d.\n", cycle);
+			if (cycle < GetSize(yw.steps))
+				set_yw_state(yw, hierarchy, cycle);
+			set_yw_clocks(yw, hierarchy, true);
+			update(true);
+			register_output_step(10 * cycle);
+
+			if (!yw.clocks.empty()) {
+				if (debug)
+					log("Simulating non-active clock edge.\n");
+				set_yw_clocks(yw, hierarchy, false);
+				update(false);
+				register_output_step(5 + 10 * cycle);
+			}
+		}
+
+		register_output_step(10 * (GetSize(yw.steps) + append));
+		write_output_files();
+	}
+
+	void write_summary()
+	{
+		if (summary_filename.empty())
+			return;
+
+		PrettyJson json;
+		if (!json.write_to_file(summary_filename))
+			log_error("Can't open file `%s' for writing: %s\n", summary_filename.c_str(), strerror(errno));
+
+		json.begin_object();
+		json.entry("version", "Yosys sim summary");
+		json.entry("generator", yosys_version_str);
+		json.entry("steps", step);
+		json.entry("top", log_id(top->module->name));
+		json.name("assertions");
+		json.begin_array();
+		for (auto &assertion : triggered_assertions) {
+			json.begin_object();
+			json.entry("step", assertion.step);
+			json.entry("type", log_id(assertion.cell->type));
+			json.entry("path", assertion.instance->witness_full_path(assertion.cell));
+			auto src = assertion.cell->get_string_attribute(ID::src);
+			if (!src.empty()) {
+				json.entry("src", src);
+			}
+			json.end_object();
+		}
+		json.end_array();
+		json.end_object();
+	}
+
 	std::string define_signal(Wire *wire)
 	{
 		std::stringstream f;
@@ -1734,9 +2126,15 @@ 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](const char *name, Wire *wire, int id, bool is_reg) {
+			[this,use_signal](const char *name, int size, 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);
+					// Works around gtkwave trying to parse everything past the last [ in a signal
+					// name. While the emitted range doesn't necessarily match the wire's range,
+					// this is consistent with the range gtkwave makes up if it doesn't find a
+					// range
+					std::string range = strchr(name, '[') ? stringf("[%d:0]", size - 1) : std::string();
+					vcdfile << stringf("$var %s %d n%d %s%s%s $end\n", is_reg ? "reg" : "wire", size, id, name[0] == '$' ? "\\" : "", name, range.c_str());
+
 				}
 			}
 		);
@@ -1796,9 +2194,9 @@ 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](const char *name, Wire *wire, int id, bool is_reg) {
+			[this,use_signal](const char *name, int size, 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),
+				fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, size,
 												name, 0);
 				mapping.emplace(id, fst_id);
 			}
@@ -1881,7 +2279,7 @@ struct AIWWriter : public OutputWriter
 		worker->top->write_output_header(
 			[](IdString) {},
 			[]() {},
-			[this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; }
+			[this](const char */*name*/, int /*size*/, Wire *wire, int id, bool) { if (wire != nullptr) mapping[wire] = id; }
 		);
 
 		std::map<int, Yosys::RTLIL::Const> current;
@@ -2013,11 +2411,17 @@ struct SimPass : public Pass {
 		log("    -w\n");
 		log("        writeback mode: use final simulation state as new init state\n");
 		log("\n");
-		log("    -r\n");
-		log("        read simulation results file\n");
-		log("            File formats supported: FST, VCD, AIW and WIT\n");
+		log("    -r <filename>\n");
+		log("        read simulation or formal results file\n");
+		log("            File formats supported: FST, VCD, AIW, WIT and .yw\n");
 		log("            VCD support requires vcd2fst external tool to be present\n");
 		log("\n");
+		log("    -append <integer>\n");
+		log("        number of extra clock cycles to simulate for a Yosys witness input\n");
+		log("\n");
+		log("    -summary <filename>\n");
+		log("        write a JSON summary to the given file\n");
+		log("\n");
 		log("    -map <filename>\n");
 		log("        read file with port and latch symbols, needed for AIGER witness input\n");
 		log("\n");
@@ -2063,6 +2467,7 @@ struct SimPass : public Pass {
 	{
 		SimWorker worker;
 		int numcycles = 20;
+		int append = 0;
 		bool start_set = false, stop_set = false, at_set = false;
 
 		log_header(design, "Executing SIM pass (simulate the circuit).\n");
@@ -2146,12 +2551,22 @@ struct SimPass : public Pass {
 				worker.sim_filename = sim_filename;
 				continue;
 			}
+			if (args[argidx] == "-append" && argidx+1 < args.size()) {
+				append = atoi(args[++argidx].c_str());
+				continue;
+			}
 			if (args[argidx] == "-map" && argidx+1 < args.size()) {
 				std::string map_filename = args[++argidx];
 				rewrite_filename(map_filename);
 				worker.map_filename = map_filename;
 				continue;
 			}
+			if (args[argidx] == "-summary" && argidx+1 < args.size()) {
+				std::string summary_filename = args[++argidx];
+				rewrite_filename(summary_filename);
+				worker.summary_filename = summary_filename;
+				continue;
+			}
 			if (args[argidx] == "-scope" && argidx+1 < args.size()) {
 				worker.scope = args[++argidx];
 				continue;
@@ -2235,10 +2650,14 @@ struct SimPass : public Pass {
 				worker.run_cosim_aiger_witness(top_mod);
 			} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
 				worker.run_cosim_btor2_witness(top_mod);
+			} else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) {
+				worker.run_cosim_yw_witness(top_mod, append);
 			} else {
 				log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
 			}
 		}
+
+		worker.write_summary();
 	}
 } SimPass;