Merge branch 'master' of https://github.com/ALGCDG/yosys

12 files changed, 1454 insertions, 153 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 547d131ee..513f9d95a 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -19,6 +19,7 @@
 
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
+#include "libs/json11/json11.hpp"
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -61,6 +62,8 @@ struct AigerWriter
 	dict<SigBit, int> init_inputs;
 	int initstate_ff = 0;
 
+	dict<SigBit, int> ywmap_clocks;
+
 	int mkgate(int a0, int a1)
 	{
 		aig_m++, aig_a++;
@@ -159,6 +162,17 @@ struct AigerWriter
 					output_bits.insert(wirebit);
 				}
 			}
+
+			if (wire->width == 1) {
+				auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+				if (gclk_attr != wire->attributes.end()) {
+					SigBit bit = sigmap(wire);
+					if (gclk_attr->second == State::S1)
+						ywmap_clocks[bit] |= 1;
+					else if (gclk_attr->second == State::S0)
+						ywmap_clocks[bit] |= 2;
+				}
+			}
 		}
 
 		for (auto bit : input_bits)
@@ -186,6 +200,22 @@ struct AigerWriter
 				unused_bits.erase(D);
 				undriven_bits.erase(Q);
 				ff_map[Q] = D;
+
+				if (cell->type != ID($_FF_)) {
+					auto sig_clk = sigmap(cell->getPort(ID::C).as_bit());
+					ywmap_clocks[sig_clk] |= cell->type == ID($_DFF_N_) ? 2 : 1;
+				}
+				continue;
+			}
+
+			if (cell->type == ID($anyinit))
+			{
+				auto sig_d = sigmap(cell->getPort(ID::D));
+				auto sig_q = sigmap(cell->getPort(ID::Q));
+				for (int i = 0; i < sig_d.size(); i++) {
+					undriven_bits.erase(sig_q[i]);
+					ff_map[sig_q[i]] = sig_d[i];
+				}
 				continue;
 			}
 
@@ -678,6 +708,137 @@ struct AigerWriter
 		for (auto &it : wire_lines)
 			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)
+	{
+		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);
+
+		dict<int, string> clock_lines;
+		dict<int, string> input_lines;
+		dict<int, string> init_lines;
+		dict<int, string> seq_lines;
+
+		for (auto cell : module->cells())
+		{
+			if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_), ID($anyinit), ID($anyconst), ID($anyseq)))
+			{
+				// Use sig_q to get the FF output name, but sig to lookup aiger bits
+				auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q);
+				SigSpec sig = sigmap(sig_qy);
+
+				for (int i = 0; i < GetSize(sig_qy); i++) {
+					if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr)
+						continue;
+
+					auto wire = sig_qy[i].wire;
+
+					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 {
+							{ "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 {
+							{ "path", witness_path(wire) },
+							{ "input", (a >> 1) - 1 },
+							{ "offset", sig_qy[i].offset },
+						}).dump();
+					}
+				}
+			}
+		}
+
+		for (auto wire : module->wires())
+		{
+			SigSpec sig = sigmap(wire);
+			if (wire->port_input)
+			{
+				auto path = witness_path(wire);
+				for (int i = 0; i < GetSize(wire); i++) {
+					if (aig_map.count(sig[i]) == 0 || sig[i].wire == nullptr)
+						continue;
+
+					int a = aig_map.at(sig[i]);
+					log_assert((a & 1) == 0);
+					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 {
+								{ "path", path },
+								{ "input", (a >> 1) - 1 },
+								{ "offset", i },
+								{ "edge", clock_mode == 1 ? "posedge" : "negedge" },
+							}).dump();
+						}
+					}
+				}
+			}
+		}
+
+		f << "  \"clocks\": [";
+		clock_lines.sort();
+		const char *sep = "\n    ";
+		for (auto &it : clock_lines) {
+			f << sep << it.second;
+			sep = ",\n    ";
+		}
+		f << "\n  ],\n";
+
+		f << "  \"inputs\": [";
+		input_lines.sort();
+		sep = "\n    ";
+		for (auto &it : input_lines) {
+			f << sep << it.second;
+			sep = ",\n    ";
+		}
+		f << "\n  ],\n";
+
+		f << "  \"seqs\": [";
+		sep = "\n    ";
+		for (auto &it : seq_lines) {
+			f << sep << it.second;
+			sep = ",\n    ";
+		}
+		f << "\n  ],\n";
+
+		f << "  \"inits\": [";
+		sep = "\n    ";
+		for (auto &it : init_lines) {
+			f << sep << it.second;
+			sep = ",\n    ";
+		}
+		f << "\n  ]\n}\n";
+	}
+
 };
 
 struct AigerBackend : public Backend {
@@ -717,6 +878,9 @@ struct AigerBackend : public Backend {
 		log("    -no-startoffset\n");
 		log("        make indexes zero based, enable using map files with smt solvers.\n");
 		log("\n");
+		log("    -ywmap <filename>\n");
+		log("        write a map file for conversion to and from yosys witness traces.\n");
+		log("\n");
 		log("    -I, -O, -B, -L\n");
 		log("        If the design contains no input/output/assert/flip-flop then create one\n");
 		log("        dummy input/output/bad_state-pin or latch to make the tools reading the\n");
@@ -736,6 +900,7 @@ struct AigerBackend : public Backend {
 		bool lmode = false;
 		bool no_startoffset = false;
 		std::string map_filename;
+		std::string yw_map_filename;
 
 		log_header(design, "Executing AIGER backend.\n");
 
@@ -767,6 +932,10 @@ struct AigerBackend : public Backend {
 				verbose_map = true;
 				continue;
 			}
+			if (yw_map_filename.empty() && args[argidx] == "-ywmap" && argidx+1 < args.size()) {
+				yw_map_filename = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-no-startoffset") {
 				no_startoffset = true;
 				continue;
@@ -791,6 +960,9 @@ struct AigerBackend : public Backend {
 		}
 		extra_args(f, filename, args, argidx, !ascii_mode);
 
+		if (!yw_map_filename.empty() && !zinit_mode)
+			log_error("Currently -ywmap requires -zinit.\n");
+
 		Module *top_module = design->top_module();
 
 		if (top_module == nullptr)
@@ -815,6 +987,14 @@ struct AigerBackend : public Backend {
 				log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
 			writer.write_map(mapf, verbose_map, no_startoffset);
 		}
+
+		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);
+		}
 	}
 } AigerBackend;
 
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 7de5deadd..06de71018 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -446,25 +446,28 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in(ID($not), ID($neg), ID($_NOT_)))
+		if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos)))
 		{
 			string btor_op;
 			if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
 			if (cell->type == ID($neg)) btor_op = "neg";
-			log_assert(!btor_op.empty());
 
 			int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
 
 			bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
-
-			int sid = get_bv_sid(width);
 			int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
-
-			int nid = next_nid++;
-			btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
-
 			SigSpec sig = sigmap(cell->getPort(ID::Y));
 
+			// the $pos cell just passes through, all other cells need an actual operation applied
+			int nid = nid_a;
+			if (cell->type != ID($pos))
+			{
+				log_assert(!btor_op.empty());
+				int sid = get_bv_sid(width);
+				nid = next_nid++;
+				btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
+			}
+
 			if (GetSize(sig) < width) {
 				int sid = get_bv_sid(GetSize(sig));
 				int nid2 = next_nid++;
@@ -609,7 +612,7 @@ struct BtorWorker
 			goto okay;
 		}
 
-		if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
+		if (cell->type.in(ID($dff), ID($ff), ID($anyinit), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
 		{
 			SigSpec sig_d = sigmap(cell->getPort(ID::D));
 			SigSpec sig_q = sigmap(cell->getPort(ID::Q));
@@ -1109,6 +1112,16 @@ struct BtorWorker
 
 			btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str());
 			add_nid_sig(nid, sig);
+
+			if (!info_filename.empty()) {
+				auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+				if (gclk_attr != wire->attributes.end()) {
+					if (gclk_attr->second == State::S1)
+						info_clocks[nid] |= 1;
+					else if (gclk_attr->second == State::S0)
+						info_clocks[nid] |= 2;
+				}
+			}
 		}
 
 		btorf_pop("inputs");
diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h
index b4ffa87cd..073921cc4 100644
--- a/backends/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/cxxrtl.h
@@ -1575,6 +1575,27 @@ value<BitsY> mod_ss(const value<BitsA> &a, const value<BitsB> &b) {
 	return divmod_ss<BitsY>(a, b).second;
 }
 
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> modfloor_uu(const value<BitsA> &a, const value<BitsB> &b) {
+	return divmod_uu<BitsY>(a, b).second;
+}
+
+// GHDL Modfloor operator. Returns r=a mod b, such that r has the same sign as b and
+// a=b*N+r where N is some integer
+// In practical terms, when a and b have different signs and the remainder returned by divmod_ss is not 0
+// then return the remainder + b
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> modfloor_ss(const value<BitsA> &a, const value<BitsB> &b) {
+	value<BitsY> r;
+	r = divmod_ss<BitsY>(a, b).second;
+	if((b.is_neg() != a.is_neg()) && !r.is_zero())
+		return add_ss<BitsY>(b, r);
+	return r;
+}
+
+
 // Memory helper
 struct memory_index {
 	bool valid;
diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index 404755b1e..62768bd33 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -185,7 +185,7 @@ bool is_binary_cell(RTLIL::IdString type)
 		ID($and), ID($or), ID($xor), ID($xnor), ID($logic_and), ID($logic_or),
 		ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx),
 		ID($eq), ID($ne), ID($eqx), ID($nex), ID($gt), ID($ge), ID($lt), ID($le),
-		ID($add), ID($sub), ID($mul), ID($div), ID($mod));
+		ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($modfloor));
 }
 
 bool is_extending_cell(RTLIL::IdString type)
diff --git a/backends/jny/jny.cc b/backends/jny/jny.cc
index d801b144c..2b8d51b76 100644
--- a/backends/jny/jny.cc
+++ b/backends/jny/jny.cc
@@ -27,6 +27,8 @@
 #include <algorithm>
 #include <unordered_map>
 #include <vector>
+#include <sstream>
+#include <iterator>
 
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
@@ -116,17 +118,17 @@ struct JnyWriter
         _include_connections(connections), _include_attributes(attributes), _include_properties(properties)
          { }
 
-    void write_metadata(Design *design, uint16_t indent_level = 0)
+    void write_metadata(Design *design, uint16_t indent_level = 0, std::string invk = "")
     {
         log_assert(design != nullptr);
 
         design->sort();
 
         f << "{\n";
+        f << "  \"$schema\": \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\",\n";
         f << stringf("  \"generator\": \"%s\",\n", escape_string(yosys_version_str).c_str());
-        // XXX(aki): Replace this with a proper version info eventually:tm:
-        f << "  \"version\": \"0.0.0\",\n";
-
+        f << "  \"version\": \"0.0.1\",\n";
+        f << "  \"invocation\": \"" << escape_string(invk) << "\",\n";
         f << "  \"features\": [";
 
         size_t fnum{0};
@@ -409,11 +411,12 @@ struct JnyWriter
 struct JnyBackend : public Backend {
     JnyBackend() : Backend("jny", "generate design metadata") { }
     void help() override {
-        // XXX(aki): TODO: explicitly document the JSON schema
         //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
         log("\n");
         log("    jny [options] [selection]\n");
         log("\n");
+        log("Write JSON netlist metadata for the current design\n");
+        log("\n");
         log("    -no-connections\n");
         log("        Don't include connection information in the netlist output.\n");
         log("\n");
@@ -423,8 +426,8 @@ struct JnyBackend : public Backend {
         log("    -no-properties\n");
         log("        Don't include property information in the netlist output.\n");
         log("\n");
-        log("Write a JSON metadata for the current design\n");
-        log("\n");
+        log("The JSON schema for JNY output files is located in the \"jny.schema.json\" file\n");
+        log("which is located at \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\"\n");
         log("\n");
     }
 
@@ -453,12 +456,22 @@ struct JnyBackend : public Backend {
 
             break;
         }
+
+        // Compose invocation line
+        std::ostringstream invk;
+        if (!args.empty()) {
+            std::copy(args.begin(), args.end(),
+                std::ostream_iterator<std::string>(invk, " ")
+            );
+        }
+        invk << filename;
+
         extra_args(f, filename, args, argidx);
 
         log_header(design, "Executing jny backend.\n");
 
         JnyWriter jny_writer(*f, false, connections, attributes, properties);
-        jny_writer.write_metadata(design);
+        jny_writer.write_metadata(design, 0, invk.str());
     }
 
 } JnyBackend;
@@ -472,7 +485,7 @@ struct JnyPass : public Pass {
         log("\n");
         log("    jny [options] [selection]\n");
         log("\n");
-        log("Write a JSON netlist metadata for the current design\n");
+        log("Write JSON netlist metadata for the current design\n");
         log("\n");
         log("    -o <filename>\n");
         log("        write to the specified file.\n");
@@ -520,6 +533,15 @@ struct JnyPass : public Pass {
 
             break;
         }
+
+        // Compose invocation line
+        std::ostringstream invk;
+        if (!args.empty()) {
+            std::copy(args.begin(), args.end(),
+                std::ostream_iterator<std::string>(invk, " ")
+            );
+        }
+
         extra_args(args, argidx, design);
 
         std::ostream *f;
@@ -534,13 +556,14 @@ struct JnyPass : public Pass {
                 log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
             }
             f = ff;
+            invk << filename;
         } else {
             f = &buf;
         }
 
 
         JnyWriter jny_writer(*f, false, connections, attributes, properties);
-        jny_writer.write_metadata(design);
+        jny_writer.write_metadata(design, 0, invk.str());
 
         if (!filename.empty()) {
             delete f;
diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc
index 1b11de5ec..b5163aefe 100644
--- a/backends/rtlil/rtlil_backend.cc
+++ b/backends/rtlil/rtlil_backend.cc
@@ -75,7 +75,7 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
 			else if (str[i] == '\t')
 				f << stringf("\\t");
 			else if (str[i] < 32)
-				f << stringf("\\%03o", str[i]);
+				f << stringf("\\%03o", (unsigned char)str[i]);
 			else if (str[i] == '"')
 				f << stringf("\\\"");
 			else if (str[i] == '\\')
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index fb01308bd..3afe990e7 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -7,6 +7,7 @@ ifneq ($(CONFIG),emcc)
 # MSYS targets support yosys-smtbmc, but require a launcher script
 ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
 TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc.exe $(PROGRAM_PREFIX)yosys-smtbmc-script.py
+TARGETS += $(PROGRAM_PREFIX)yosys-witness.exe $(PROGRAM_PREFIX)yosys-witness-script.py
 # Needed to find the Python interpreter for yosys-smtbmc scripts.
 # Override if necessary, it is only used for msys2 targets.
 PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
@@ -15,18 +16,31 @@ $(PROGRAM_PREFIX)yosys-smtbmc-script.py: backends/smt2/smtbmc.py
 	$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
 		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
 
+$(PROGRAM_PREFIX)yosys-witness-script.py: backends/smt2/witness.py
+	$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
+		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+
 $(PROGRAM_PREFIX)yosys-smtbmc.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-smtbmc-script.py
 	$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
+
+$(PROGRAM_PREFIX)yosys-witness.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-witness-script.py
+	$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
 # Other targets
 else
-TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc
+TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc $(PROGRAM_PREFIX)yosys-witness
 
 $(PROGRAM_PREFIX)yosys-smtbmc: backends/smt2/smtbmc.py
 	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
 	$(Q) chmod +x $@.new
 	$(Q) mv $@.new $@
+
+$(PROGRAM_PREFIX)yosys-witness: backends/smt2/witness.py
+	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
+	$(Q) chmod +x $@.new
+	$(Q) mv $@.new $@
 endif
 
 $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
+$(eval $(call add_share_file,share/python3,backends/smt2/ywio.py))
 endif
 endif
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 7481e0510..54783cf1b 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -23,6 +23,7 @@
 #include "kernel/celltypes.h"
 #include "kernel/log.h"
 #include "kernel/mem.h"
+#include "libs/json11/json11.hpp"
 #include <string>
 
 USING_YOSYS_NAMESPACE
@@ -241,6 +242,17 @@ struct Smt2Worker
 
 		for (auto wire : module->wires())
 		{
+			auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+			if (gclk_attr != wire->attributes.end()) {
+				if (gclk_attr->second == State::S1)
+					clock_posedge.insert(sigmap(wire));
+				else if (gclk_attr->second == State::S0)
+					clock_negedge.insert(sigmap(wire));
+			}
+		}
+
+		for (auto wire : module->wires())
+		{
 			if (!wire->port_input || GetSize(wire) != 1)
 				continue;
 			SigBit bit = sigmap(wire);
@@ -449,7 +461,7 @@ struct Smt2Worker
 		bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
 		int width = GetSize(sig_y);
 
-		if (type == 's' || type == 'd' || type == 'b') {
+		if (type == 's' || type == 'S' || type == 'd' || type == 'b') {
 			width = max(width, GetSize(cell->getPort(ID::A)));
 			if (cell->hasPort(ID::B))
 				width = max(width, GetSize(cell->getPort(ID::B)));
@@ -462,7 +474,7 @@ struct Smt2Worker
 
 		if (cell->hasPort(ID::B)) {
 			sig_b = cell->getPort(ID::B);
-			sig_b.extend_u0(width, is_signed && !(type == 's'));
+			sig_b.extend_u0(width, (type == 'S') || (is_signed && !(type == 's')));
 		}
 
 		std::string processed_expr;
@@ -577,31 +589,41 @@ struct Smt2Worker
 			if (cell->type.in(ID($ff), ID($dff)))
 			{
 				registers.insert(cell);
+				for (auto chunk : cell->getPort(ID::Q).chunks())
+					if (chunk.is_wire())
+						decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire));
 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
 				register_bv(cell->getPort(ID::Q), idcounter++);
 				recursive_cells.erase(cell);
 				return;
 			}
 
-			if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq)))
+			if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq)))
 			{
+				auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
 				registers.insert(cell);
 				string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
 				if (cell->attributes.count(ID::reg))
 					infostr += " " + cell->attributes.at(ID::reg).decode_string();
-				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str()));
-				if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){
+				decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(QY)), infostr.c_str()));
+				if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::maximize)){
 					decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
-					log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
+					log("Wire %s is maximized\n", cell->getPort(QY).as_wire()->name.str().c_str());
 				}
-				else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){
+				else if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::minimize)){
 					decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
-					log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
+					log("Wire %s is minimized\n", cell->getPort(QY).as_wire()->name.str().c_str());
 				}
-				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y)));
+
+				bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
+				for (auto chunk : cell->getPort(QY).chunks())
+					if (chunk.is_wire())
+						decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+
+				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY)));
 				if (cell->type == ID($anyseq))
 					ex_input_eq.push_back(stringf("  (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
-				register_bv(cell->getPort(ID::Y), idcounter++);
+				register_bv(cell->getPort(QY), idcounter++);
 				recursive_cells.erase(cell);
 				return;
 			}
@@ -619,8 +641,8 @@ struct Smt2Worker
 			if (cell->type.in(ID($shift), ID($shiftx))) {
 				if (cell->getParam(ID::B_SIGNED).as_bool()) {
 					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
-							"(bvlshr A B) (bvlshr A (bvneg B)))",
-							GetSize(cell->getPort(ID::B)), 0), 's');
+							"(bvlshr A B) (bvshl A (bvneg B)))",
+							GetSize(cell->getPort(ID::B)), 0), 'S'); // type 'S' sign extends B
 				} else {
 					return export_bvop(cell, "(bvlshr A B)", 's');
 				}
@@ -748,6 +770,7 @@ struct Smt2Worker
 				log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
 
 			decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
+			decls.push_back(witness_memory(get_id(mem->memid), cell, mem));
 
 			string memstate;
 			if (has_async_wr) {
@@ -840,6 +863,7 @@ struct Smt2Worker
 		if (m != nullptr)
 		{
 			decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
+			decls.push_back(witness_cell(get_id(cell->name), cell));
 			string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
 
 			for (auto &conn : cell->connections())
@@ -920,7 +944,7 @@ struct Smt2Worker
 
 		pool<SigBit> reg_bits;
 		for (auto cell : module->cells())
-			if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
+			if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_), ID($anyinit))) {
 				// not using sigmap -- we want the net directly at the dff output
 				for (auto bit : cell->getPort(ID::Q))
 					reg_bits.insert(bit);
@@ -938,14 +962,19 @@ struct Smt2Worker
 
 		for (auto wire : module->wires()) {
 			bool is_register = false;
-			for (auto bit : SigSpec(wire))
+			bool contains_clock = false;
+			for (auto bit : SigSpec(wire)) {
 				if (reg_bits.count(bit))
 					is_register = true;
+				auto sig_bit = sigmap(bit);
+				if (clock_posedge.count(sig_bit) || clock_negedge.count(sig_bit))
+					contains_clock = true;
+			}
 			bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
 			if (is_smtlib2_comb_expr && !is_smtlib2_module)
 				log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
 					  log_id(wire));
-			if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
+			if (wire->port_id || is_register || contains_clock || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
 				RTLIL::SigSpec sig = sigmap(wire);
 				std::vector<std::string> comments;
 				if (wire->port_input)
@@ -956,9 +985,20 @@ struct Smt2Worker
 					comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
 				if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic()))
 					comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
-				if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
+				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) {
+					for (int i = 0; i < GetSize(sig); i++) {
+						bool is_posedge = clock_posedge.count(sig[i]);
+						bool is_negedge = clock_negedge.count(sig[i]);
+						if (is_posedge != is_negedge)
+							comments.push_back(witness_signal(
+									is_posedge ? "posedge" : "negedge", 1, i, get_id(wire), -1, wire));
+					}
+				}
+				if (wire->port_input)
+					comments.push_back(witness_signal("input", wire->width, 0, get_id(wire), -1, wire));
 				std::string smtlib2_comb_expr;
 				if (is_smtlib2_comb_expr) {
 					smtlib2_comb_expr =
@@ -968,6 +1008,8 @@ struct Smt2Worker
 					if (!bvmode && GetSize(sig) > 1)
 						log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
 							  log_id(module), log_id(wire));
+
+					comments.push_back(witness_signal("blackbox", wire->width, 0, get_id(wire), -1, wire));
 				}
 				auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
 				if (bvmode && GetSize(sig) > 1) {
@@ -1136,7 +1178,7 @@ struct Smt2Worker
 					ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str()));
 				}
 
-				if (cell->type.in(ID($ff), ID($dff)))
+				if (cell->type.in(ID($ff), ID($dff), ID($anyinit)))
 				{
 					std::string expr_d = get_bv(cell->getPort(ID::D));
 					std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state");
@@ -1435,6 +1477,90 @@ struct Smt2Worker
 			f << "true)";
 		f << stringf(" ; end of module %s\n", get_id(module));
 	}
+
+	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;
+	}
+
+	std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire)
+	{
+		std::vector<std::string> hiername;
+		const char *wire_name = wire->name.c_str();
+		if (wire_name[0] == '\\') {
+			auto hdlname = wire->get_string_attribute(ID::hdlname);
+			for (auto token : split_tokens(hdlname))
+				hiername.push_back("\\" + token);
+		}
+		if (hiername.empty())
+			hiername.push_back(wire->name.str());
+
+		std::string line = "; yosys-smt2-witness ";
+		(json11::Json { json11::Json::object {
+			{ "type", type },
+			{ "offset", offset },
+			{ "width", width },
+			{ "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
+			{ "path", witness_path(wire) },
+		}}).dump(line);
+		line += "\n";
+		return line;
+	}
+
+	std::string witness_cell(const char *smtname, RTLIL::Cell *cell)
+	{
+		std::string line = "; yosys-smt2-witness ";
+		(json11::Json {json11::Json::object {
+			{ "type", "cell" },
+			{ "smtname", smtname },
+			{ "path", witness_path(cell) },
+		}}).dump(line);
+		line += "\n";
+		return line;
+	}
+
+	std::string witness_memory(const char *smtname, RTLIL::Cell *cell, Mem *mem)
+	{
+		json11::Json::array uninitialized;
+		auto init_data = mem->get_init_data();
+
+		int cursor = 0;
+
+		while (cursor < init_data.size()) {
+			while (cursor < init_data.size() && init_data[cursor] != State::Sx)
+				cursor++;
+			int offset = cursor;
+			while (cursor < init_data.size() && init_data[cursor] == State::Sx)
+				cursor++;
+			int width = cursor - offset;
+			if (width)
+				uninitialized.push_back(json11::Json::object {
+					{"width", width},
+					{"offset", offset},
+				});
+		}
+
+		std::string line = "; yosys-smt2-witness ";
+		(json11::Json { json11::Json::object {
+			{ "type", "mem" },
+			{ "width", mem->width },
+			{ "size", mem->size },
+			{ "rom", mem->wr_ports.empty() },
+			{ "statebv", statebv },
+			{ "smtname", smtname },
+			{ "uninitialized", uninitialized },
+			{ "path", witness_path(cell) },
+		}}).dump(line);
+		line += "\n";
+		return line;
+	}
 };
 
 struct Smt2Backend : public Backend {
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 137182f33..5f05287de 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -17,9 +17,10 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import os, sys, getopt, re
+import os, sys, getopt, re, bisect
 ##yosys-sys-path##
 from smtio import SmtIo, SmtOpts, MkVcd
+from ywio import ReadWitness, WriteWitness, WitnessValues
 from collections import defaultdict
 
 got_topt = False
@@ -28,6 +29,8 @@ step_size = 1
 num_steps = 20
 append_steps = 0
 vcdfile = None
+inywfile = None
+outywfile = None
 cexfile = None
 aimfile = None
 aiwfile = None
@@ -51,6 +54,7 @@ smtctop = None
 noinit = False
 binarymode = False
 keep_going = False
+check_witness = False
 so = SmtOpts()
 
 
@@ -94,6 +98,9 @@ def usage():
         the AIGER witness file does not include the status and
         properties lines.
 
+    --yw <yosys_witness_filename>
+        read a Yosys witness.
+
     --btorwit <btor_witness_filename>
         read a BTOR witness.
 
@@ -121,6 +128,9 @@ def usage():
         (hint: use 'write_smt2 -wires' for maximum
         coverage of signals in generated VCD file)
 
+    --dump-yw <yw_filename>
+        write trace as a Yosys witness trace
+
     --dump-vlogtb <verilog_filename>
         write trace as Verilog test bench
 
@@ -161,15 +171,19 @@ def usage():
         covering all found failed assertions, the character '%' is
         replaced in all dump filenames with an increasing number.
 
+    --check-witness
+        check that the used witness file contains sufficient
+        constraints to force an assertion failure.
+
 """ + so.helpmsg())
     sys.exit(1)
 
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
-             "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
-             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"])
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
+             "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
+             "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"])
 except:
     usage()
 
@@ -204,10 +218,14 @@ for o, a in opts:
             aiwfile = a + ".aiw"
     elif o == "--aig-noheader":
         aigheader = False
+    elif o == "--yw":
+        inywfile = a
     elif o == "--btorwit":
         btorwitfile = a
     elif o == "--dump-vcd":
         vcdfile = a
+    elif o == "--dump-yw":
+        outywfile = a
     elif o == "--dump-vlogtb":
         vlogtbfile = a
     elif o == "--vlogtb-top":
@@ -244,6 +262,8 @@ for o, a in opts:
         binarymode = True
     elif o == "--keep-going":
         keep_going = True
+    elif o == "--check-witness":
+        check_witness = True
     elif so.handle(o, a):
         pass
     else:
@@ -462,7 +482,8 @@ if cexfile is not None:
             constr_assumes[step].append((cexfile, smtexpr))
 
             if not got_topt:
-                skip_steps = max(skip_steps, step)
+                if not check_witness:
+                    skip_steps = max(skip_steps, step)
                 num_steps = max(num_steps, step+1)
 
 if aimfile is not None:
@@ -595,13 +616,119 @@ if aimfile is not None:
                     constr_assumes[step].append((cexfile, smtexpr))
 
             if not got_topt:
-                skip_steps = max(skip_steps, step)
+                if not check_witness:
+                    skip_steps = max(skip_steps, step)
                 # some solvers optimize the properties so that they fail one cycle early,
                 # thus we check the properties in the cycle the aiger witness ends, and
                 # if that doesn't work, we check the cycle after that as well.
                 num_steps = max(num_steps, step+2)
             step += 1
 
+if inywfile is not None:
+    if not got_topt:
+        assume_skipped = 0
+        skip_steps = 0
+        num_steps = 0
+
+    with open(inywfile, "r") as f:
+        inyw = ReadWitness(f)
+
+        inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True)
+
+        smt_wires = defaultdict(list)
+        smt_mems = defaultdict(list)
+
+        for wire in inits + seqs:
+            smt_wires[wire["path"]].append(wire)
+
+        for mem in mems:
+            smt_mems[mem["path"]].append(mem)
+
+        addr_re = re.compile(r'\\\[[0-9]+\]$')
+        bits_re = re.compile(r'[01?]*$')
+
+        for t, step in inyw.steps():
+            present_signals, missing = step.present_signals(inyw.sigmap)
+            for sig in present_signals:
+                bits = step[sig]
+                if not bits_re.match(bits):
+                    raise ValueError("unsupported bit value in Yosys witness file")
+
+                sig_end = sig.offset + len(bits)
+                if sig.path in smt_wires:
+                    for wire in smt_wires[sig.path]:
+                        width, offset = wire["width"], wire["offset"]
+
+                        smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1
+
+                        offset = max(offset, 0)
+
+                        end = width + offset
+                        common_offset = max(sig.offset, offset)
+                        common_end = min(sig_end, end)
+                        if common_end <= common_offset:
+                            continue
+
+                        smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"])
+
+                        if not smt_bool:
+                            slice_high = common_end - offset - 1
+                            slice_low = common_offset - offset
+                            smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr)
+
+                        bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)]
+
+                        if bit_slice.count("?") == len(bit_slice):
+                            continue
+
+                        if smt_bool:
+                            assert width == 1
+                            smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false")
+                        else:
+                            if "?" in bit_slice:
+                                mask = bit_slice.replace("0", "1").replace("?", "0")
+                                bit_slice = bit_slice.replace("?", "0")
+                                smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
+
+                            smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
+
+                        constr_assumes[t].append((inywfile, smt_constr))
+
+                if sig.memory_path:
+                    if sig.memory_path in smt_mems:
+                        for mem in smt_mems[sig.memory_path]:
+                            width, size, bv = mem["width"], mem["size"], mem["statebv"]
+
+                            smt_expr = smt.net_expr(topmod, f"s{t}", mem["smtpath"])
+
+                            if bv:
+                                word_low = sig.memory_addr * width
+                                word_high = word_low + width - 1
+                                smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr)
+                            else:
+                                addr_width = (size - 1).bit_length()
+                                addr_bits = f"{sig.memory_addr:0{addr_width}b}"
+                                smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits)
+
+                            if len(bits) < width:
+                                slice_high = sig.offset + len(bits) - 1
+                                smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
+
+                            bit_slice = bits
+
+                            if "?" in bit_slice:
+                                mask = bit_slice.replace("0", "1").replace("?", "0")
+                                bit_slice = bit_slice.replace("?", "0")
+                                smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
+
+                            smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
+                            constr_assumes[t].append((inywfile, smt_constr))
+
+            if not got_topt:
+                if not check_witness:
+                    skip_steps = max(skip_steps, t)
+                num_steps = max(num_steps, t+1)
+
 if btorwitfile is not None:
     with open(btorwitfile, "r") as f:
         step = None
@@ -699,128 +826,137 @@ if btorwitfile is not None:
         skip_steps = step
         num_steps = step+1
 
-def write_vcd_trace(steps_start, steps_stop, index):
-    filename = vcdfile.replace("%", index)
-    print_msg("Writing trace to VCD file: %s" % (filename))
+def collect_mem_trace_data(steps_start, steps_stop, vcd=None):
+    mem_trace_data = dict()
 
-    with open(filename, "w") as vcd_file:
-        vcd = MkVcd(vcd_file)
-        path_list = list()
+    for mempath in sorted(smt.hiermems(topmod)):
+        abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
 
-        for netpath in sorted(smt.hiernets(topmod)):
-            hidden_net = False
-            for n in netpath:
-                if n.startswith("$"):
-                    hidden_net = True
-            if not hidden_net:
-                edge = smt.net_clock(topmod, netpath)
-                if edge is None:
-                    vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
-                else:
-                    vcd.add_clock([topmod] + netpath, edge)
-                path_list.append(netpath)
-
-        mem_trace_data = dict()
-        for mempath in sorted(smt.hiermems(topmod)):
-            abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
+        expr_id = list()
+        expr_list = list()
+        for i in range(steps_start, steps_stop):
+            for j in range(rports):
+                expr_id.append(('R', i-steps_start, j, 'A'))
+                expr_id.append(('R', i-steps_start, j, 'D'))
+                expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
+                expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
+            for j in range(wports):
+                expr_id.append(('W', i-steps_start, j, 'A'))
+                expr_id.append(('W', i-steps_start, j, 'D'))
+                expr_id.append(('W', i-steps_start, j, 'M'))
+                expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
+                expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
+                expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
+
+        rdata = list()
+        wdata = list()
+        addrs = set()
+
+        for eid, edat in zip(expr_id, smt.get_list(expr_list)):
+            t, i, j, f = eid
+
+            if t == 'R':
+                c = rdata
+            elif t == 'W':
+                c = wdata
+            else:
+                assert False
 
-            expr_id = list()
-            expr_list = list()
-            for i in range(steps_start, steps_stop):
-                for j in range(rports):
-                    expr_id.append(('R', i-steps_start, j, 'A'))
-                    expr_id.append(('R', i-steps_start, j, 'D'))
-                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
-                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
-                for j in range(wports):
-                    expr_id.append(('W', i-steps_start, j, 'A'))
-                    expr_id.append(('W', i-steps_start, j, 'D'))
-                    expr_id.append(('W', i-steps_start, j, 'M'))
-                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
-                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
-                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
-
-            rdata = list()
-            wdata = list()
-            addrs = set()
-
-            for eid, edat in zip(expr_id, smt.get_list(expr_list)):
-                t, i, j, f = eid
-
-                if t == 'R':
-                    c = rdata
-                elif t == 'W':
-                    c = wdata
-                else:
-                    assert False
+            while len(c) <= i:
+                c.append(list())
+            c = c[i]
 
-                while len(c) <= i:
-                    c.append(list())
-                c = c[i]
+            while len(c) <= j:
+                c.append(dict())
+            c = c[j]
 
-                while len(c) <= j:
-                    c.append(dict())
-                c = c[j]
+            c[f] = smt.bv2bin(edat)
 
-                c[f] = smt.bv2bin(edat)
+            if f == 'A':
+                addrs.add(c[f])
 
-                if f == 'A':
-                    addrs.add(c[f])
+        for addr in addrs:
+            tdata = list()
+            data = ["x"] * width
+            gotread = False
 
-            for addr in addrs:
-                tdata = list()
-                data = ["x"] * width
-                gotread = False
+            if len(wdata) == 0 and len(rdata) != 0:
+                wdata = [[]] * len(rdata)
 
-                if len(wdata) == 0 and len(rdata) != 0:
-                    wdata = [[]] * len(rdata)
+            assert len(rdata) == len(wdata)
 
-                assert len(rdata) == len(wdata)
+            for i in range(len(wdata)):
+                if not gotread:
+                    for j_data in rdata[i]:
+                        if j_data["A"] == addr:
+                            data = list(j_data["D"])
+                            gotread = True
+                            break
 
-                for i in range(len(wdata)):
-                    if not gotread:
-                        for j_data in rdata[i]:
-                            if j_data["A"] == addr:
-                                data = list(j_data["D"])
-                                gotread = True
-                                break
+                    if gotread:
+                        buf = data[:]
+                        for ii in reversed(range(len(tdata))):
+                            for k in range(width):
+                                if tdata[ii][k] == "x":
+                                    tdata[ii][k] = buf[k]
+                                else:
+                                    buf[k] = tdata[ii][k]
 
-                        if gotread:
-                            buf = data[:]
-                            for ii in reversed(range(len(tdata))):
-                                for k in range(width):
-                                    if tdata[ii][k] == "x":
-                                        tdata[ii][k] = buf[k]
-                                    else:
-                                        buf[k] = tdata[ii][k]
+                if not asyncwr:
+                    tdata.append(data[:])
 
-                    if not asyncwr:
-                        tdata.append(data[:])
+                for j_data in wdata[i]:
+                    if j_data["A"] != addr:
+                        continue
 
-                    for j_data in wdata[i]:
-                        if j_data["A"] != addr:
-                            continue
+                    D = j_data["D"]
+                    M = j_data["M"]
 
-                        D = j_data["D"]
-                        M = j_data["M"]
+                    for k in range(width):
+                        if M[k] == "1":
+                            data[k] = D[k]
 
-                        for k in range(width):
-                            if M[k] == "1":
-                                data[k] = D[k]
+                if asyncwr:
+                    tdata.append(data[:])
 
-                    if asyncwr:
-                        tdata.append(data[:])
+            assert len(tdata) == len(rdata)
 
-                assert len(tdata) == len(rdata)
+            int_addr = int(addr, 2)
 
-                netpath = mempath[:]
-                netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2))
+            netpath = mempath[:]
+            if vcd:
+                netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int_addr)
                 vcd.add_net([topmod] + netpath, width)
 
-                for i in range(steps_start, steps_stop):
-                    if i not in mem_trace_data:
-                        mem_trace_data[i] = list()
-                    mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start])))
+            for i in range(steps_start, steps_stop):
+                if i not in mem_trace_data:
+                    mem_trace_data[i] = list()
+                mem_trace_data[i].append((netpath, int_addr, "".join(tdata[i-steps_start])))
+
+    return mem_trace_data
+
+def write_vcd_trace(steps_start, steps_stop, index):
+    filename = vcdfile.replace("%", index)
+    print_msg("Writing trace to VCD file: %s" % (filename))
+
+    with open(filename, "w") as vcd_file:
+        vcd = MkVcd(vcd_file)
+        path_list = list()
+
+        for netpath in sorted(smt.hiernets(topmod)):
+            hidden_net = False
+            for n in netpath:
+                if n.startswith("$"):
+                    hidden_net = True
+            if not hidden_net:
+                edge = smt.net_clock(topmod, netpath)
+                if edge is None:
+                    vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
+                else:
+                    vcd.add_clock([topmod] + netpath, edge)
+                path_list.append(netpath)
+
+        mem_trace_data = collect_mem_trace_data(steps_start, steps_stop, vcd)
 
         for i in range(steps_start, steps_stop):
             vcd.set_time(i)
@@ -828,7 +964,7 @@ def write_vcd_trace(steps_start, steps_stop, index):
             for path, value in zip(path_list, value_list):
                 vcd.set_net([topmod] + path, value)
             if i in mem_trace_data:
-                for path, value in mem_trace_data[i]:
+                for path, addr, value in mem_trace_data[i]:
                     vcd.set_net([topmod] + path, value)
 
         vcd.set_time(steps_stop)
@@ -1072,8 +1208,72 @@ def write_constr_trace(steps_start, steps_stop, index):
             for name, val in zip(pi_names, pi_values):
                 print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 
+def write_yw_trace(steps_start, steps_stop, index, allregs=False):
+    filename = outywfile.replace("%", index)
+    print_msg("Writing trace to Yosys witness file: %s" % (filename))
+
+    mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
+
+    with open(filename, "w") as f:
+        inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs)
+
+        yw = WriteWitness(f, "smtbmc")
+
+        for clock in clocks:
+            yw.add_clock(clock["path"], clock["offset"], clock["type"])
+
+        for seq in seqs:
+            seq["sig"] = yw.add_sig(seq["path"], seq["offset"], seq["width"])
 
-def write_trace(steps_start, steps_stop, index):
+        for init in inits:
+            init["sig"] = yw.add_sig(init["path"], init["offset"], init["width"], True)
+
+        inits = seqs + inits
+
+        mem_dict = {tuple(mem["smtpath"]): mem for mem in mems}
+        mem_init_values = []
+
+        for path, addr, value in mem_trace_data.get(0, ()):
+            json_mem = mem_dict.get(tuple(path))
+            if not json_mem:
+                continue
+
+            bit_addr = addr * json_mem["width"]
+            uninit_chunks = [(chunk["width"] + chunk["offset"], chunk["offset"]) for chunk in json_mem["uninitialized"]]
+            first_chunk_nr = bisect.bisect_left(uninit_chunks, (bit_addr + 1,))
+
+            for uninit_end, uninit_offset in uninit_chunks[first_chunk_nr:]:
+                assert uninit_end > bit_addr
+                if uninit_offset > bit_addr + json_mem["width"]:
+                    break
+
+                word_path = (*json_mem["path"], f"\\[{addr}]")
+
+                overlap_start = max(uninit_offset - bit_addr, 0)
+                overlap_end = min(uninit_end - bit_addr, json_mem["width"])
+                overlap_bits = value[len(value)-overlap_end:len(value)-overlap_start]
+
+                sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True)
+                mem_init_values.append((sig, overlap_bits.replace("x", "?")))
+
+        for k in range(steps_start, steps_stop):
+            step_values = WitnessValues()
+
+            if k == steps_start:
+                for sig, value in mem_init_values:
+                    step_values[sig] = value
+                sigs = inits + seqs
+            else:
+                sigs = seqs
+
+            for sig in sigs:
+                step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"])))
+            yw.step(step_values)
+
+        yw.end_trace()
+
+
+def write_trace(steps_start, steps_stop, index, allregs=False):
     if vcdfile is not None:
         write_vcd_trace(steps_start, steps_stop, index)
 
@@ -1083,6 +1283,9 @@ def write_trace(steps_start, steps_stop, index):
     if outconstr is not None:
         write_constr_trace(steps_start, steps_stop, index)
 
+    if outywfile is not None:
+        write_yw_trace(steps_start, steps_stop, index, allregs)
+
 
 def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()):
     assert mod in smt.modinfo
@@ -1392,12 +1595,12 @@ if tempind:
                 print_msg("Temporal induction failed!")
                 print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
-                write_trace(step, num_steps+1, '%')
+                write_trace(step, num_steps+1, '%', allregs=True)
 
             elif dumpall:
                 print_anyconsts(num_steps)
                 print_failed_asserts(num_steps)
-                write_trace(step, num_steps+1, "%d" % step)
+                write_trace(step, num_steps+1, "%d" % step, allregs=True)
 
         else:
             print_msg("Temporal induction successful.")
@@ -1590,6 +1793,7 @@ else:  # not tempind, covermode
 
                         smt_assert("(not %s)" % active_assert_expr)
                     else:
+                        active_assert_expr = "true"
                         smt_assert("false")
 
 
@@ -1597,6 +1801,17 @@ else:  # not tempind, covermode
                         if retstatus != "FAILED":
                             print("%s BMC failed!" % smt.timestamp())
 
+                        if check_witness:
+                            print_msg("Checking witness constraints...")
+                            smt_pop()
+                            smt_push()
+                            smt_assert(active_assert_expr)
+                            if smt_check_sat() != "sat":
+                                retstatus = "PASSED"
+                                check_witness = False
+                                num_steps = -1
+                                break
+
                         if append_steps > 0:
                             for i in range(last_check_step+1, last_check_step+1+append_steps):
                                 print_msg("Appending additional step %d." % i)
@@ -1689,6 +1904,8 @@ else:  # not tempind, covermode
         print_anyconsts(0)
         write_trace(0, num_steps, '%')
 
+    if check_witness:
+        retstatus = "FAILED"
 
 smt.write("(exit)")
 smt.wait()
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 91efc13a3..de09c040e 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -16,7 +16,7 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import sys, re, os, signal
+import sys, re, os, signal, json
 import subprocess
 if os.name == "posix":
     import resource
@@ -108,6 +108,7 @@ class SmtModInfo:
         self.allconsts = dict()
         self.allseqs = dict()
         self.asize = dict()
+        self.witness = []
 
 
 class SmtIo:
@@ -337,7 +338,7 @@ class SmtIo:
 
     def p_thread_main(self):
         while True:
-            data = self.p.stdout.readline().decode("ascii")
+            data = self.p.stdout.readline().decode("utf-8")
             if data == "": break
             self.p_queue.put(data)
         self.p_queue.put("")
@@ -359,7 +360,7 @@ class SmtIo:
 
     def p_write(self, data, flush):
         assert self.p is not None
-        self.p.stdin.write(bytes(data, "ascii"))
+        self.p.stdin.write(bytes(data, "utf-8"))
         if flush: self.p.stdin.flush()
 
     def p_read(self):
@@ -587,6 +588,11 @@ class SmtIo:
             self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
             self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 
+        if fields[1] == "yosys-smt2-witness":
+            data = json.loads(stmt.split(None, 2)[2])
+            if data.get("type") in ["cell", "mem", "posedge", "negedge", "input", "reg", "init", "seq", "blackbox"]:
+                self.modinfo[self.curmod].witness.append(data)
+
     def hiernets(self, top, regs_only=False):
         def hiernets_worker(nets, mod, cursor):
             for netname in sorted(self.modinfo[mod].wsize.keys()):
@@ -658,6 +664,57 @@ class SmtIo:
         hiermems_worker(mems, top, [])
         return mems
 
+    def hierwitness(self, top, allregs=False, blackbox=True):
+        init_witnesses = []
+        seq_witnesses = []
+        clk_witnesses = []
+        mem_witnesses = []
+
+        def absolute(path, cursor, witness):
+            return {
+                **witness,
+                "path": path + tuple(witness["path"]),
+                "smtpath": cursor + [witness["smtname"]],
+            }
+
+        for witness in self.modinfo[top].witness:
+            if witness["type"] == "input":
+                seq_witnesses.append(absolute((), [], witness))
+            if witness["type"] in ("posedge", "negedge"):
+                clk_witnesses.append(absolute((), [], witness))
+
+        init_types = ["init"]
+        if allregs:
+            init_types.append("reg")
+
+        seq_types = ["seq"]
+        if blackbox:
+            seq_types.append("blackbox")
+
+        def worker(mod, path, cursor):
+            cell_paths = {}
+            for witness in self.modinfo[mod].witness:
+                if witness["type"] in init_types:
+                    init_witnesses.append(absolute(path, cursor, witness))
+                if witness["type"] in seq_types:
+                    seq_witnesses.append(absolute(path, cursor, witness))
+                if witness["type"] == "mem":
+                    if allregs and not witness["rom"]:
+                        width, size = witness["width"], witness["size"]
+                        witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}}
+                    if not witness["uninitialized"]:
+                        continue
+
+                    mem_witnesses.append(absolute(path, cursor, witness))
+                if witness["type"] == "cell":
+                    cell_paths[witness["smtname"]] = tuple(witness["path"])
+
+            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+                worker(celltype, path + cell_paths.get(cellname, ("?" + cellname,)), cursor + [cellname])
+
+        worker(top, (), [])
+        return init_witnesses, seq_witnesses, clk_witnesses, mem_witnesses
+
     def read(self):
         stmt = []
         count_brackets = 0
@@ -887,6 +944,8 @@ class SmtIo:
             assert mod in self.modinfo
             if path[0] == "":
                 return base
+            if isinstance(path[0], int):
+                return "(|%s#%d| %s)" % (mod, path[0], base)
             if path[0] in self.modinfo[mod].cells:
                 return "(|%s_h %s| %s)" % (mod, path[0], base)
             if path[0] in self.modinfo[mod].wsize:
@@ -909,6 +968,8 @@ class SmtIo:
             mod = self.modinfo[mod].cells[net_path[i]]
 
         assert mod in self.modinfo
+        if isinstance(net_path[-1], int):
+            return None
         assert net_path[-1] in self.modinfo[mod].wsize
         return self.modinfo[mod].wsize[net_path[-1]]
 
diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py
new file mode 100644
index 000000000..a1e65569d
--- /dev/null
+++ b/backends/smt2/witness.py
@@ -0,0 +1,254 @@
+#!/usr/bin/env python3
+#
+# 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.
+#
+
+import os, sys, itertools, re
+##yosys-sys-path##
+import json
+import click
+
+from ywio import ReadWitness, WriteWitness, WitnessSig, WitnessSigMap, WitnessValues, coalesce_signals
+
+@click.group()
+def cli():
+    pass
+
+
+@cli.command(help="""
+Display a Yosys witness trace in a human readable format.
+""")
+@click.argument("input", type=click.File("r"))
+def display(input):
+    click.echo(f"Reading Yosys witness trace {input.name!r}...")
+    inyw = ReadWitness(input)
+
+    def output():
+
+        yield click.style("*** RTLIL bit-order below may differ from source level declarations ***", fg="red")
+        if inyw.clocks:
+            yield click.style("=== Clock Signals ===", fg="blue")
+            for clock in inyw.clocks:
+                yield f"  {clock['edge']} {WitnessSig(clock['path'], clock['offset']).pretty()}"
+
+        for t, values in inyw.steps():
+            if t:
+                yield click.style(f"=== Step {t} ===", fg="blue")
+            else:
+                yield click.style("=== Initial State ===", fg="blue")
+
+            step_prefix = click.style(f"#{t}", fg="bright_black")
+
+            signals, missing = values.present_signals(inyw.sigmap)
+
+            assert not missing
+
+            for sig in signals:
+                display_bits = values[sig].replace("?", click.style("?", fg="bright_black"))
+                yield f"  {step_prefix} {sig.pretty()} = {display_bits}"
+    click.echo_via_pager([line + "\n" for line in output()])
+
+
+@cli.command(help="""
+Display statistics of a Yosys witness trace.
+""")
+@click.argument("input", type=click.File("r"))
+def stats(input):
+    click.echo(f"Reading Yosys witness trace {input.name!r}...")
+    inyw = ReadWitness(input)
+
+    total = 0
+
+    for t, values in inyw.steps():
+        click.echo(f"{t:5}: {len(values.values):8} bits")
+        total += len(values.values)
+
+    click.echo(f"total: {total:8} bits")
+
+
+@cli.command(help="""
+Transform a Yosys witness trace.
+
+Currently no transformations are implemented, so it is only useful for testing.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def yw2yw(input, output):
+    click.echo(f"Copying yosys witness trace from {input.name!r} to {output.name!r}...")
+    inyw = ReadWitness(input)
+    outyw = WriteWitness(output, "yosys-witness yw2yw")
+
+    for clock in inyw.clocks:
+        outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+    for sig in inyw.signals:
+        outyw.add_sig(sig.path, sig.offset, sig.width, sig.init_only)
+
+    for t, values in inyw.steps():
+        outyw.step(values)
+
+    outyw.end_trace()
+
+    click.echo(f"Copied {outyw.t + 1} time steps.")
+
+
+class AigerMap:
+    def __init__(self, mapfile):
+        data = json.load(mapfile)
+
+        self.latch_count = data["latch_count"]
+        self.input_count = data["input_count"]
+
+        self.clocks = data["clocks"]
+
+        self.sigmap = WitnessSigMap()
+        self.init_inputs = set(init["input"] for init in data["inits"])
+
+        for bit in data["inputs"] + data["seqs"] + data["inits"]:
+            self.sigmap.add_bit((tuple(bit["path"]), bit["offset"]), bit["input"])
+
+
+
+@cli.command(help="""
+Convert an AIGER witness trace into a Yosys witness trace.
+
+This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("mapfile", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def aiw2yw(input, mapfile, output):
+    input_name = input.name
+    click.echo(f"Converting AIGER witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
+    click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
+    aiger_map = AigerMap(mapfile)
+
+    header_lines = list(itertools.islice(input, 0, 2))
+
+    if len(header_lines) == 2 and header_lines[1][0] in ".bcjf":
+        status = header_lines[0].strip()
+        if status == "0":
+            raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is unsat")
+        elif status == "2":
+            raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is sat")
+        elif status != "1":
+            raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
+    else:
+        input = itertools.chain(header_lines, input)
+
+    ffline = next(input, None)
+    if ffline is None:
+        raise click.ClickException(f"{input_name}: unexpected end of file")
+    ffline = ffline.strip()
+    if not re.match(r'[01x]*$', ffline):
+        raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
+    if not re.match(r'[0]*$', ffline):
+        raise click.ClickException(f"{input_name}: non-default initial state not supported")
+
+    outyw = WriteWitness(output, 'yosys-witness aiw2yw')
+
+    for clock in aiger_map.clocks:
+        outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+    for (path, offset), id in aiger_map.sigmap.bit_to_id.items():
+        outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs)
+
+    missing = set()
+
+    while True:
+        inline = next(input, None)
+        if inline is None:
+            click.echo(f"Warning: {input_name}: file may be incomplete")
+            break
+        inline = inline.strip()
+        if inline in [".", "# DONE"]:
+            break
+        if inline.startswith("#"):
+            continue
+
+        if not re.match(r'[01x]*$', ffline):
+            raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
+
+        if len(inline) != aiger_map.input_count:
+            raise click.ClickException(
+                    f"{input_name}: {mapfile.name}: number of inputs does not match, "
+                    f"{len(inline)} in witness, {aiger_map.input_count} in map file")
+
+        values = WitnessValues()
+        for i, v in enumerate(inline):
+            if v == "x" or outyw.t > 0 and i in aiger_map.init_inputs:
+                continue
+
+            try:
+                bit = aiger_map.sigmap.id_to_bit[i]
+            except IndexError:
+                bit = None
+            if bit is None:
+                missing.insert(i)
+
+            values[bit] = v
+
+        outyw.step(values)
+
+    outyw.end_trace()
+
+    if missing:
+        click.echo("The following AIGER inputs belong to unknown signals:")
+        click.echo("  " + " ".join(str(id) for id in sorted(missing)))
+
+    click.echo(f"Converted {outyw.t} time steps.")
+
+@cli.command(help="""
+Convert a Yosys witness trace into an AIGER witness trace.
+
+This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("mapfile", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def yw2aiw(input, mapfile, output):
+    click.echo(f"Converting Yosys witness trace {input.name!r} to AIGER witness trace {output.name!r}...")
+    click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
+    aiger_map = AigerMap(mapfile)
+    inyw = ReadWitness(input)
+
+    print("1", file=output)
+    print("b0", file=output)
+    # TODO the b0 status isn't really accurate, but we don't have any better info here
+    print("0" * aiger_map.latch_count, file=output)
+
+    all_missing = set()
+
+    for t, step in inyw.steps():
+        bits, missing = step.pack_present(aiger_map.sigmap)
+        bits = bits[::-1].replace('?', 'x')
+        all_missing.update(missing)
+        bits += 'x' * (aiger_map.input_count - len(bits))
+        print(bits, file=output)
+
+    print(".", file=output)
+
+    if all_missing:
+        click.echo("The following signals are missing in the AIGER map file and will be dropped:")
+        for sig in coalesce_signals(WitnessSig(*bit) for bit in all_missing):
+            click.echo("  " + sig.pretty())
+
+
+    click.echo(f"Converted {len(inyw)} time steps.")
+
+if __name__ == "__main__":
+    cli()
diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py
new file mode 100644
index 000000000..8469b4162
--- /dev/null
+++ b/backends/smt2/ywio.py
@@ -0,0 +1,392 @@
+#
+# 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.
+#
+
+import json, re
+
+from functools import total_ordering
+
+
+class PrettyJson:
+    def __init__(self, f):
+        self.f = f
+        self.indent = 0
+        self.state = ["value"]
+
+    def line(self):
+        indent = len(self.state) - bool(self.state and self.state[-1] == "value")
+        print("\n", end=" " * (2 * indent), file=self.f)
+
+    def raw(self, str):
+        print(end=str, file=self.f)
+
+    def begin_object(self):
+        self.begin_value()
+        self.raw("{")
+        self.state.append("object_first")
+
+    def begin_array(self):
+        self.begin_value()
+        self.raw("[")
+        self.state.append("array_first")
+
+    def end_object(self):
+        state = self.state.pop()
+        if state == "object":
+            self.line()
+        else:
+            assert state == "object_first"
+        self.raw("}")
+        self.end_value()
+
+    def end_array(self):
+        state = self.state.pop()
+        if state == "array":
+            self.line()
+        else:
+            assert state == "array_first"
+        self.raw("]")
+        self.end_value()
+
+    def name(self, name):
+        if self.state[-1] == "object_first":
+            self.state[-1] = "object"
+        else:
+            self.raw(",")
+        self.line()
+        json.dump(str(name), self.f)
+        self.raw(": ")
+        self.state.append("value")
+
+    def begin_value(self):
+        if self.state[-1] == "array_first":
+            self.line()
+            self.state[-1] = "array"
+        elif self.state[-1] == "array":
+            self.raw(",")
+            self.line()
+        else:
+            assert self.state.pop() == "value"
+
+    def end_value(self):
+        if not self.state:
+            print(file=self.f, flush=True)
+
+    def value(self, value):
+        self.begin_value()
+        json.dump(value, self.f)
+        self.end_value()
+
+    def entry(self, name, value):
+        self.name(name)
+        self.value(value)
+
+    def object(self, entries=None):
+        if isinstance(entries, dict):
+            entries = dict.items()
+        self.begin_object()
+        for name, value in entries:
+            self.entry(name, value)
+        self.end_object()
+
+    def array(self, values=None):
+        self.begin_array()
+        for value in values:
+            self.value(value)
+        self.end_array()
+
+
+addr_re = re.compile(r'\\\[[0-9]+\]$')
+public_name_re = re.compile(r"\\([a-zA-Z_][a-zA-Z0-9_]*(\[[0-9]+\])?|\[[0-9]+\])$")
+
+def pretty_name(id):
+    if public_name_re.match(id):
+        return id.lstrip("\\")
+    else:
+        return id
+
+def pretty_path(path):
+    out = ""
+    for name in path:
+        name = pretty_name(name)
+        if name.startswith("["):
+            out += name
+            continue
+        if out:
+            out += "."
+        if name.startswith("\\") or name.startswith("$"):
+            out += name + " "
+        else:
+            out += name
+
+    return out
+
+@total_ordering
+class WitnessSig:
+    def __init__(self, path, offset, width=1, init_only=False):
+        path = tuple(path)
+        self.path, self.width, self.offset, self.init_only = path, width, offset, init_only
+
+        self.memory_path = None
+        self.memory_addr = None
+
+        sort_path = path
+        sort_id = -1
+        if path and addr_re.match(path[-1]):
+            self.memory_path = sort_path = path[:-1]
+            self.memory_addr = sort_id = int(path[-1][2:-1])
+
+        self.sort_key = (init_only, sort_path, sort_id, offset, width)
+
+    def bits(self):
+        return ((self.path, i) for i in range(self.offset, self.offset + self.width))
+
+    def rev_bits(self):
+        return ((self.path, i) for i in reversed(range(self.offset, self.offset + self.width)))
+
+    def pretty(self):
+        if self.width > 1:
+            last_offset = self.offset + self.width - 1
+            return f"{pretty_path(self.path)}[{last_offset}:{self.offset}]"
+        else:
+            return f"{pretty_path(self.path)}[{self.offset}]"
+
+    def __eq__(self):
+        return self.sort_key
+
+    def __hash__(self):
+        return hash(self.sort_key)
+
+    def __lt__(self, other):
+        return self.sort_key < other.sort_key
+
+
+def coalesce_signals(signals):
+    bits = {}
+    for sig in signals:
+        for bit in sig.bits():
+            if sig.init_only:
+                bits.setdefault(bit, False)
+            else:
+                bits[bit] = True
+
+    active = None
+
+    out = []
+
+    for bit, not_init in sorted(bits.items()):
+        if active:
+            if active[0] == bit[0] and active[2] == bit[1] and active[3] == not_init:
+                active[2] += 1
+            else:
+                out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3]))
+                active = None
+
+        if active is None:
+            active = [bit[0], bit[1], bit[1] + 1, not_init]
+
+    if active:
+        out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3]))
+
+    return sorted(out)
+
+
+class WitnessSigMap:
+    def __init__(self, signals=[]):
+        self.signals = []
+
+        self.id_to_bit = []
+        self.bit_to_id = {}
+        self.bit_to_sig = {}
+
+        for sig in signals:
+            self.add_signal(sig)
+
+    def add_signal(self, sig):
+        self.signals.append(sig)
+        for bit in sig.bits():
+            self.add_bit(bit)
+            self.bit_to_sig[bit] = sig
+
+    def add_bit(self, bit, id=None):
+        if id is None:
+            id = len(self.id_to_bit)
+            self.id_to_bit.append(bit)
+        else:
+            if len(self.id_to_bit) <= id:
+                self.id_to_bit += [None] * (id - len(self.id_to_bit) + 1)
+            self.id_to_bit[id] = bit
+        self.bit_to_id[bit] = id
+
+
+class WitnessValues:
+    def __init__(self):
+        self.values = {}
+
+    def __setitem__(self, key, value):
+        if isinstance(key, tuple) and len(key) == 2:
+            if value != "?":
+                assert isinstance(value, str)
+                assert len(value) == 1
+                self.values[key] = value
+        else:
+            assert isinstance(key, WitnessSig)
+            assert key.width == len(value)
+            if isinstance(value, str):
+                value = reversed(value)
+            for bit, bit_value in zip(key.bits(), value):
+                if bit_value != "?":
+                    self.values[bit] = bit_value
+
+    def __getitem__(self, key):
+        if isinstance(key, tuple) and len(key) == 2:
+            return self.values.get(key, "?")
+        else:
+            assert isinstance(key, WitnessSig)
+            return "".join([self.values.get(bit, "?") for bit in key.rev_bits()])
+
+    def pack_present(self, sigmap):
+        missing = []
+
+        max_id = max((sigmap.bit_to_id.get(bit, -1) for bit in self.values), default=-1)
+
+        vector = ["?"] * (max_id + 1)
+        for bit, bit_value in self.values.items():
+            id = sigmap.bit_to_id.get(bit, - 1)
+            if id < 0:
+                missing.append(bit)
+            else:
+                vector[max_id - sigmap.bit_to_id[bit]] = bit_value
+
+        return "".join(vector), missing
+
+    def pack(self, sigmap):
+        packed, missing = self.pack_present(sigmap)
+        if missing:
+            raise RuntimeError(f"Cannot pack bits {missing!r}")
+        return packed
+
+    def unpack(self, sigmap, bits):
+        for i, bit_value in enumerate(reversed(bits)):
+            if bit_value != "?":
+                self.values[sigmap.id_to_bit[i]] = bit_value
+
+    def present_signals(self, sigmap):
+        signals = set(sigmap.bit_to_sig.get(bit) for bit in self.values)
+        missing_signals = None in signals
+        if missing_signals:
+            signals.discard(None)
+
+        return sorted(signals), missing_signals
+
+
+class WriteWitness:
+    def __init__(self, f, generator):
+        self.out = PrettyJson(f)
+        self.t = 0
+        self.header_written = False
+        self.clocks = []
+        self.signals = []
+
+        self.out.begin_object()
+        self.out.entry("format", "Yosys Witness Trace")
+        self.out.entry("generator", generator)
+
+    def add_clock(self, path, offset, edge):
+        assert not self.header_written
+        self.clocks.append({
+            "path": path,
+            "edge": edge,
+            "offset": offset,
+        })
+
+    def add_sig(self, path, offset, width=1, init_only=False):
+        assert not self.header_written
+        sig = WitnessSig(path, offset, width, init_only)
+        self.signals.append(sig)
+        return sig
+
+    def write_header(self):
+        assert not self.header_written
+        self.header_written = True
+        self.out.name("clocks")
+        self.out.array(self.clocks)
+
+        self.signals = coalesce_signals(self.signals)
+        self.sigmap = WitnessSigMap(self.signals)
+
+        self.out.name("signals")
+        self.out.array({
+            "path": sig.path,
+            "width": sig.width,
+            "offset": sig.offset,
+            "init_only": sig.init_only,
+        } for sig in self.signals)
+
+        self.out.name("steps")
+        self.out.begin_array()
+
+    def step(self, values):
+        if not self.header_written:
+            self.write_header()
+
+        self.out.value({"bits": values.pack(self.sigmap)})
+
+        self.t += 1
+
+    def end_trace(self):
+        if not self.header_written:
+            self.write_header()
+        self.out.end_array()
+        self.out.end_object()
+
+
+class ReadWitness:
+    def __init__(self, f):
+        data = json.load(f)
+        if not isinstance(data, dict):
+            data = {}
+
+        data_format = data.get("format", "Unknown Format")
+
+        if data_format != "Yosys Witness Trace":
+            raise ValueError(f"unsupported format {data_format!r}")
+
+        self.clocks = data["clocks"]
+        for clock in self.clocks:
+            clock["path"] = tuple(clock["path"])
+
+        self.signals = [
+            WitnessSig(sig["path"], sig["offset"], sig["width"], sig["init_only"])
+            for sig in data["signals"]
+        ]
+
+        self.sigmap = WitnessSigMap(self.signals)
+
+        self.bits = [step["bits"] for step in data["steps"]]
+
+    def step(self, t):
+        values = WitnessValues()
+        values.unpack(self.sigmap, self.bits[t])
+        return values
+
+    def steps(self):
+        for i in range(len(self.bits)):
+            yield i, self.step(i)
+
+    def __len__(self):
+        return len(self.bits)