Support for BTOR witness to Yosys witness conversion

backends/btor/btor.cc

@@ -28,6 +28,7 @@
 #include "kernel/celltypes.h"
 #include "kernel/log.h"
 #include "kernel/mem.h"
+#include "kernel/json.h"
 #include <string>
 
 USING_YOSYS_NAMESPACE
@@ -83,6 +84,20 @@ 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_clocks;
+
+	PrettyJson ywmap_json;
+
 	void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3))
 	{
 		va_list ap;
@@ -126,6 +141,62 @@ struct BtorWorker
 		return " " + infostr;
 	}
 
+	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 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 +688,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 +700,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_clocks[sig_c] |= negedge ? 2 : 1;
 			}
 
 			IdString symbol;
@@ -662,6 +737,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 +760,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 +784,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 +849,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 +876,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 +1000,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 +1081,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 +1164,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;
@@ -1111,6 +1203,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 +1215,16 @@ struct BtorWorker
 						info_clocks[nid] |= 2;
 				}
 			}
+
+			if (ywmap_json.active()) {
+				auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+				if (gclk_attr != wire->attributes.end()) {
+					if (gclk_attr->second == State::S1)
+						ywmap_clocks[sig] |= 1;
+					else if (gclk_attr->second == State::S0)
+						ywmap_clocks[sig] |= 2;
+				}
+			}
 		}
 
 		btorf_pop("inputs");
@@ -1378,6 +1481,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_clocks) {
+				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 +1545,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 +1586,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 +1602,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");
 	}

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,132 @@ 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()
+            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])]
+
+            if btor_sig is None:
+                continue
+
+            if isinstance(btor_sig, dict):
+                addr = tokens[1]
+                if not addr.startswith('[') or not addr.endswith(']'):
+                    raise click.ClickException(f"{input_name}: expected address in BTOR witness file")
+                addr = int(addr[1:-1], 2)
+
+                if addr < 0 or addr >= btor_sig["size"]:
+                    raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file")
+
+                btor_sig = [{
+                    "path": (*btor_sig["path"], f"\\[{addr}]"),
+                    "width": btor_sig["width"],
+                    "offset": 0,
+                }]
+
+                signal_value = iter(reversed(tokens[2]))
+            else:
+                signal_value = iter(reversed(tokens[1]))
+
+            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(signal_value)
+
+            if next(signal_value, 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()

backends/smt2/ywio.py

@@ -175,8 +175,9 @@ class WitnessSig:
         return self.sort_key < other.sort_key
 
 
-def coalesce_signals(signals):
+def coalesce_signals(signals, bits=None):
-    bits = {}
+    if bits is None:
+        bits = {}
     for sig in signals:
         for bit in sig.bits():
             if sig.init_only:

kernel/json.cc

@@ -57,8 +57,13 @@ bool PrettyJson::write_to_file(const std::string &path)
     return true;
 }
 
-void PrettyJson::line()
+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());
@@ -95,7 +100,7 @@ void PrettyJson::end_object()
     Scope top_scope = state.back();
     state.pop_back();
     if (top_scope == OBJECT)
-        line();
+        line(false);
     else
         log_assert(top_scope == OBJECT_FIRST);
     raw("}");
@@ -104,22 +109,25 @@ void PrettyJson::end_object()
 
 void PrettyJson::end_array()
 {
-    if (state.back() == ARRAY)
+    Scope top_scope = state.back();
-        line();
-    else
-        log_assert(state.back() == ARRAY_FIRST);
     state.pop_back();
-    raw("}");
+    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)
+    if (state.back() == OBJECT_FIRST) {
         state.back() = OBJECT;
-    else
+        line(false);
+    } else {
         raw(",");
-    line();
+        line();
+    }
     raw(Json(name).dump().c_str());
     raw(": ");
     state.push_back(VALUE);
@@ -128,7 +136,7 @@ void PrettyJson::name(const char *name)
 void PrettyJson::begin_value()
 {
     if (state.back() == ARRAY_FIRST) {
-        line();
+        line(false);
         state.back() = ARRAY;
     } else if (state.back() == ARRAY) {
         raw(",");
@@ -145,6 +153,8 @@ void PrettyJson::end_value()
         raw("\n");
         flush();
     }
+    if (GetSize(state) < compact_depth)
+        compact_depth = INT_MAX;
 }
 
 void PrettyJson::value_json(const Json &value)

kernel/json.h

@@ -47,6 +47,7 @@ class PrettyJson
     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();
@@ -55,7 +56,9 @@ public:
 
     bool active() { return !targets.empty(); }
 
-    void line();
+    void compact() { compact_depth = GetSize(state); }
+
+    void line(bool space_if_inline = true);
     void raw(const char *raw_json);
     void flush();
     void begin_object();