From 4adef63cd484d81da08ae6b5fe49b1d5d4d0b369 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 17 Jun 2022 17:23:13 +0200 Subject: smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction This avoids provability regressions now that we infer more ROMs. This fixes #3378 --- backends/smt2/smt2.cc | 1 + 1 file changed, 1 insertion(+) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 7481e0510..6e70f9043 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1609,6 +1609,7 @@ struct Smt2Backend : public Backend { log_header(design, "Executing SMT2 backend.\n"); log_push(); + Pass::call(design, "memory_map -rom-only"); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); log_pop(); -- cgit v1.2.3 From d78d807a7fa1747b40da8bac9e278183cf86d3cc Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 27 Jun 2022 15:47:55 +0200 Subject: memory_map: -keepdc option for formal Use it when invoking memory_map -rom-only from write_{smt2,btor}. --- backends/smt2/smt2.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 6e70f9043..c75d4a98a 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1609,7 +1609,7 @@ struct Smt2Backend : public Backend { log_header(design, "Executing SMT2 backend.\n"); log_push(); - Pass::call(design, "memory_map -rom-only"); + Pass::call(design, "memory_map -rom-only -keepdc"); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); log_pop(); -- cgit v1.2.3 From 930bcf0e75f3b8d6c5afbdffda5ef7fd7eddc964 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 29 Jun 2022 18:28:34 +0200 Subject: smt2, btor: Revert calling memory_map -rom-only This approach had major issues with ROMs whose initialization was not fully defined. If required, memory_map -rom-only -keepdc should be called early in a formal flow instead. (This does require a careful choice of optimization passes though. Sby's scripts will be updated accordingly.) --- backends/smt2/smt2.cc | 1 - 1 file changed, 1 deletion(-) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index c75d4a98a..7481e0510 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -1609,7 +1609,6 @@ struct Smt2Backend : public Backend { log_header(design, "Executing SMT2 backend.\n"); log_push(); - Pass::call(design, "memory_map -rom-only -keepdc"); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); log_pop(); -- cgit v1.2.3 From 6af5e74f95abdead1c4c900e0c1951b71dcf80c8 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 20:16:41 +0200 Subject: smt2: Fix $shift/$shiftx with negative shift ammounts Fixes #3431, fixes #3344 --- backends/smt2/smt2.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 7481e0510..f6c3560c1 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -449,7 +449,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 +462,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; @@ -619,8 +619,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'); } -- cgit v1.2.3 From a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:49:51 +0200 Subject: formalff: Set new replaced_by_gclk attribute on removed dff's clks This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute. --- backends/smt2/smt2.cc | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index f6c3560c1..126ee1175 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -239,6 +239,17 @@ struct Smt2Worker clock_negedge.erase(bit); } + 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) -- cgit v1.2.3 From 021c3c8da52ebaf6088ea740fdc12b496bfc338a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:53:47 +0200 Subject: smt2: Support $anyinit cells --- backends/smt2/smt2.cc | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 126ee1175..e6729aade 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -594,25 +594,26 @@ struct Smt2Worker 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))); + 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; } @@ -931,7 +932,7 @@ struct Smt2Worker pool 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); @@ -1147,7 +1148,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"); -- cgit v1.2.3 From f041e36c6e142878c5bca4da5b459177c4f75e07 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 16:49:36 +0200 Subject: smtbmc: Add native json based witness format + smt2 backend support This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication. --- backends/smt2/smt2.cc | 120 ++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 117 insertions(+), 3 deletions(-) (limited to 'backends/smt2/smt2.cc') diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e6729aade..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 USING_YOSYS_NAMESPACE @@ -588,6 +589,9 @@ 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); @@ -610,6 +614,12 @@ struct Smt2Worker decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter)); log("Wire %s is minimized\n", cell->getPort(QY).as_wire()->name.str().c_str()); } + + 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)); @@ -760,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) { @@ -852,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()) @@ -950,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 comments; if (wire->port_input) @@ -968,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 = @@ -980,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) { @@ -1447,6 +1477,90 @@ struct Smt2Worker f << "true)"; f << stringf(" ; end of module %s\n", get_id(module)); } + + 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; + } + + std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire) + { + std::vector 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 { -- cgit v1.2.3