From 636b9f27052ef67192ee55a862c31e57a1ccad79 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 3 Jan 2023 14:45:41 +0100 Subject: [PATCH] Support for BTOR witness to Yosys witness conversion --- backends/btor/btor.cc | 159 +++++++++++++++++++++++++++++++++++++-- backends/smt2/witness.py | 131 ++++++++++++++++++++++++++++++++ backends/smt2/ywio.py | 5 +- kernel/json.cc | 32 +++++--- kernel/json.h | 5 +- 5 files changed, 312 insertions(+), 20 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 8368ab82d..4315f6f67 100644 --- a/backends/btor/btor.cc +++ b/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 USING_YOSYS_NAMESPACE @@ -83,6 +84,20 @@ struct BtorWorker vector info_lines; dict 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_inputs; + vector ywmap_states; + dict 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 static std::vector witness_path(T *obj) { + std::vector 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 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 \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 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"); } diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index a1e65569d..14cf61fd7 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -110,6 +110,10 @@ class AigerMap: def __init__(self, mapfile): data = json.load(mapfile) + version = data.get("version") if isinstance(data, dict) else {} + if version != "Yosys Witness Aiger map": + raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}") + self.latch_count = data["latch_count"] self.input_count = data["input_count"] @@ -250,5 +254,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() diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py index 8469b4162..39cfac41e 100644 --- a/backends/smt2/ywio.py +++ b/backends/smt2/ywio.py @@ -175,8 +175,9 @@ class WitnessSig: return self.sort_key < other.sort_key -def coalesce_signals(signals): - bits = {} +def coalesce_signals(signals, bits=None): + if bits is None: + bits = {} for sig in signals: for bit in sig.bits(): if sig.init_only: diff --git a/kernel/json.cc b/kernel/json.cc index 59f782e5e..738746267 100644 --- a/kernel/json.cc +++ b/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) - line(); - else - log_assert(state.back() == ARRAY_FIRST); + Scope top_scope = state.back(); 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) diff --git a/kernel/json.h b/kernel/json.h index ae86b3aa6..c9aa0e045 100644 --- a/kernel/json.h +++ b/kernel/json.h @@ -47,6 +47,7 @@ class PrettyJson std::string newline_indent = "\n"; std::vector> targets; std::vector 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();