diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/aiger/aiger.cc | 180 | ||||
| -rw-r--r-- | backends/btor/btor.cc | 12 | ||||
| -rw-r--r-- | backends/smt2/Makefile.inc | 16 | ||||
| -rw-r--r-- | backends/smt2/smt2.cc | 152 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 439 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 63 | ||||
| -rw-r--r-- | backends/smt2/witness.py | 254 | ||||
| -rw-r--r-- | backends/smt2/ywio.py | 392 |
8 files changed, 1381 insertions, 127 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 547d131ee..2ea999dc0 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::CLK).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 831a3ada2..06de71018 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -612,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)); @@ -1112,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/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 f6c3560c1..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); @@ -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; } @@ -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 3ba43825c..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: @@ -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) |