From 5042600c0d3adeae9ad7e936e92d4bf7ccff3e53 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:24:10 +0100 Subject: 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 + 1 file changed, 1 insertion(+) (limited to 'kernel') 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) -- cgit v1.2.3 From 1494cfff001bd23ee1bcd5dbfe1ee04dded25ac4 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 21 Dec 2022 14:42:34 +0100 Subject: 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. --- kernel/yw.cc | 209 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/yw.h | 170 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 379 insertions(+) create mode 100644 kernel/yw.cc create mode 100644 kernel/yw.h (limited to 'kernel') 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 -- cgit v1.2.3 From 29461ade177eb3dfb2ba5714c4a6bf365b09a24e Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 23 Dec 2022 16:52:52 +0100 Subject: 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. --- kernel/json.cc | 129 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/json.h | 93 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 222 insertions(+) create mode 100644 kernel/json.cc create mode 100644 kernel/json.h (limited to 'kernel') 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 -- cgit v1.2.3 From 3e25e61778cc9fe427bf68f45de43f26985b12c3 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 23 Dec 2022 17:22:24 +0100 Subject: aiger: Use new JSON code for writing aiger witness map files --- kernel/json.cc | 43 ++++++++++++++++++++++++++++++++++++++----- kernel/json.h | 10 +++++++++- 2 files changed, 47 insertions(+), 6 deletions(-) (limited to 'kernel') 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(); -- cgit v1.2.3 From 636b9f27052ef67192ee55a862c31e57a1ccad79 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 3 Jan 2023 14:45:41 +0100 Subject: Support for BTOR witness to Yosys witness conversion --- kernel/json.cc | 32 +++++++++++++++++++++----------- kernel/json.h | 5 ++++- 2 files changed, 25 insertions(+), 12 deletions(-) (limited to 'kernel') 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(); -- cgit v1.2.3 From 7ddec5093f09640db0f502dfa341c25e4028563f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 10 Jan 2023 17:04:06 +0100 Subject: sim: Improvements and fixes for yw cosim * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output --- kernel/yw.cc | 2 +- kernel/yw.h | 12 ++++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) (limited to 'kernel') 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 { -- cgit v1.2.3 From d6c7aa0e3d9e64827a8305610bedcc9a9df88a49 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 11 Jan 2023 17:52:25 +0100 Subject: sim/formalff: Clock handling for yw cosim --- kernel/yw.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') 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 { -- cgit v1.2.3