From 62afe6177995b9d2c2053903f8620271b95034f0 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 14 Dec 2022 18:31:22 +0100 Subject: [PATCH 01/14] smt2: Directly implement bwmux instead of using bwmuxmap --- backends/smt2/smt2.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index fe50ca7f6..8a683a394 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -458,7 +458,7 @@ struct Smt2Worker { RTLIL::SigSpec sig_a, sig_b; RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - bool is_signed = cell->getParam(ID::A_SIGNED).as_bool(); + bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool(); int width = GetSize(sig_y); if (type == 's' || type == 'S' || type == 'd' || type == 'b') { @@ -483,6 +483,7 @@ struct Smt2Worker if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B)); + else if (ch == 'S') processed_expr += get_bv(cell->getPort(ID::S)); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; @@ -639,6 +640,8 @@ struct Smt2Worker if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)"); if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)"); + if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U'); + if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's'); if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's'); if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's'); @@ -1744,7 +1747,6 @@ struct Smt2Backend : public Backend { log_push(); Pass::call(design, "bmuxmap"); Pass::call(design, "demuxmap"); - Pass::call(design, "bwmuxmap"); log_pop(); size_t argidx; From 673ad561b8cf75abdafd9afb3d44edf0edf1f1e1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:22:10 +0100 Subject: [PATCH 02/14] smt2: Treat bweqx as xnor Without x-bits they are equivalent --- backends/smt2/smt2.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 8a683a394..3b3585b59 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -640,6 +640,7 @@ struct Smt2Worker if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)"); if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)"); + if (cell->type == ID($bweqx)) return export_bvop(cell, "(bvxnor A B)", 'U'); if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U'); if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's'); From 5042600c0d3adeae9ad7e936e92d4bf7ccff3e53 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:24:10 +0100 Subject: [PATCH 03/14] xprop, setundef: Mark xprop decoding bwmuxes, exclude them from setundef This adds the xprop_decoder attribute to bwmuxes that drive the original unencoded signals. Setundef is changed to ignore the x inputs of these bwmuxes, so that they survive the prep script of SBY's formal flow. This is required to make simulation (via sim) using the prep model show the decoded x signals instead of 0/1 values made up by the solver. --- kernel/constids.inc | 1 + passes/cmds/setundef.cc | 10 +++++++++- passes/cmds/xprop.cc | 3 ++- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/kernel/constids.inc b/kernel/constids.inc index 239381f85..39211d0c7 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -259,5 +259,6 @@ X(WR_PORTS) X(WR_PRIORITY_MASK) X(WR_WIDE_CONTINUATION) X(X) +X(xprop_decoder) X(Y) X(Y_WIDTH) diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc index 590a7eb1d..7293002f3 100644 --- a/passes/cmds/setundef.cc +++ b/passes/cmds/setundef.cc @@ -502,7 +502,15 @@ struct SetundefPass : public Pass { } } - module->rewrite_sigspecs(worker); + for (auto &it : module->cells_) + if (!it.second->get_bool_attribute(ID::xprop_decoder)) + it.second->rewrite_sigspecs(worker); + for (auto &it : module->processes) + it.second->rewrite_sigspecs(worker); + for (auto &it : module->connections_) { + worker(it.first); + worker(it.second); + } if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST) { diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc index 5dee72e1b..5e78ff9fc 100644 --- a/passes/cmds/xprop.cc +++ b/passes/cmds/xprop.cc @@ -252,7 +252,8 @@ struct XpropWorker } if (!driven_orig.empty()) { - module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig); + auto decoder = module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig); + decoder->set_bool_attribute(ID::xprop_decoder); } if (!driven_never_x.first.empty()) { module->connect(driven_never_x); From 44b26d5c6d69999f167d219ef7e9319e48fbc3e9 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:33:20 +0100 Subject: [PATCH 04/14] sim: Emit used memory addresses as signals to output traces This matches the behavior of smtbmc. This also updates the sim internal memory API to allow masked writes where State::Sa bits (internal don't care - not a valid value for a signal) leave the memory content unchanged. --- passes/sat/sim.cc | 139 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 122 insertions(+), 17 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 0084a1f28..754fbdf95 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -93,6 +93,7 @@ struct SimShared bool ignore_x = false; bool date = false; bool multiclock = false; + int next_output_id = 0; }; void zinit(State &v) @@ -157,6 +158,7 @@ struct SimInstance std::vector memories; dict> signal_database; + dict>> trace_mem_database; dict fst_handles; dict fst_inputs; dict> fst_memories; @@ -325,7 +327,7 @@ struct SimInstance log_assert(GetSize(sig) <= GetSize(value)); for (int i = 0; i < GetSize(sig); i++) - if (state_nets.at(sig[i]) != value[i]) { + if (value[i] != State::Sa && state_nets.at(sig[i]) != value[i]) { state_nets.at(sig[i]) = value[i]; dirty_bits.insert(sig[i]); did_something = true; @@ -337,13 +339,24 @@ struct SimInstance } void set_memory_state(IdString memid, Const addr, Const data) + { + set_memory_state(memid, addr.as_int(), data); + } + + void set_memory_state(IdString memid, int addr, Const data) { auto &state = mem_database[memid]; - int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width; + bool dirty = false; + + int offset = (addr - state.mem->start_offset) * state.mem->width; for (int i = 0; i < GetSize(data); i++) - if (0 <= i+offset && i+offset < state.mem->size * state.mem->width) - state.data.bits[i+offset] = data.bits[i]; + if (0 <= i+offset && i+offset < state.mem->size * state.mem->width && data.bits[i] != State::Sa) + if (state.data.bits[i+offset] != data.bits[i]) + dirty = true, state.data.bits[i+offset] = data.bits[i]; + + if (dirty) + dirty_memories.insert(memid); } void set_memory_state_bit(IdString memid, int offset, State data) @@ -351,7 +364,10 @@ struct SimInstance auto &state = mem_database[memid]; if (offset >= state.mem->size * state.mem->width) log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid)); - state.data.bits[offset] = data; + if (state.data.bits[offset] != data) { + state.data.bits[offset] = data; + dirty_memories.insert(memid); + } } void update_cell(Cell *cell) @@ -447,9 +463,14 @@ struct SimInstance log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid)); if (addr.is_fully_def()) { - int index = addr.as_int() - mem.start_offset; + int addr_int = addr.as_int(); + int index = addr_int - mem.start_offset; if (index >= 0 && index < mem.size) data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2); + + for (int offset = 0; offset < 1 << port.wide_log2; offset++) { + register_memory_addr(id, addr_int + offset); + } } set_state(port.data, data); @@ -604,7 +625,8 @@ struct SimInstance if (addr.is_fully_def()) { - int index = addr.as_int() - mem.start_offset; + int addr_int = addr.as_int(); + int index = addr_int - mem.start_offset; if (index >= 0 && index < mem.size) for (int i = 0; i < (mem.width << port.wide_log2); i++) if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) { @@ -612,6 +634,9 @@ struct SimInstance dirty_memories.insert(mem.memid); did_something = true; } + + for (int i = 0; i < 1 << port.wide_log2; i++) + register_memory_addr(it.first, addr_int + i); } } } @@ -741,7 +766,7 @@ struct SimInstance child.second->register_signals(id); } - void write_output_header(std::function enter_scope, std::function exit_scope, std::function register_signal) + void write_output_header(std::function enter_scope, std::function exit_scope, std::function register_signal) { int exit_scopes = 1; if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) { @@ -774,11 +799,45 @@ struct SimInstance hdlname.pop_back(); for (auto name : hdlname) enter_scope("\\" + name); - register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0); + register_signal(signal_name.c_str(), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0); for (auto name : hdlname) exit_scope(); } else - register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0); + register_signal(log_id(signal.first->name), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0); + } + + for (auto &trace_mem : trace_mem_database) + { + auto memid = trace_mem.first; + auto &mdb = mem_database.at(memid); + Cell *cell = mdb.mem->cell; + + std::vector hdlname; + std::string signal_name; + bool has_hdlname = shared->hdlname && cell != nullptr && cell->name.isPublic() && cell->has_attribute(ID::hdlname); + + if (has_hdlname) { + hdlname = cell->get_hdlname_attribute(); + log_assert(!hdlname.empty()); + signal_name = std::move(hdlname.back()); + hdlname.pop_back(); + for (auto name : hdlname) + enter_scope("\\" + name); + } else { + signal_name = log_id(memid); + } + + for (auto &trace_index : trace_mem.second) { + int output_id = trace_index.second.first; + int index = trace_index.first; + register_signal( + stringf("%s[%d]", signal_name.c_str(), (index + mdb.mem->start_offset)).c_str(), + mdb.mem->width, nullptr, output_id, true); + } + + if (has_hdlname) + for (auto name : hdlname) + exit_scope(); } for (auto child : children) @@ -788,6 +847,26 @@ struct SimInstance exit_scope(); } + void register_memory_addr(IdString memid, int addr) + { + auto &mdb = mem_database.at(memid); + auto &mem = *mdb.mem; + int index = addr - mem.start_offset; + if (index < 0 || index >= mem.size) + return; + auto it = trace_mem_database.find(memid); + if (it != trace_mem_database.end() && it->second.count(index)) + return; + int output_id = shared->next_output_id++; + Const data; + if (!shared->output_data.empty()) { + data = mem.get_init_data().extract(index * mem.width, mem.width); + shared->output_data.front().second.emplace(output_id, data); + } + trace_mem_database[memid].emplace(index, make_pair(output_id, data)); + + } + void register_output_step_values(std::map *data) { for (auto &it : signal_database) @@ -803,6 +882,26 @@ struct SimInstance data->emplace(id, value); } + for (auto &trace_mem : trace_mem_database) + { + auto memid = trace_mem.first; + auto &mdb = mem_database.at(memid); + auto &mem = *mdb.mem; + for (auto &trace_index : trace_mem.second) + { + int output_id = trace_index.second.first; + int index = trace_index.first; + + auto value = mdb.data.extract(index * mem.width, mem.width); + + if (trace_index.second.second == value) + continue; + + trace_index.second.second = value; + data->emplace(output_id, value); + } + } + for (auto child : children) child.second->register_output_step_values(data); } @@ -956,8 +1055,8 @@ struct SimWorker : SimShared void register_signals() { - int id = 1; - top->register_signals(id); + next_output_id = 1; + top->register_signals(top->shared->next_output_id); } void register_output_step(int t) @@ -1734,9 +1833,15 @@ struct VCDWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); }, [this]() { vcdfile << stringf("$upscope $end\n");}, - [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { + [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) { if (use_signal.at(id)) { - vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name); + // Works around gtkwave trying to parse everything past the last [ in a signal + // name. While the emitted range doesn't necessarily match the wire's range, + // this is consistent with the range gtkwave makes up if it doesn't find a + // range + std::string range = strchr(name, '[') ? stringf("[%d:0]", size - 1) : std::string(); + vcdfile << stringf("$var %s %d n%d %s%s%s $end\n", is_reg ? "reg" : "wire", size, id, name[0] == '$' ? "\\" : "", name, range.c_str()); + } } ); @@ -1796,9 +1901,9 @@ struct FSTWriter : public OutputWriter worker->top->write_output_header( [this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); }, [this]() { fstWriterSetUpscope(fstfile); }, - [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) { + [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) { if (!use_signal.at(id)) return; - fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire), + fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, size, name, 0); mapping.emplace(id, fst_id); } @@ -1881,7 +1986,7 @@ struct AIWWriter : public OutputWriter worker->top->write_output_header( [](IdString) {}, []() {}, - [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; } + [this](const char */*name*/, int /*size*/, Wire *wire, int id, bool) { if (wire != nullptr) mapping[wire] = id; } ); std::map current; From 9c6198a8272de1558d9f613d52a23c043e1c928a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:39:49 +0100 Subject: [PATCH 05/14] sim: Internal API to set $initstate This is not yet added to any of the simulation drivers. --- passes/sat/sim.cc | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 754fbdf95..86736eeb4 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -153,6 +153,7 @@ struct SimInstance dict ff_database; dict mem_database; pool formal_database; + pool initstate_database; dict mem_cells; std::vector memories; @@ -256,6 +257,8 @@ struct SimInstance if (cell->type.in(ID($assert), ID($cover), ID($assume))) { formal_database.insert(cell); } + if (cell->type == ID($initstate)) + initstate_database.insert(cell); } if (shared->zinit) @@ -708,6 +711,14 @@ struct SimInstance it.second->update_ph3(); } + void set_initstate_outputs(State state) + { + for (auto cell : initstate_database) + set_state(cell->getPort(ID::Y), state); + for (auto child : children) + child.second->set_initstate_outputs(state); + } + void writeback(pool &wbmods) { if (!ff_database.empty() || !mem_database.empty()) { From f6458bab702e08ade0c15d7f7d8580cb5463d685 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:40:58 +0100 Subject: [PATCH 06/14] sim: Only check formal cells during gclk simulation updates This is required for compatibility with non-multiclock formal semantics. --- passes/sat/sim.cc | 35 +++++++++++++++++++---------------- 1 file changed, 19 insertions(+), 16 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 86736eeb4..344ebb681 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -653,7 +653,7 @@ struct SimInstance return did_something; } - void update_ph3() + void update_ph3(bool check_assertions) { for (auto &it : ff_database) { @@ -688,27 +688,30 @@ struct SimInstance } } - for (auto cell : formal_database) + if (check_assertions) { - string label = log_id(cell); - if (cell->attributes.count(ID::src)) - label = cell->attributes.at(ID::src).decode_string(); + for (auto cell : formal_database) + { + string label = log_id(cell); + if (cell->attributes.count(ID::src)) + label = cell->attributes.at(ID::src).decode_string(); - State a = get_state(cell->getPort(ID::A))[0]; - State en = get_state(cell->getPort(ID::EN))[0]; + State a = get_state(cell->getPort(ID::A))[0]; + State en = get_state(cell->getPort(ID::EN))[0]; - if (cell->type == ID($cover) && en == State::S1 && a != State::S1) - log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($cover) && en == State::S1 && a != State::S1) + log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assume) && en == State::S1 && a != State::S1) - log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assume) && en == State::S1 && a != State::S1) + log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assert) && en == State::S1 && a != State::S1) - log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assert) && en == State::S1 && a != State::S1) + log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + } } for (auto it : children) - it.second->update_ph3(); + it.second->update_ph3(check_assertions); } void set_initstate_outputs(State state) @@ -1116,7 +1119,7 @@ struct SimWorker : SimShared if (debug) log("\n-- ph3 --\n"); - top->update_ph3(); + top->update_ph3(gclk); } void initialize_stable_past() @@ -1126,7 +1129,7 @@ struct SimWorker : SimShared top->update_ph1(); if (debug) log("\n-- ph3 (initialize) --\n"); - top->update_ph3(); + top->update_ph3(false); } void set_inports(pool ports, State value) From 1494cfff001bd23ee1bcd5dbfe1ee04dded25ac4 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:42:34 +0100 Subject: [PATCH 07/14] New kernel/yw.{h,cc} to support reading Yosys witness files This contains parsing code as well as generic routines to associate the hierarchical signals paths within a Yosys witness file to a loaded RTLIL design, including support for memories. --- Makefile | 2 +- kernel/yw.cc | 209 +++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/yw.h | 170 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 380 insertions(+), 1 deletion(-) create mode 100644 kernel/yw.cc create mode 100644 kernel/yw.h diff --git a/Makefile b/Makefile index e8af0e77d..7aafe847d 100644 --- a/Makefile +++ b/Makefile @@ -653,7 +653,7 @@ ifneq ($(ABCEXTERNAL),) kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' endif endif -OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o +OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o ifeq ($(ENABLE_ZLIB),1) OBJS += kernel/fstdata.o endif diff --git a/kernel/yw.cc b/kernel/yw.cc new file mode 100644 index 000000000..4a6e37a13 --- /dev/null +++ b/kernel/yw.cc @@ -0,0 +1,209 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder + * + * 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. + * + */ + +#include "kernel/yw.h" +#include "libs/json11/json11.hpp" + +USING_YOSYS_NAMESPACE + +// Use the same formatting as witness.py uses +static const char *pretty_name(IdString id) +{ + const char *c_str = id.c_str(); + const char *p = c_str; + + if (*p != '\\') + return c_str; + p++; + + if (*p == '[') { + p++; + while (*p >= '0' && *p <= '9') + p++; + if (p[0] != ']' || p[1] != 0) + return c_str; + return c_str + 1; + } + + if (!(*p >= 'a' && *p <= 'z') && !(*p >= 'A' && *p <= 'Z') && *p != '_') + return c_str; + p++; + while ((*p >= '0' && *p <= '9') || (*p >= 'a' && *p <= 'z') || (*p >= 'A' && *p <= 'Z') || *p == '_') + p++; + + if (*p != 0) + return c_str; + return c_str + 1; +} + +std::string IdPath::str() const +{ + std::string result; + + for (auto &item : *this) { + const char *pretty = pretty_name(item); + if (pretty[0] == '[') { + result += pretty; + continue; + } + if (!result.empty()) + result += '.'; + result += pretty; + if (pretty[0] == '\\' || pretty[0] == '$') + result += ' '; + } + + return result; +} + +bool IdPath::get_address(int &addr) const +{ + if (empty()) + return false; + auto &last = back(); + if (!last.begins_with("\\[")) + return false; + if (last == "\\[0]") { + addr = 0; + return true; + } + char first = last.c_str()[2]; + if (first < '1' || first > '9') + return false; + char *endptr; + addr = std::strtol(last.c_str() + 2, &endptr, 10); + return endptr[0] == ']' && endptr[1] == 0; +} + +static std::vector get_path(const json11::Json &json) +{ + std::vector result; + for (auto &path_item : json.array_items()) { + auto const &path_item_str = path_item.string_value(); + if (path_item_str.empty()) + return {};; + result.push_back(path_item_str); + } + return result; +} + +ReadWitness::ReadWitness(const std::string &filename) : + filename(filename) +{ + std::ifstream f(filename.c_str()); + if (f.fail() || GetSize(filename) == 0) + log_error("Cannot open file `%s`\n", filename.c_str()); + std::stringstream buf; + buf << f.rdbuf(); + std::string err; + json11::Json json = json11::Json::parse(buf.str(), err); + if (!err.empty()) + log_error("Failed to parse `%s`: %s\n", filename.c_str(), err.c_str()); + + std::string format = json["format"].string_value(); + + if (format.empty()) + log_error("Failed to parse `%s`: Unknown format\n", filename.c_str()); + if (format != "Yosys Witness Trace") + log_error("Failed to parse `%s`: Unsupported format `%s`\n", filename.c_str(), format.c_str()); + + for (auto &clock_json : json["clocks"].array_items()) { + Clock clock; + clock.path = get_path(clock_json["path"]); + if (clock.path.empty()) + log_error("Failed to parse `%s`: Missing path for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + auto edge_str = clock_json["edge"]; + if (edge_str.string_value() == "posedge") + clock.is_posedge = true; + else if (edge_str.string_value() == "negedge") + clock.is_negedge = true; + else + log_error("Failed to parse `%s`: Unknown edge type for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + if (!clock_json["offset"].is_number()) + log_error("Failed to parse `%s`: Unknown offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + clock.offset = clock_json["offset"].int_value(); + if (clock.offset < 0) + log_error("Failed to parse `%s`: Invalid offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str()); + clocks.push_back(clock); + } + + int bits_offset = 0; + for (auto &signal_json : json["signals"].array_items()) { + Signal signal; + signal.bits_offset = bits_offset; + signal.path = get_path(signal_json["path"]); + if (signal.path.empty()) + log_error("Failed to parse `%s`: Missing path for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + if (!signal_json["width"].is_number()) + log_error("Failed to parse `%s`: Unknown width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + signal.width = signal_json["width"].int_value(); + if (signal.width < 0) + log_error("Failed to parse `%s`: Invalid width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + bits_offset += signal.width; + if (!signal_json["offset"].is_number()) + log_error("Failed to parse `%s`: Unknown offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + signal.offset = signal_json["offset"].int_value(); + if (signal.offset < 0) + log_error("Failed to parse `%s`: Invalid offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); + signal.init_only = json["init_only"].bool_value(); + signals.push_back(signal); + } + + for (auto &step_json : json["steps"].array_items()) { + Step step; + if (!step_json["bits"].is_string()) + log_error("Failed to parse `%s`: Expected string as bits value for step %d\n", filename.c_str(), GetSize(steps)); + step.bits = step_json["bits"].string_value(); + for (char c : step.bits) { + if (c != '0' && c != '1' && c != 'x' && c != '?') + log_error("Failed to parse `%s`: Invalid bit '%c' value for step %d\n", filename.c_str(), c, GetSize(steps)); + } + steps.push_back(step); + } +} + +RTLIL::Const ReadWitness::get_bits(int t, int bits_offset, int width) const +{ + log_assert(t >= 0 && t < GetSize(steps)); + + const std::string &bits = steps[t].bits; + + RTLIL::Const result(State::Sa, width); + result.bits.reserve(width); + + int read_begin = GetSize(bits) - 1 - bits_offset; + int read_end = max(-1, read_begin - width); + + min(width, GetSize(bits) - bits_offset); + + for (int i = read_begin, j = 0; i > read_end; i--, j++) { + RTLIL::State bit = State::Sa; + switch (bits[i]) { + case '0': bit = State::S0; break; + case '1': bit = State::S1; break; + case 'x': bit = State::Sx; break; + case '?': bit = State::Sa; break; + default: + log_abort(); + } + result.bits[j] = bit; + } + + return result; +} diff --git a/kernel/yw.h b/kernel/yw.h new file mode 100644 index 000000000..8b651fd83 --- /dev/null +++ b/kernel/yw.h @@ -0,0 +1,170 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder + * + * 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. + * + */ + +#ifndef YW_H +#define YW_H + +#include "kernel/yosys.h" +#include "kernel/mem.h" + +YOSYS_NAMESPACE_BEGIN + +struct IdPath : public std::vector +{ + template + IdPath(T&&... args) : std::vector(std::forward(args)...) { } + IdPath prefix() const { return {begin(), end() - !empty()}; } + std::string str() const; + + bool has_address() const { int tmp; return get_address(tmp); }; + bool get_address(int &addr) const; + + int hash() const { return hashlib::hash_ops>::hash(*this); } +}; + +struct WitnessHierarchyItem { + RTLIL::Module *module; + RTLIL::Wire *wire = nullptr; + RTLIL::Cell *cell = nullptr; + Mem *mem = nullptr; + + WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Wire *wire) : module(module), wire(wire) {} + WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Cell *cell) : module(module), cell(cell) {} + WitnessHierarchyItem(RTLIL::Module *module, Mem *mem) : module(module), mem(mem) {} +}; + +template +void witness_hierarchy(RTLIL::Module *module, D data, T callback); + +struct ReadWitness +{ + struct Clock { + IdPath path; + int offset; + bool is_posedge; + bool is_negedge; + }; + + struct Signal { + IdPath path; + int offset; + int width; + bool init_only; + + int bits_offset; + }; + + struct Step { + std::string bits; + }; + + std::string filename; + std::vector clocks; + std::vector signals; + std::vector steps; + + ReadWitness(const std::string &filename); + + RTLIL::Const get_bits(int t, int bits_offset, int width) const; +}; + +template +void witness_hierarchy_recursion(IdPath &path, int hdlname_mode, RTLIL::Module *module, D data, T &callback) +{ + auto const &const_path = path; + size_t path_size = path.size(); + for (auto wire : module->wires()) + { + auto hdlname = hdlname_mode < 0 ? std::vector() : wire->get_hdlname_attribute(); + for (auto item : hdlname) + path.push_back("\\" + item); + if (hdlname.size() == 1 && path.back() == wire->name) + hdlname.clear(); + if (!hdlname.empty()) + callback(const_path, WitnessHierarchyItem(module, wire), data); + path.resize(path_size); + if (hdlname.empty() || hdlname_mode <= 0) { + path.push_back(wire->name); + callback(const_path, WitnessHierarchyItem(module, wire), data); + path.pop_back(); + } + } + + for (auto cell : module->cells()) + { + Module *child = module->design->module(cell->type); + if (child == nullptr) + continue; + + auto hdlname = hdlname_mode < 0 ? std::vector() : cell->get_hdlname_attribute(); + for (auto item : hdlname) + path.push_back("\\" + item); + if (hdlname.size() == 1 && path.back() == cell->name) + hdlname.clear(); + if (!hdlname.empty()) { + D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data); + witness_hierarchy_recursion(path, 1, child, child_data, callback); + } + path.resize(path_size); + if (hdlname.empty() || hdlname_mode <= 0) { + path.push_back(cell->name); + D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data); + witness_hierarchy_recursion(path, hdlname.empty() ? hdlname_mode : -1, child, child_data, callback); + path.pop_back(); + } + } + + for (auto mem : Mem::get_all_memories(module)) { + std::vector hdlname; + + if (hdlname_mode >= 0 && mem.cell != nullptr) + hdlname = mem.cell->get_hdlname_attribute(); + for (auto item : hdlname) + path.push_back("\\" + item); + if (hdlname.size() == 1 && path.back() == mem.cell->name) + hdlname.clear(); + if (!hdlname.empty()) { + callback(const_path, WitnessHierarchyItem(module, &mem), data); + } + path.resize(path_size); + + if (hdlname.empty() || hdlname_mode <= 0) { + path.push_back(mem.memid); + callback(const_path, WitnessHierarchyItem(module, &mem), data); + path.pop_back(); + + if (mem.cell != nullptr && mem.cell->name != mem.memid) { + path.push_back(mem.cell->name); + callback(const_path, WitnessHierarchyItem(module, &mem), data); + path.pop_back(); + } + } + } +} + +template +void witness_hierarchy(RTLIL::Module *module, D data, T callback) +{ + IdPath path; + witness_hierarchy_recursion(path, 0, module, data, callback); +} + +YOSYS_NAMESPACE_END + +#endif From 2dd56522159a9b55196c88063e1b950f670a5ea2 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:44:15 +0100 Subject: [PATCH 08/14] sim: Add Yosys witness (.yw) cosimulation --- passes/sat/sim.cc | 197 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 194 insertions(+), 3 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 344ebb681..9aa87c092 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -23,6 +23,7 @@ #include "kernel/mem.h" #include "kernel/fstdata.h" #include "kernel/ff.h" +#include "kernel/yw.h" #include @@ -1603,6 +1604,194 @@ struct SimWorker : SimShared write_output_files(); } + struct FoundYWPath + { + SimInstance *instance; + Wire *wire; + IdString memid; + int addr; + }; + + struct YwHierarchy { + dict signal_paths; + dict clock_paths; + }; + + YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw) + { + pool paths; + dict> mem_paths; + + for (auto &signal : yw.signals) + paths.insert(signal.path); + + for (auto &clock : yw.clocks) { + if (paths.count(clock.path)) + log_warning("Witness path `%s` is present as witness signal and as clock, treating as clock and ignoring signal data.\n", clock.path.str().c_str()); + paths.insert(clock.path); + } + for (auto &path : paths) + if (path.has_address()) + mem_paths[path.prefix()].insert(path.back()); + + YwHierarchy hierarchy; + witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) { + if (item.cell != nullptr) + return instance->children.at(item.cell); + if (item.wire != nullptr) { + if (paths.count(path)) { + if (debug) + log("witness hierarchy: found wire %s\n", path.str().c_str()); + bool inserted = hierarchy.signal_paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second; + if (!inserted) + log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); + } + } else if (item.mem) { + auto it = mem_paths.find(path); + if (it != mem_paths.end()) { + if (debug) + log("witness hierarchy: found mem %s\n", path.str().c_str()); + IdPath word_path = path; + word_path.emplace_back(); + for (auto addr_part : it->second) { + word_path.back() = addr_part; + int addr; + word_path.get_address(addr); + if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size) + continue; + bool inserted = hierarchy.signal_paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second; + if (!inserted) + log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); + } + } + } + return instance; + }); + + for (auto &path : paths) + if (!hierarchy.signal_paths.count(path)) + log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str()); + + for (auto &clock : yw.clocks) { + auto found_path_it = hierarchy.signal_paths.find(clock.path); + if (found_path_it == hierarchy.signal_paths.end()) + continue; + hierarchy.clock_paths.insert(*found_path_it); + hierarchy.signal_paths.erase(found_path_it); + paths.insert(clock.path); + } + + + // TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file + + return hierarchy; + } + + void set_yw_state(const ReadWitness &yw, const YwHierarchy &hierarchy, int t) + { + log_assert(t >= 0 && t < GetSize(yw.steps)); + + for (auto &signal : yw.signals) { + if (signal.init_only && t >= 1) + continue; + auto found_path_it = hierarchy.signal_paths.find(signal.path); + if (found_path_it == hierarchy.signal_paths.end()) + continue; + auto &found_path = found_path_it->second; + + Const value = yw.get_bits(t, signal.bits_offset, signal.width); + + if (debug) + log("yw: set %s to %s\n", signal.path.str().c_str(), log_const(value)); + + if (found_path.wire != nullptr) { + found_path.instance->set_state( + SigChunk(found_path.wire, signal.offset, signal.width), + value); + } else if (!found_path.memid.empty()) { + found_path.instance->register_memory_addr(found_path.memid, found_path.addr); + found_path.instance->set_memory_state( + found_path.memid, found_path.addr, + value); + } + } + } + + void set_yw_clocks(const ReadWitness &yw, const YwHierarchy &hierarchy, bool active_edge) + { + for (auto &clock : yw.clocks) { + if (clock.is_negedge == clock.is_posedge) + continue; + auto found_path_it = hierarchy.clock_paths.find(clock.path); + if (found_path_it == hierarchy.clock_paths.end()) + continue; + auto &found_path = found_path_it->second; + + if (found_path.wire != nullptr) { + found_path.instance->set_state( + SigChunk(found_path.wire, clock.offset, 1), + active_edge == clock.is_posedge ? State::S1 : State::S0); + } + } + } + + void run_cosim_yw_witness(Module *topmod) + { + if (!clock.empty()) + log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n"); + if (!reset.empty()) + log_cmd_error("The -reset option is not required nor supported when reading a Yosys witness file.\n"); + if (multiclock) + log_warning("The -multiclock option is not required and ignored when reading a Yosys witness file.\n"); + + ReadWitness yw(sim_filename); + + top = new SimInstance(this, scope, topmod); + register_signals(); + + YwHierarchy hierarchy = prepare_yw_hierarchy(yw); + + if (yw.steps.empty()) { + log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str()); + } else { + top->set_initstate_outputs(State::S1); + set_yw_state(yw, hierarchy, 0); + set_yw_clocks(yw, hierarchy, true); + initialize_stable_past(); + register_output_step(0); + + if (!yw.clocks.empty()) { + if (debug) + log("Simulating non-active clock edge.\n"); + set_yw_clocks(yw, hierarchy, false); + update(false); + register_output_step(5); + } + top->set_initstate_outputs(State::S0); + } + + for (int cycle = 1; cycle < GetSize(yw.steps); cycle++) + { + if (verbose) + log("Simulating cycle %d.\n", cycle); + set_yw_state(yw, hierarchy, cycle); + set_yw_clocks(yw, hierarchy, true); + update(true); + register_output_step(10 * cycle); + + if (!yw.clocks.empty()) { + if (debug) + log("Simulating non-active clock edge.\n"); + set_yw_clocks(yw, hierarchy, false); + update(false); + register_output_step(5 + 10 * cycle); + } + } + + register_output_step(10*GetSize(yw.steps)); + write_output_files(); + } + std::string define_signal(Wire *wire) { std::stringstream f; @@ -2132,9 +2321,9 @@ struct SimPass : public Pass { log(" -w\n"); log(" writeback mode: use final simulation state as new init state\n"); log("\n"); - log(" -r\n"); - log(" read simulation results file\n"); - log(" File formats supported: FST, VCD, AIW and WIT\n"); + log(" -r \n"); + log(" read simulation or formal results file\n"); + log(" File formats supported: FST, VCD, AIW, WIT and .yw\n"); log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); log(" -map \n"); @@ -2354,6 +2543,8 @@ struct SimPass : public Pass { worker.run_cosim_aiger_witness(top_mod); } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) { worker.run_cosim_btor2_witness(top_mod); + } else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) { + worker.run_cosim_yw_witness(top_mod); } else { log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); } From dda972a148aea9f422c04c6351a21f882741e6c6 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:59:29 +0100 Subject: [PATCH 09/14] sim: New -append option for Yosys witness cosim This is needed to support SBY's append option. --- passes/sat/sim.cc | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 9aa87c092..af3a38be8 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1735,7 +1735,7 @@ struct SimWorker : SimShared } } - void run_cosim_yw_witness(Module *topmod) + void run_cosim_yw_witness(Module *topmod, int append) { if (!clock.empty()) log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n"); @@ -1770,11 +1770,12 @@ struct SimWorker : SimShared top->set_initstate_outputs(State::S0); } - for (int cycle = 1; cycle < GetSize(yw.steps); cycle++) + for (int cycle = 1; cycle < GetSize(yw.steps) + append; cycle++) { if (verbose) log("Simulating cycle %d.\n", cycle); - set_yw_state(yw, hierarchy, cycle); + if (cycle < GetSize(yw.steps)) + set_yw_state(yw, hierarchy, cycle); set_yw_clocks(yw, hierarchy, true); update(true); register_output_step(10 * cycle); @@ -1788,7 +1789,7 @@ struct SimWorker : SimShared } } - register_output_step(10*GetSize(yw.steps)); + register_output_step(10 * (GetSize(yw.steps) + append)); write_output_files(); } @@ -2326,6 +2327,9 @@ struct SimPass : public Pass { log(" File formats supported: FST, VCD, AIW, WIT and .yw\n"); log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); + log(" -append \n"); + log(" number of extra clock cycles to simulate for a Yosys witness input\n"); + log("\n"); log(" -map \n"); log(" read file with port and latch symbols, needed for AIGER witness input\n"); log("\n"); @@ -2371,6 +2375,7 @@ struct SimPass : public Pass { { SimWorker worker; int numcycles = 20; + int append = 0; bool start_set = false, stop_set = false, at_set = false; log_header(design, "Executing SIM pass (simulate the circuit).\n"); @@ -2454,6 +2459,10 @@ struct SimPass : public Pass { worker.sim_filename = sim_filename; continue; } + if (args[argidx] == "-append" && argidx+1 < args.size()) { + append = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-map" && argidx+1 < args.size()) { std::string map_filename = args[++argidx]; rewrite_filename(map_filename); @@ -2544,7 +2553,7 @@ struct SimPass : public Pass { } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) { worker.run_cosim_btor2_witness(top_mod); } else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) { - worker.run_cosim_yw_witness(top_mod); + worker.run_cosim_yw_witness(top_mod, append); } else { log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); } From 29461ade177eb3dfb2ba5714c4a6bf365b09a24e Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 23 Dec 2022 16:52:52 +0100 Subject: [PATCH 10/14] Add json.{h,cc} for pretty printing JSON Avoids errors in trailing comma handling, broken indentation and improper escaping that is common when building JSON by manually concatenating strings. --- Makefile | 2 +- kernel/json.cc | 129 +++++++++++++++++++++++++++++++++++++++++++++++++ kernel/json.h | 93 +++++++++++++++++++++++++++++++++++ 3 files changed, 223 insertions(+), 1 deletion(-) create mode 100644 kernel/json.cc create mode 100644 kernel/json.h diff --git a/Makefile b/Makefile index 7aafe847d..9a579d6de 100644 --- a/Makefile +++ b/Makefile @@ -653,7 +653,7 @@ ifneq ($(ABCEXTERNAL),) kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"' endif endif -OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o +OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o ifeq ($(ENABLE_ZLIB),1) OBJS += kernel/fstdata.o endif diff --git a/kernel/json.cc b/kernel/json.cc new file mode 100644 index 000000000..6ea873329 --- /dev/null +++ b/kernel/json.cc @@ -0,0 +1,129 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder + * + * 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. + * + */ + +#include "kernel/json.h" + +USING_YOSYS_NAMESPACE + +void PrettyJson::emit_to_log() +{ + targets.push_back([](const char *raw_json) { log("%s", raw_json); }); +} + +void PrettyJson::append_to_string(std::string &target) +{ + std::string *target_p = ⌖ + targets.push_back([=](const char *raw_json) { *target_p += raw_json; }); +} + +void PrettyJson::line() +{ + int indent = state.size() - (state.empty() ? 0 : state.back() == VALUE); + newline_indent.resize(1 + 2 * indent, ' '); + raw(newline_indent.c_str()); +} + +void PrettyJson::raw(const char *raw_json) +{ + for (auto &target : targets) + target(raw_json); +} + +void PrettyJson::begin_object() +{ + begin_value(); + raw("{"); + state.push_back(OBJECT_FIRST); +} + +void PrettyJson::begin_array() +{ + begin_value(); + raw("["); + state.push_back(ARRAY_FIRST); +} + +void PrettyJson::end_object() +{ + Scope top_scope = state.back(); + state.pop_back(); + if (top_scope == OBJECT) + line(); + else + log_assert(top_scope == OBJECT_FIRST); + raw("}"); + end_value(); +} + +void PrettyJson::end_array() +{ + if (state.back() == ARRAY) + line(); + else + log_assert(state.back() == ARRAY_FIRST); + state.pop_back(); + raw("}"); + end_value(); +} + +void PrettyJson::name(const char *name) +{ + if (state.back() == OBJECT_FIRST) + state.back() = OBJECT; + else + raw(","); + line(); + raw(Json(name).dump().c_str()); + raw(": "); + state.push_back(VALUE); +} + +void PrettyJson::begin_value() +{ + if (state.back() == ARRAY_FIRST) { + line(); + state.back() = ARRAY; + } else if (state.back() == ARRAY) { + raw(","); + line(); + } else { + log_assert(state.back() == VALUE); + state.pop_back(); + } +} + +void PrettyJson::end_value() +{ + if (state.empty()) + raw("\n"); +} + +void PrettyJson::value_json(const Json &value) +{ + begin_value(); + raw(value.dump().c_str()); + end_value(); +} + +void PrettyJson::entry_json(const char *name, const Json &value) +{ + this->name(name); + this->value(value); +} + diff --git a/kernel/json.h b/kernel/json.h new file mode 100644 index 000000000..3ba355327 --- /dev/null +++ b/kernel/json.h @@ -0,0 +1,93 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder + * + * 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. + * + */ + +#ifndef JSON_H +#define JSON_H + +#include "kernel/yosys.h" +#include "libs/json11/json11.hpp" +#include + +YOSYS_NAMESPACE_BEGIN + +using json11::Json; + +class PrettyJson +{ + enum Scope { + VALUE, + OBJECT_FIRST, + OBJECT, + ARRAY_FIRST, + ARRAY, + }; + + std::string newline_indent = "\n"; + std::vector> targets; + std::vector state = {VALUE}; +public: + + void emit_to_log(); + void append_to_string(std::string &target); + + bool active() { return !targets.empty(); } + + void line(); + void raw(const char *raw_json); + void begin_object(); + void begin_array(); + void end_object(); + void end_array(); + void name(const char *name); + void begin_value(); + void end_value(); + void value_json(const Json &value); + void value(unsigned int value) { value_json(Json((int)value)); } + template + void value(T &&value) { value_json(Json(std::forward(value))); }; + + void entry_json(const char *name, const Json &value); + void entry(const char *name, unsigned int value) { entry_json(name, Json((int)value)); } + template + void entry(const char *name, T &&value) { entry_json(name, Json(std::forward(value))); }; + + template + void object(const T &&values) + { + begin_object(); + for (auto &item : values) + entry(item.first, item.second); + end_object(); + } + + template + void array(const T &&values) + { + begin_object(); + for (auto &item : values) + value(item); + end_object(); + } +}; + + + +YOSYS_NAMESPACE_END + +#endif From 3e25e61778cc9fe427bf68f45de43f26985b12c3 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 23 Dec 2022 17:22:24 +0100 Subject: [PATCH 11/14] aiger: Use new JSON code for writing aiger witness map files --- backends/aiger/aiger.cc | 98 ++++++++++++++++++++--------------------- kernel/json.cc | 43 +++++++++++++++--- kernel/json.h | 10 ++++- 3 files changed, 96 insertions(+), 55 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 513f9d95a..5cfdff3fb 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -19,6 +19,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/json.h" #include "libs/json11/json11.hpp" USING_YOSYS_NAMESPACE @@ -721,18 +722,19 @@ struct AigerWriter return path; } - void write_ywmap(std::ostream &f) + void write_ywmap(PrettyJson &json) { - 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); + json.begin_object(); + json.entry("version", "Yosys Witness Aiger map"); + json.entry("gennerator", yosys_version_str); - dict clock_lines; - dict input_lines; - dict init_lines; - dict seq_lines; + json.entry("latch_count", aig_l); + json.entry("input_count", aig_i); + + dict clock_lines; + dict input_lines; + dict init_lines; + dict seq_lines; for (auto cell : module->cells()) { @@ -751,21 +753,21 @@ struct AigerWriter 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 { + 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 { + seq_lines[a] = json11::Json(json11::Json::object { { "path", witness_path(wire) }, { "input", (a >> 1) - 1 }, { "offset", sig_qy[i].offset }, - }).dump(); + }); } } } @@ -783,60 +785,55 @@ struct AigerWriter int a = aig_map.at(sig[i]); log_assert((a & 1) == 0); - input_lines[a] += json11::Json(json11::Json::object { + 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 { + 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\": ["; + json.name("clocks"); + json.begin_array(); clock_lines.sort(); - const char *sep = "\n "; - for (auto &it : clock_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ],\n"; + for (auto &it : clock_lines) + json.value(it.second); + json.end_array(); - f << " \"inputs\": ["; + json.name("inputs"); + json.begin_array(); input_lines.sort(); - sep = "\n "; - for (auto &it : input_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ],\n"; + for (auto &it : input_lines) + json.value(it.second); + json.end_array(); - f << " \"seqs\": ["; - sep = "\n "; - for (auto &it : seq_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ],\n"; + json.name("seqs"); + json.begin_array(); + input_lines.sort(); + for (auto &it : seq_lines) + json.value(it.second); + json.end_array(); - f << " \"inits\": ["; - sep = "\n "; - for (auto &it : init_lines) { - f << sep << it.second; - sep = ",\n "; - } - f << "\n ]\n}\n"; + json.name("inits"); + json.begin_array(); + input_lines.sort(); + for (auto &it : init_lines) + json.value(it.second); + json.end_array(); + json.end_object(); } }; @@ -991,9 +988,12 @@ struct AigerBackend : public Backend { 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); + + PrettyJson json; + + if (!json.write_to_file(yw_map_filename)) + log_error("Can't open file `%s' for writing: %s\n", yw_map_filename.c_str(), strerror(errno)); + writer.write_ywmap(json); } } } AigerBackend; diff --git a/kernel/json.cc b/kernel/json.cc index 6ea873329..59f782e5e 100644 --- a/kernel/json.cc +++ b/kernel/json.cc @@ -23,13 +23,38 @@ USING_YOSYS_NAMESPACE void PrettyJson::emit_to_log() { - targets.push_back([](const char *raw_json) { log("%s", raw_json); }); + struct LogTarget : public Target { + void emit(const char *data) override { log("%s", data); } + }; + + targets.push_back(std::unique_ptr(new LogTarget)); } void PrettyJson::append_to_string(std::string &target) { - std::string *target_p = ⌖ - targets.push_back([=](const char *raw_json) { *target_p += raw_json; }); + struct AppendStringTarget : public Target { + std::string ⌖ + AppendStringTarget(std::string &target) : target(target) {} + void emit(const char *data) override { target += data; } + }; + + targets.push_back(std::unique_ptr(new AppendStringTarget(target))); +} + +bool PrettyJson::write_to_file(const std::string &path) +{ + struct WriteFileTarget : public Target { + std::ofstream target; + void emit(const char *data) override { target << data; } + void flush() override { target.flush(); } + }; + + auto target = std::unique_ptr(new WriteFileTarget); + target->target.open(path); + if (target->target.fail()) + return false; + targets.push_back(std::unique_ptr(target.release())); + return true; } void PrettyJson::line() @@ -42,7 +67,13 @@ void PrettyJson::line() void PrettyJson::raw(const char *raw_json) { for (auto &target : targets) - target(raw_json); + target->emit(raw_json); +} + +void PrettyJson::flush() +{ + for (auto &target : targets) + target->flush(); } void PrettyJson::begin_object() @@ -110,8 +141,10 @@ void PrettyJson::begin_value() void PrettyJson::end_value() { - if (state.empty()) + if (state.empty()) { raw("\n"); + flush(); + } } void PrettyJson::value_json(const Json &value) diff --git a/kernel/json.h b/kernel/json.h index 3ba355327..ae86b3aa6 100644 --- a/kernel/json.h +++ b/kernel/json.h @@ -38,18 +38,26 @@ class PrettyJson ARRAY, }; + struct Target { + virtual void emit(const char *data) = 0; + virtual void flush() {}; + virtual ~Target() {}; + }; + std::string newline_indent = "\n"; - std::vector> targets; + std::vector> targets; std::vector state = {VALUE}; public: void emit_to_log(); void append_to_string(std::string &target); + bool write_to_file(const std::string &path); bool active() { return !targets.empty(); } void line(); void raw(const char *raw_json); + void flush(); void begin_object(); void begin_array(); void end_object(); From 636b9f27052ef67192ee55a862c31e57a1ccad79 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 3 Jan 2023 14:45:41 +0100 Subject: [PATCH 12/14] 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(); From 7ddec5093f09640db0f502dfa341c25e4028563f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 10 Jan 2023 17:04:06 +0100 Subject: [PATCH 13/14] sim: Improvements and fixes for yw cosim * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output --- backends/aiger/aiger.cc | 13 +----- backends/btor/btor.cc | 13 +----- backends/smt2/witness.py | 67 +++++++++++++++++++--------- kernel/yw.cc | 2 +- kernel/yw.h | 12 +++++ passes/sat/sim.cc | 95 ++++++++++++++++++++++++++++++++++++++-- 6 files changed, 152 insertions(+), 50 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 5cfdff3fb..4ef28be9f 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -20,6 +20,7 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" #include "kernel/json.h" +#include "kernel/yw.h" #include "libs/json11/json11.hpp" USING_YOSYS_NAMESPACE @@ -710,18 +711,6 @@ struct AigerWriter f << it.second; } - 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 write_ywmap(PrettyJson &json) { json.begin_object(); diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4315f6f67..4eb675c3c 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -29,6 +29,7 @@ #include "kernel/log.h" #include "kernel/mem.h" #include "kernel/json.h" +#include "kernel/yw.h" #include USING_YOSYS_NAMESPACE @@ -141,18 +142,6 @@ 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); diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py index 14cf61fd7..8d0cc8112 100644 --- a/backends/smt2/witness.py +++ b/backends/smt2/witness.py @@ -316,6 +316,7 @@ def wit2yw(input, mapfile, output): if current_t > t: t = current_t values = WitnessValues() + array_inits = set() frames.append(values) line = next(input, None) @@ -327,39 +328,63 @@ def wit2yw(input, mapfile, output): line = next(input, None) btor_sig = btor_map.data[mode][int(tokens[0])] + btor_sigs = [btor_sig] if btor_sig is None: continue if isinstance(btor_sig, dict): addr = tokens[1] - if not addr.startswith('[') or not addr.endswith(']'): + if not addr.startswith('['): + addr = '[*]' + value = tokens[1] + else: + value = tokens[2] + if not addr.endswith(']'): raise click.ClickException(f"{input_name}: expected address in BTOR witness file") - addr = int(addr[1:-1], 2) + path = btor_sig["path"] + width = btor_sig["width"] + size = btor_sig["size"] + if addr == '[*]': + btor_sigs = [ + [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + for addr in range(size) + if (path, addr) not in array_inits + ] + array_inits.update((path, addr) for addr in range(size)) + else: + 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") + if addr < 0 or addr >= 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])) + array_inits.add((path, addr)) + btor_sig = [{ + "path": (*path, f"\\[{addr}]"), + "width": width, + "offset": 0, + }] + btor_sigs = [btor_sig] else: - signal_value = iter(reversed(tokens[1])) + value = 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) + for btor_sig in btor_sigs: + value_bits = iter(reversed(value)) - if next(signal_value, None) is not None: - raise click.ClickException(f"{input_name}: excess bits in BTOR witness file") + 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(value_bits) + + if next(value_bits, None) is not None: + raise click.ClickException(f"{input_name}: excess bits in BTOR witness file") if line is None: diff --git a/kernel/yw.cc b/kernel/yw.cc index 4a6e37a13..73e7710db 100644 --- a/kernel/yw.cc +++ b/kernel/yw.cc @@ -161,7 +161,7 @@ ReadWitness::ReadWitness(const std::string &filename) : signal.offset = signal_json["offset"].int_value(); if (signal.offset < 0) log_error("Failed to parse `%s`: Invalid offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str()); - signal.init_only = json["init_only"].bool_value(); + signal.init_only = signal_json["init_only"].bool_value(); signals.push_back(signal); } diff --git a/kernel/yw.h b/kernel/yw.h index 8b651fd83..503319b1d 100644 --- a/kernel/yw.h +++ b/kernel/yw.h @@ -52,6 +52,18 @@ struct WitnessHierarchyItem { template void witness_hierarchy(RTLIL::Module *module, D data, T callback); +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; +} + struct ReadWitness { struct Clock { diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index af3a38be8..1dd406f22 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -24,6 +24,7 @@ #include "kernel/fstdata.h" #include "kernel/ff.h" #include "kernel/yw.h" +#include "kernel/json.h" #include @@ -75,6 +76,17 @@ struct OutputWriter SimWorker *worker; }; +struct SimInstance; +struct TriggeredAssertion { + int step; + SimInstance *instance; + Cell *cell; + + TriggeredAssertion(int step, SimInstance *instance, Cell *cell) : + step(step), instance(instance), cell(cell) + { } +}; + struct SimShared { bool debug = false; @@ -95,6 +107,8 @@ struct SimShared bool date = false; bool multiclock = false; int next_output_id = 0; + int step = 0; + std::vector triggered_assertions; }; void zinit(State &v) @@ -161,6 +175,7 @@ struct SimInstance dict> signal_database; dict>> trace_mem_database; + dict, Const> trace_mem_init_database; dict fst_handles; dict fst_inputs; dict> fst_memories; @@ -306,6 +321,21 @@ struct SimInstance return log_id(module->name); } + vector witness_full_path() const + { + if (instance != nullptr) + return parent->witness_full_path(instance); + return vector(); + } + + vector witness_full_path(Cell *cell) const + { + auto result = witness_full_path(); + auto cell_path = witness_path(cell); + result.insert(result.end(), cell_path.begin(), cell_path.end()); + return result; + } + Const get_state(SigSpec sig) { Const value; @@ -700,7 +730,11 @@ struct SimInstance State a = get_state(cell->getPort(ID::A))[0]; State en = get_state(cell->getPort(ID::EN))[0]; - if (cell->type == ID($cover) && en == State::S1 && a != State::S1) + if (en == State::S1 && (cell->type == ID($cover) ? a == State::S1 : a != State::S1)) { + shared->triggered_assertions.emplace_back(shared->step, this, cell); + } + + if (cell->type == ID($cover) && en == State::S1 && a == State::S1) log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); if (cell->type == ID($assume) && en == State::S1 && a != State::S1) @@ -875,7 +909,11 @@ struct SimInstance int output_id = shared->next_output_id++; Const data; if (!shared->output_data.empty()) { - data = mem.get_init_data().extract(index * mem.width, mem.width); + auto init_it = trace_mem_init_database.find(std::make_pair(memid, addr)); + if (init_it != trace_mem_init_database.end()) + data = init_it->second; + else + data = mem.get_init_data().extract(index * mem.width, mem.width); shared->output_data.front().second.emplace(output_id, data); } trace_mem_database[memid].emplace(index, make_pair(output_id, data)); @@ -1060,6 +1098,7 @@ struct SimWorker : SimShared std::string timescale; std::string sim_filename; std::string map_filename; + std::string summary_filename; std::string scope; ~SimWorker() @@ -1103,6 +1142,9 @@ struct SimWorker : SimShared void update(bool gclk) { + if (gclk) + step += 1; + while (1) { if (debug) @@ -1130,7 +1172,7 @@ struct SimWorker : SimShared top->update_ph1(); if (debug) log("\n-- ph3 (initialize) --\n"); - top->update_ph3(false); + top->update_ph3(true); } void set_inports(pool ports, State value) @@ -1709,7 +1751,10 @@ struct SimWorker : SimShared SigChunk(found_path.wire, signal.offset, signal.width), value); } else if (!found_path.memid.empty()) { - found_path.instance->register_memory_addr(found_path.memid, found_path.addr); + if (t >= 1) + found_path.instance->register_memory_addr(found_path.memid, found_path.addr); + else + found_path.instance->trace_mem_init_database.emplace(make_pair(found_path.memid, found_path.addr), value); found_path.instance->set_memory_state( found_path.memid, found_path.addr, value); @@ -1793,6 +1838,37 @@ struct SimWorker : SimShared write_output_files(); } + void write_summary() + { + if (summary_filename.empty()) + return; + + PrettyJson json; + if (!json.write_to_file(summary_filename)) + log_error("Can't open file `%s' for writing: %s\n", summary_filename.c_str(), strerror(errno)); + + json.begin_object(); + json.entry("version", "Yosys sim summary"); + json.entry("generator", yosys_version_str); + json.entry("steps", step); + json.entry("top", log_id(top->module->name)); + json.name("assertions"); + json.begin_array(); + for (auto &assertion : triggered_assertions) { + json.begin_object(); + json.entry("step", assertion.step); + json.entry("type", log_id(assertion.cell->type)); + json.entry("path", assertion.instance->witness_full_path(assertion.cell)); + auto src = assertion.cell->get_string_attribute(ID::src); + if (!src.empty()) { + json.entry("src", src); + } + json.end_object(); + } + json.end_array(); + json.end_object(); + } + std::string define_signal(Wire *wire) { std::stringstream f; @@ -2330,6 +2406,9 @@ struct SimPass : public Pass { log(" -append \n"); log(" number of extra clock cycles to simulate for a Yosys witness input\n"); log("\n"); + log(" -summary \n"); + log(" write a JSON summary to the given file\n"); + log("\n"); log(" -map \n"); log(" read file with port and latch symbols, needed for AIGER witness input\n"); log("\n"); @@ -2469,6 +2548,12 @@ struct SimPass : public Pass { worker.map_filename = map_filename; continue; } + if (args[argidx] == "-summary" && argidx+1 < args.size()) { + std::string summary_filename = args[++argidx]; + rewrite_filename(summary_filename); + worker.summary_filename = summary_filename; + continue; + } if (args[argidx] == "-scope" && argidx+1 < args.size()) { worker.scope = args[++argidx]; continue; @@ -2558,6 +2643,8 @@ struct SimPass : public Pass { log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str()); } } + + worker.write_summary(); } } SimPass; From d6c7aa0e3d9e64827a8305610bedcc9a9df88a49 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 11 Jan 2023 17:52:25 +0100 Subject: [PATCH 14/14] sim/formalff: Clock handling for yw cosim --- backends/btor/btor.cc | 34 +++++-- backends/smt2/smt2.cc | 2 +- kernel/yw.h | 4 +- passes/sat/formalff.cc | 216 ++++++++++++++++++++++++++++++++++++++++- passes/sat/sim.cc | 51 ++++++---- 5 files changed, 274 insertions(+), 33 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 4eb675c3c..4c43e91e7 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -95,7 +95,9 @@ struct BtorWorker vector ywmap_inputs; vector ywmap_states; - dict ywmap_clocks; + dict ywmap_clock_bits; + dict ywmap_clock_inputs; + PrettyJson ywmap_json; @@ -693,7 +695,7 @@ struct BtorWorker info_clocks[nid] |= negedge ? 2 : 1; if (ywmap_json.active()) - ywmap_clocks[sig_c] |= negedge ? 2 : 1; + ywmap_clock_bits[sig_c] |= negedge ? 2 : 1; } IdString symbol; @@ -1175,6 +1177,20 @@ struct BtorWorker btorf_push("inputs"); + if (ywmap_json.active()) { + for (auto wire : module->wires()) + { + auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); + if (gclk_attr == wire->attributes.end()) + continue; + SigSpec sig = sigmap(wire); + if (gclk_attr->second == State::S1) + ywmap_clock_bits[sig] |= 1; + else if (gclk_attr->second == State::S0) + ywmap_clock_bits[sig] |= 2; + } + } + for (auto wire : module->wires()) { if (wire->attributes.count(ID::init)) { @@ -1206,12 +1222,12 @@ struct BtorWorker } 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; + for (int i = 0; i < GetSize(sig); i++) { + auto input_bit = SigBit(wire, i); + auto bit = sigmap(input_bit); + if (!ywmap_clock_bits.count(bit)) + continue; + ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit]; } } } @@ -1479,7 +1495,7 @@ struct BtorWorker ywmap_json.name("clocks"); ywmap_json.begin_array(); - for (auto &entry : ywmap_clocks) { + for (auto &entry : ywmap_clock_inputs) { if (entry.second != 1 && entry.second != 2) continue; log_assert(entry.first.is_wire()); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 3b3585b59..1ab39a405 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -998,7 +998,7 @@ struct Smt2Worker 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) { + if (wire->port_input && 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]); diff --git a/kernel/yw.h b/kernel/yw.h index 503319b1d..c2f5921b1 100644 --- a/kernel/yw.h +++ b/kernel/yw.h @@ -69,8 +69,8 @@ struct ReadWitness struct Clock { IdPath path; int offset; - bool is_posedge; - bool is_negedge; + bool is_posedge = false; + bool is_negedge = false; }; struct Signal { diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index e36379096..099df4be9 100644 --- a/passes/sat/formalff.cc +++ b/passes/sat/formalff.cc @@ -317,6 +317,172 @@ struct InitValWorker } }; +struct ReplacedPort { + IdString name; + int offset; + bool clk_pol; +}; + +struct HierarchyWorker +{ + Design *design; + pool pending; + + dict> replaced_clk_inputs; + + HierarchyWorker(Design *design) : + design(design) + { + for (auto module : design->modules()) + pending.insert(module); + } + + void propagate(); + + const std::vector &find_replaced_clk_inputs(IdString cell_type); +}; + +// Propagates replaced clock signals +struct PropagateWorker +{ + HierarchyWorker &hierarchy; + + Module *module; + SigMap sigmap; + + dict replaced_clk_bits; + dict not_drivers; + + std::vector replaced_clk_inputs; + std::vector> pending; + + PropagateWorker(Module *module, HierarchyWorker &hierarchy) : + hierarchy(hierarchy), module(module), sigmap(module) + { + hierarchy.pending.erase(module); + + for (auto wire : module->wires()) + if (wire->has_attribute(ID::replaced_by_gclk)) + replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false); + + for (auto cell : module->cells()) { + if (cell->type.in(ID($not), ID($_NOT_))) { + auto sig_a = cell->getPort(ID::A); + auto &sig_y = cell->getPort(ID::Y); + sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool()); + + for (int i = 0; i < GetSize(sig_a); i++) + if (sig_a[i].is_wire()) + not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i])); + } else { + for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type)) + replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true); + } + } + + while (!pending.empty()) { + auto current = pending.back(); + pending.pop_back(); + auto it = not_drivers.find(current.first); + if (it == not_drivers.end()) + continue; + + replace_clk_bit(it->second, !current.second, true); + } + + for (auto cell : module->cells()) { + if (cell->type.in(ID($not), ID($_NOT_))) + continue; + for (auto &conn : cell->connections()) { + if (!cell->output(conn.first)) + continue; + for (SigBit bit : conn.second) { + sigmap.apply(bit); + if (replaced_clk_bits.count(bit)) + log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n", + log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module)); + } + } + } + + for (auto port : module->ports) { + auto wire = module->wire(port); + if (!wire->port_input) + continue; + for (int i = 0; i < GetSize(wire); i++) { + SigBit bit(wire, i); + sigmap.apply(bit); + auto it = replaced_clk_bits.find(bit); + if (it == replaced_clk_bits.end()) + continue; + replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second}); + + if (it->second) { + bit = module->Not(NEW_ID, bit); + } + } + } + } + + void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute) + { + sigmap.apply(bit); + if (!bit.is_wire()) + log_error("XXX todo\n"); + + auto it = replaced_clk_bits.find(bit); + if (it != replaced_clk_bits.end()) { + if (it->second != polarity) + log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n", + log_signal(bit), log_id(module)); + return; + } + + replaced_clk_bits.emplace(bit, polarity); + + if (add_attribute) { + Wire *clk_wire = bit.wire; + if (bit.offset != 0 || GetSize(bit.wire) != 1) { + clk_wire = module->addWire(NEW_ID); + module->connect(RTLIL::SigBit(clk_wire), bit); + } + clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0; + clk_wire->set_bool_attribute(ID::keep); + } + + pending.emplace_back(bit, polarity); + } +}; + +const std::vector &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type) +{ + static const std::vector empty; + if (!cell_type.isPublic()) + return empty; + + Module *module = design->module(cell_type); + if (module == nullptr) + return empty; + + auto it = replaced_clk_inputs.find(module); + if (it != replaced_clk_inputs.end()) + return it->second; + + if (pending.count(module)) { + PropagateWorker worker(module, *this); + return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second; + } + + return empty; +} + + +void HierarchyWorker::propagate() +{ + while (!pending.empty()) + PropagateWorker worker(pending.pop(), *this); +} + struct FormalFfPass : public Pass { FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } void help() override @@ -362,6 +528,15 @@ struct FormalFfPass : public Pass { log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n"); log(" cells that drive wires with private names.\n"); log("\n"); + log(" -hierarchy\n"); + log(" Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n"); + log(" through the design hierarchy towards the toplevel inputs. This option\n"); + log(" works on the whole design and ignores the selection.\n"); + log("\n"); + log(" -assume\n"); + log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n"); + log(" attribute to the value they would have before an active clock edge.\n"); + log("\n"); // TODO: An option to check whether all FFs use the same clock before changing it to the global clock } @@ -372,6 +547,8 @@ struct FormalFfPass : public Pass { bool flag_anyinit2ff = false; bool flag_fine = false; bool flag_setundef = false; + bool flag_hierarchy = false; + bool flag_assume = false; log_header(design, "Executing FORMALFF pass.\n"); @@ -398,12 +575,20 @@ struct FormalFfPass : public Pass { flag_setundef = true; continue; } + if (args[argidx] == "-hierarchy") { + flag_hierarchy = true; + continue; + } + if (args[argidx] == "-assume") { + flag_assume = true; + continue; + } break; } extra_args(args, argidx, design); - if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff)) - log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n"); + if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume)) + log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n"); if (flag_ff2anyinit && flag_anyinit2ff) log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n"); @@ -548,6 +733,33 @@ struct FormalFfPass : public Pass { ff.emit(); } } + + if (flag_hierarchy) { + HierarchyWorker worker(design); + worker.propagate(); + } + + if (flag_assume) { + for (auto module : design->selected_modules()) { + std::vector> found; + for (auto wire : module->wires()) { + if (!wire->has_attribute(ID::replaced_by_gclk)) + continue; + bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1; + + found.emplace_back(SigSpec(wire), clk_pol); + } + for (auto pair : found) { + SigBit clk = pair.first; + + if (pair.second) + clk = module->Not(NEW_ID, clk); + + module->addAssume(NEW_ID, clk, State::S1); + + } + } + } } } FormalFfPass; diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 1dd406f22..cfe31968d 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -1655,28 +1655,25 @@ struct SimWorker : SimShared }; struct YwHierarchy { - dict signal_paths; - dict clock_paths; + dict paths; }; YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw) { + YwHierarchy hierarchy; pool paths; dict> mem_paths; for (auto &signal : yw.signals) paths.insert(signal.path); - for (auto &clock : yw.clocks) { - if (paths.count(clock.path)) - log_warning("Witness path `%s` is present as witness signal and as clock, treating as clock and ignoring signal data.\n", clock.path.str().c_str()); + for (auto &clock : yw.clocks) paths.insert(clock.path); - } + for (auto &path : paths) if (path.has_address()) mem_paths[path.prefix()].insert(path.back()); - YwHierarchy hierarchy; witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) { if (item.cell != nullptr) return instance->children.at(item.cell); @@ -1684,7 +1681,7 @@ struct SimWorker : SimShared if (paths.count(path)) { if (debug) log("witness hierarchy: found wire %s\n", path.str().c_str()); - bool inserted = hierarchy.signal_paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second; + bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second; if (!inserted) log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); } @@ -1701,7 +1698,7 @@ struct SimWorker : SimShared word_path.get_address(addr); if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size) continue; - bool inserted = hierarchy.signal_paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second; + bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second; if (!inserted) log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str()); } @@ -1711,19 +1708,35 @@ struct SimWorker : SimShared }); for (auto &path : paths) - if (!hierarchy.signal_paths.count(path)) + if (!hierarchy.paths.count(path)) log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str()); + dict> clock_inputs; + for (auto &clock : yw.clocks) { - auto found_path_it = hierarchy.signal_paths.find(clock.path); - if (found_path_it == hierarchy.signal_paths.end()) + if (clock.is_negedge == clock.is_posedge) continue; - hierarchy.clock_paths.insert(*found_path_it); - hierarchy.signal_paths.erase(found_path_it); - paths.insert(clock.path); + clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge); } + for (auto &signal : yw.signals) { + auto it = clock_inputs.find(signal.path); + if (it == clock_inputs.end()) + continue; + for (auto &clock_input : it->second) { + int offset = clock_input.first; + if (offset >= signal.offset && (offset - signal.offset) < signal.width) { + int clock_bits_offset = signal.bits_offset + (offset - signal.offset); + State expected = clock_input.second ? State::S0 : State::S1; + + for (int t = 0; t < GetSize(yw.steps); t++) { + if (yw.get_bits(t, clock_bits_offset, 1) != expected) + log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t); + } + } + } + } // TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file return hierarchy; @@ -1736,8 +1749,8 @@ struct SimWorker : SimShared for (auto &signal : yw.signals) { if (signal.init_only && t >= 1) continue; - auto found_path_it = hierarchy.signal_paths.find(signal.path); - if (found_path_it == hierarchy.signal_paths.end()) + auto found_path_it = hierarchy.paths.find(signal.path); + if (found_path_it == hierarchy.paths.end()) continue; auto &found_path = found_path_it->second; @@ -1767,8 +1780,8 @@ struct SimWorker : SimShared for (auto &clock : yw.clocks) { if (clock.is_negedge == clock.is_posedge) continue; - auto found_path_it = hierarchy.clock_paths.find(clock.path); - if (found_path_it == hierarchy.clock_paths.end()) + auto found_path_it = hierarchy.paths.find(clock.path); + if (found_path_it == hierarchy.paths.end()) continue; auto &found_path = found_path_it->second;