From 0ef11ee048be25b0c4a89d1865d13030b15f173c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 15 Jul 2026 14:50:06 +1200 Subject: [PATCH 01/41] wip: symfpu pass --- .gitmodules | 4 + libs/CMakeLists.txt | 6 + libs/symfpu | 1 + passes/cmds/CMakeLists.txt | 5 + passes/cmds/symfpu.cc | 411 +++++++++++++++++++++++++++++++++++++ 5 files changed, 427 insertions(+) create mode 160000 libs/symfpu create mode 100644 passes/cmds/symfpu.cc diff --git a/.gitmodules b/.gitmodules index ab798fb71..bbe58b111 100644 --- a/.gitmodules +++ b/.gitmodules @@ -20,3 +20,7 @@ [submodule "sv-elab"] path = frontends/slang/lib url = https://github.com/povik/sv-elab +[submodule "libs/symfpu"] + path = libs/symfpu + url = https://github.com/martin-cs/symfpu + branch = experimental diff --git a/libs/CMakeLists.txt b/libs/CMakeLists.txt index cb81b3af2..076390e23 100644 --- a/libs/CMakeLists.txt +++ b/libs/CMakeLists.txt @@ -7,6 +7,12 @@ add_subdirectory(json11) add_subdirectory(minisat) add_subdirectory(sha1) add_subdirectory(subcircuit) + +add_library(symfpu INTERFACE) +target_include_directories(symfpu INTERFACE + ${CMAKE_CURRENT_SOURCE_DIR} +) + block() set(BUILD_SHARED_LIBS OFF) include(FetchContent) diff --git a/libs/symfpu b/libs/symfpu new file mode 160000 index 000000000..aeaa3fa62 --- /dev/null +++ b/libs/symfpu @@ -0,0 +1 @@ +Subproject commit aeaa3fa62730148c855f5a9e0a9b7040d48e0b7e diff --git a/passes/cmds/CMakeLists.txt b/passes/cmds/CMakeLists.txt index e86ecaa20..64cf330ee 100644 --- a/passes/cmds/CMakeLists.txt +++ b/passes/cmds/CMakeLists.txt @@ -211,3 +211,8 @@ yosys_pass(sort yosys_pass(icell_liberty icell_liberty.cc ) +yosys_pass(symfpu + symfpu.cc + LIBRARIES + symfpu +) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc new file mode 100644 index 000000000..2b7664b33 --- /dev/null +++ b/passes/cmds/symfpu.cc @@ -0,0 +1,411 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2025 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/log_help.h" +#include "kernel/yosys.h" + +#include "libs/symfpu/baseTypes/shared.h" +#include "libs/symfpu/core/add.h" +#include "libs/symfpu/core/divide.h" +#include "libs/symfpu/core/ite.h" +#include "libs/symfpu/core/multiply.h" +#include "libs/symfpu/core/packing.h" +#include "libs/symfpu/core/unpackedFloat.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct prop; + +template struct bv; + +struct rm { + enum class mode { RNE, RNA, RTP, RTN, RTZ }; + mode mode; + + prop operator==(rm op) const; +}; + +thread_local Module *symfpu_mod = nullptr; + +struct rtlil_traits { + typedef uint64_t bwt; + typedef rm rm; + typedef symfpu::shared::floatingPointTypeInfo fpt; + typedef prop prop; + typedef bv sbv; + typedef bv ubv; + + // Return an instance of each rounding mode. + static rm RNE(void) { return {rm::mode::RNE}; }; + static rm RNA(void) { return {rm::mode::RNA}; }; + static rm RTP(void) { return {rm::mode::RTP}; }; + static rm RTN(void) { return {rm::mode::RTN}; }; + static rm RTZ(void) { return {rm::mode::RTZ}; }; + + // Handle various invariants. + // These can be empty to start with. + static void precondition(const bool b) { assert(b); } + static void postcondition(const bool b) { assert(b); } + static void invariant(const bool b) { assert(b); } + static void precondition(const prop &p); + static void postcondition(const prop &p); + static void invariant(const prop &p); +}; + +using bwt = rtlil_traits::bwt; +using fpt = rtlil_traits::fpt; +using ubv = rtlil_traits::ubv; +using sbv = rtlil_traits::sbv; +using symfpu::ite; +using uf = symfpu::unpackedFloat; + +PRIVATE_NAMESPACE_END + +namespace symfpu +{ +template <> struct ite { + static prop iteOp(const prop &cond, const prop &t, const prop &e); +}; +template struct ite> { + static bv iteOp(const prop &cond, const bv &t, const bv &e); +}; +template <> struct ite { + static prop iteOp(bool cond, const prop &t, const prop &e); +}; +template struct ite> { + static bv iteOp(bool cond, const bv &t, const bv &e); +}; +} // namespace symfpu + +PRIVATE_NAMESPACE_BEGIN + +struct prop { + SigBit bit; + + explicit prop(SigBit bit) : bit(bit) {} + prop(bool v) : bit(v) {} + + prop operator&&(const prop &op) const { return prop{symfpu_mod->And(NEW_ID, bit, op.bit)}; } + prop operator||(const prop &op) const { return prop{symfpu_mod->Or(NEW_ID, bit, op.bit)}; } + prop operator^(const prop &op) const { return prop{symfpu_mod->Xor(NEW_ID, bit, op.bit)}; } + prop operator!() const { return prop{symfpu_mod->Not(NEW_ID, bit)}; } + + prop operator==(const prop &op) const { return prop{symfpu_mod->Eq(NEW_ID, bit, op.bit)}; } + + const prop &named(std::string_view s) const + { + symfpu_mod->connect(symfpu_mod->addWire(symfpu_mod->uniquify(stringf("\\%s", s))), bit); + return *this; + } +}; + +template struct bv { + SigSpec bits; + + const bv &named(std::string_view s) const + { + symfpu_mod->connect(symfpu_mod->addWire(symfpu_mod->uniquify(stringf("\\%s", s)), bits.size()), bits); + return *this; + } + + friend ite>; + + explicit bv(SigSpec bits) : bits(bits) {} + explicit bv(prop prop) : bits(prop.bit) {} + explicit bv(bwt w, unsigned v) { bits = Const((long long)v, w); } + bv(bv const &other) : bits(other.bits) {} + + bwt getWidth() const { return bits.size(); } + + static bv one(bwt w) { return bv{SigSpec(1, w)}; } + static bv zero(bwt w) { return bv{SigSpec(0, w)}; } + static bv allOnes(bwt w) { return bv{SigSpec(State::S1, w)}; } + + static bv maxValue(bwt w) + { + if (!is_signed) + return allOnes(w); + log_assert(w > 0); + Const value = Const(State::S1, w); + value.set(w - 1, State::S0); + return bv{SigSpec(value)}; + } + static bv minValue(bwt w) + { + + if (!is_signed) + return zero(w); + log_assert(w > 0); + Const value = Const(State::S0, w); + value.set(w - 1, State::S1); + return bv{SigSpec(value)}; + } + + bv toSigned(void) const { return bv(*this); } + bv toUnsigned(void) const { return bv(*this); } + + bv extract(bwt upper, bwt lower) const + { + return bv{bits.extract(lower, upper + 1 - lower)}; + } + + bv extend(bwt extension) const + { + auto extended_bits = bits; + extended_bits.extend_u0(bits.size() + extension, is_signed); + return bv{extended_bits}; + } + + inline bv matchWidth(const bv &op) const + { + log_assert(this->getWidth() <= op.getWidth()); + return this->extend(op.getWidth() - this->getWidth()); + } + + inline bv resize(bwt newSize) const + { + bwt width = this->getWidth(); + + if (newSize > width) { + return this->extend(newSize - width); + } else if (newSize < width) { + return this->extract(newSize - 1, 0); + } else { + return *this; + } + } + + inline bv contract(bwt reduction) const + { + log_assert(getWidth() > reduction); + return resize(getWidth() - reduction); + } + + bv append(const bv &op) const { return bv{SigSpec({bits, op.bits})}; } + + prop isAllOnes() const { return prop{symfpu_mod->ReduceAnd(NEW_ID, bits)}; } + prop isAllZeros() const { return prop{symfpu_mod->ReduceAnd(NEW_ID, symfpu_mod->Not(NEW_ID, bits))}; } + + bv operator-() const { return bv{symfpu_mod->Neg(NEW_ID, bits, is_signed)}; } + bv operator~() const { return bv{symfpu_mod->Not(NEW_ID, bits, is_signed)}; } + + bv operator+(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return bv{symfpu_mod->Add(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator-(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return bv{symfpu_mod->Sub(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator*(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + log_assert(!is_signed); + return bv{symfpu_mod->Mul(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator%(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + log_assert(!is_signed); + return bv{symfpu_mod->Mod(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator/(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + log_assert(!is_signed); + return bv{symfpu_mod->Div(NEW_ID, bits, op.bits, is_signed)}; + } + + bv operator|(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return bv{symfpu_mod->Or(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator&(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return bv{symfpu_mod->And(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator<<(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return bv{symfpu_mod->Shl(NEW_ID, bits, op.bits, is_signed)}; + } + bv operator>>(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + if (is_signed) + return bv{symfpu_mod->Sshr(NEW_ID, bits, op.bits, is_signed)}; + else + return bv{symfpu_mod->Shr(NEW_ID, bits, op.bits, is_signed)}; + } + + prop operator==(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return prop{symfpu_mod->Eq(NEW_ID, bits, op.bits, is_signed)}; + } + + prop operator<=(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return prop{symfpu_mod->Le(NEW_ID, bits, op.bits, is_signed)}; + } + prop operator>=(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return prop{symfpu_mod->Ge(NEW_ID, bits, op.bits, is_signed)}; + } + + prop operator<(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return prop{symfpu_mod->Lt(NEW_ID, bits, op.bits, is_signed)}; + } + prop operator>(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return prop{symfpu_mod->Gt(NEW_ID, bits, op.bits, is_signed)}; + } + + inline bv increment() const { return *this + one(getWidth()); } + inline bv decrement() const { return *this - one(getWidth()); } + + inline bv modularLeftShift(const bv &op) const { return *this << op; } + + inline bv modularRightShift(const bv &op) const { return *this >> op; } + + inline bv modularIncrement() const { return this->increment(); } + + inline bv modularDecrement() const { return this->decrement(); } + + inline bv modularAdd(const bv &op) const { return *this + op; } + inline bv modularSubtract(const bv &op) const { return *this - op; } + + inline bv modularNegate() const { return -(*this); } + + inline bv signExtendRightShift(const bv &op) const { return bv{sbv(sbv(*this) >> sbv(op))}; } +}; + +PRIVATE_NAMESPACE_END + +prop symfpu::ite::iteOp(const prop &cond, const prop &t, const prop &e) { return prop{symfpu_mod->Mux(NEW_ID, e.bit, t.bit, cond.bit)}; } + +template bv symfpu::ite>::iteOp(const prop &cond, const bv &t, const bv &e) +{ + log_assert(t.getWidth() == e.getWidth()); + return bv{symfpu_mod->Mux(NEW_ID, e.bits, t.bits, cond.bit)}; +} + +prop symfpu::ite::iteOp(bool cond, const prop &t, const prop &e) { return cond ? t : e; } + +template bv symfpu::ite>::iteOp(bool cond, const bv &t, const bv &e) +{ + log_assert(t.getWidth() == e.getWidth()); + return cond ? t : e; +} + +PRIVATE_NAMESPACE_BEGIN + +prop rm::operator==(rm op) const { return mode == op.mode; } + +void rtlil_traits::precondition(const prop &cond) +{ + Cell *cell = symfpu_mod->addAssert(NEW_ID, cond.bit, State::S1); + cell->set_bool_attribute(ID(symfpu_pre)); +} +void rtlil_traits::postcondition(const prop &cond) +{ + Cell *cell = symfpu_mod->addAssert(NEW_ID, cond.bit, State::S1); + cell->set_bool_attribute(ID(symfpu_post)); +} +void rtlil_traits::invariant(const prop &cond) +{ + Cell *cell = symfpu_mod->addAssert(NEW_ID, cond.bit, State::S1); + cell->set_bool_attribute(ID(symfpu_inv)); +} + +ubv input_ubv(IdString name, int width) +{ + auto input = symfpu_mod->addWire(name, width); + input->port_input = true; + return ubv(SigSpec(input)); +} + +void output_ubv(IdString name, const ubv &value) +{ + auto output = symfpu_mod->addWire(name, value.getWidth()); + symfpu_mod->connect(output, value.bits); + output->port_output = true; +} + +struct SymFpuPass : public Pass { + SymFpuPass() : Pass("symfpu", "SymFPU based floating point netlist generator") {} + bool formatted_help() override + { + auto *help = PrettyHelp::get_current(); + help->set_group("formal"); + return false; + } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" symfpu [options] [selection]\n"); + log("\n"); + log("TODO\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *design) override + { + + log_header(design, "Executing SYMFPU pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + + break; + } + + extra_args(args, argidx, design); + + fpt format(8, 24); + + auto mod = design->addModule(ID(symfpu)); + + symfpu_mod = mod; + + uf a = symfpu::unpack(format, input_ubv(ID(a), 32)); + uf b = symfpu::unpack(format, input_ubv(ID(b), 32)); + + uf added(symfpu::add(format, rtlil_traits::RNE(), a, b, prop(true))); + uf multiplied(symfpu::multiply(format, rtlil_traits::RNE(), a, b)); + uf divided(symfpu::divide(format, rtlil_traits::RNE(), a, b)); + + output_ubv(ID(added), symfpu::pack(format, added)); + output_ubv(ID(multiplied), symfpu::pack(format, multiplied)); + output_ubv(ID(divided), symfpu::pack(format, divided)); + symfpu_mod->fixup_ports(); + } +} SymFpuPass; + +PRIVATE_NAMESPACE_END From 648fb01ffcb85630f433e301c9f064d05ce35568 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:06 +1200 Subject: [PATCH 02/41] symfpu: Configurable eb and sb --- passes/cmds/symfpu.cc | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 2b7664b33..f4640fbf0 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -364,38 +364,45 @@ struct SymFpuPass : public Pass { { auto *help = PrettyHelp::get_current(); help->set_group("formal"); - return false; - } - void help() override - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" symfpu [options] [selection]\n"); - log("\n"); - log("TODO\n"); - log("\n"); + + auto content_root = help->get_root(); + + content_root->usage("symfpu [options]"); + content_root->paragraph("TODO"); + + content_root->option("-eb ", "use bits for exponent; default=8"); + content_root->option("-sb ", "use bits for significand, including hidden bit; default=24"); + + return true; } void execute(std::vector args, RTLIL::Design *design) override { - + int eb = 8, sb = 24; log_header(design, "Executing SYMFPU pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - + if (args[argidx] == "-eb" && argidx+1 < args.size()) { + eb = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-sb" && argidx+1 < args.size()) { + sb = atoi(args[++argidx].c_str()); + continue; + } break; } extra_args(args, argidx, design); - fpt format(8, 24); + fpt format(eb, sb); auto mod = design->addModule(ID(symfpu)); symfpu_mod = mod; - uf a = symfpu::unpack(format, input_ubv(ID(a), 32)); - uf b = symfpu::unpack(format, input_ubv(ID(b), 32)); + uf a = symfpu::unpack(format, input_ubv(ID(a), eb+sb)); + uf b = symfpu::unpack(format, input_ubv(ID(b), eb+sb)); uf added(symfpu::add(format, rtlil_traits::RNE(), a, b, prop(true))); uf multiplied(symfpu::multiply(format, rtlil_traits::RNE(), a, b)); From 625aecb5d32ab110743ab481aafdc0140c483142 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:07 +1200 Subject: [PATCH 03/41] symfpu: Configurable op --- passes/cmds/symfpu.cc | 63 ++++++++++++++++++++++++++++++++++++++----- 1 file changed, 57 insertions(+), 6 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index f4640fbf0..3330cd150 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -23,9 +23,11 @@ #include "libs/symfpu/baseTypes/shared.h" #include "libs/symfpu/core/add.h" #include "libs/symfpu/core/divide.h" +#include "libs/symfpu/core/fma.h" #include "libs/symfpu/core/ite.h" #include "libs/symfpu/core/multiply.h" #include "libs/symfpu/core/packing.h" +#include "libs/symfpu/core/sqrt.h" #include "libs/symfpu/core/unpackedFloat.h" USING_YOSYS_NAMESPACE @@ -358,6 +360,13 @@ void output_ubv(IdString name, const ubv &value) output->port_output = true; } +void output_prop(IdString name, const prop &value) +{ + auto output = symfpu_mod->addWire(name); + symfpu_mod->connect(output, value.bit); + output->port_output = true; +} + struct SymFpuPass : public Pass { SymFpuPass() : Pass("symfpu", "SymFPU based floating point netlist generator") {} bool formatted_help() override @@ -373,11 +382,26 @@ struct SymFpuPass : public Pass { content_root->option("-eb ", "use bits for exponent; default=8"); content_root->option("-sb ", "use bits for significand, including hidden bit; default=24"); + auto op_option = content_root->open_option("-op "); + op_option->paragraph("floating point operation to generate, must be one of the below; default=mul"); + op_option->codeblock( + " | description | equation\n" + "-------+--------------------------------+------------\n" + "sqrt | one input square root | o = sqrt(a)\n" + "add | two input addition | o = a+b\n" + "sub | two input subtraction | o = a-b\n" + "mul | two input multiplication | o = a*b\n" + "div | two input divison | o = a/b\n" + "muladd | three input fused multiple-add | o = (a*b)+c\n" + ); + return true; } void execute(std::vector args, RTLIL::Design *design) override { int eb = 8, sb = 24; + string op = "mul"; + int inputs = 2; log_header(design, "Executing SYMFPU pass.\n"); size_t argidx; @@ -390,6 +414,22 @@ struct SymFpuPass : public Pass { sb = atoi(args[++argidx].c_str()); continue; } + if (args[argidx] == "-op" && argidx+1 < args.size()) { + op = args[++argidx]; + if (op.compare("sqrt") == 0) + inputs = 1; + else if (op.compare("add") == 0 + || op.compare("sub") == 0 + || op.compare("mul") == 0 + || op.compare("div") == 0) + inputs = 2; + else if (op.compare("muladd") == 0) + inputs = 3; + else + log_cmd_error("Unknown operation '%s'. Call help symfpu for available operations.\n", op); + log("Generating '%s'\n", op); + continue; + } break; } @@ -403,14 +443,25 @@ struct SymFpuPass : public Pass { uf a = symfpu::unpack(format, input_ubv(ID(a), eb+sb)); uf b = symfpu::unpack(format, input_ubv(ID(b), eb+sb)); + uf c = symfpu::unpack(format, input_ubv(ID(c), eb+sb)); + uf o = symfpu::unpackedFloat::makeNaN(format); - uf added(symfpu::add(format, rtlil_traits::RNE(), a, b, prop(true))); - uf multiplied(symfpu::multiply(format, rtlil_traits::RNE(), a, b)); - uf divided(symfpu::divide(format, rtlil_traits::RNE(), a, b)); + if (op.compare("sqrt") == 0) + o = symfpu::sqrt(format, rtlil_traits::RNE(), a); + else if (op.compare("add") == 0) + o = symfpu::add(format, rtlil_traits::RNE(), a, b, prop(true)); + else if (op.compare("sub") == 0) + o = symfpu::add(format, rtlil_traits::RNE(), a, b, prop(false)); + else if (op.compare("mul") == 0) + o = symfpu::multiply(format, rtlil_traits::RNE(), a, b); + else if (op.compare("div") == 0) + o = symfpu::divide(format, rtlil_traits::RNE(), a, b); + else if (op.compare("muladd") == 0) + o = symfpu::fma(format, rtlil_traits::RNE(), a, b, c); + else + log_abort(); - output_ubv(ID(added), symfpu::pack(format, added)); - output_ubv(ID(multiplied), symfpu::pack(format, multiplied)); - output_ubv(ID(divided), symfpu::pack(format, divided)); + output_ubv(ID(o), symfpu::pack(format, o)); symfpu_mod->fixup_ports(); } } SymFpuPass; From 1347790f4d2418436132707a188b79314617573b Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:25 +1200 Subject: [PATCH 04/41] symfpu: Add flags Use symfpu fork. Add tests for symfpu properties and extra edge case checking for flags. --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 81 ++++++++++- tests/Makefile | 1 + tests/symfpu/.gitignore | 1 + tests/symfpu/edges.sv | 287 +++++++++++++++++++++++++++++++++++++++ tests/symfpu/run-test.sh | 35 +++++ 6 files changed, 403 insertions(+), 4 deletions(-) create mode 100644 tests/symfpu/.gitignore create mode 100644 tests/symfpu/edges.sv create mode 100755 tests/symfpu/run-test.sh diff --git a/libs/symfpu b/libs/symfpu index aeaa3fa62..ac3816506 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit aeaa3fa62730148c855f5a9e0a9b7040d48e0b7e +Subproject commit ac38165068f507d2b46ad16b870272f0ca5a6c0a diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 3330cd150..7d58146e3 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -69,6 +69,7 @@ struct rtlil_traits { static void precondition(const prop &p); static void postcondition(const prop &p); static void invariant(const prop &p); + static void setflag(const string &name, const prop &p); }; using bwt = rtlil_traits::bwt; @@ -261,6 +262,12 @@ template struct bv { return bv{symfpu_mod->Shr(NEW_ID, bits, op.bits, is_signed)}; } + prop operator!=(const bv &op) const + { + log_assert(getWidth() == op.getWidth()); + return prop{symfpu_mod->Ne(NEW_ID, bits, op.bits, is_signed)}; + } + prop operator==(const bv &op) const { log_assert(getWidth() == op.getWidth()); @@ -367,6 +374,19 @@ void output_prop(IdString name, const prop &value) output->port_output = true; } +// unpacked floats don't track NaN signalling, so we need to check the +// raw bitvector +template prop is_sNaN(bv bitvector, int sb) { + return bitvector.extract(sb-2, sb-2).isAllZeros(); +} + +std::map flag_map; + +void rtlil_traits::setflag(const string &name, const prop &cond) +{ + flag_map[name].append(cond.bit); +} + struct SymFpuPass : public Pass { SymFpuPass() : Pass("symfpu", "SymFPU based floating point netlist generator") {} bool formatted_help() override @@ -382,6 +402,7 @@ struct SymFpuPass : public Pass { content_root->option("-eb ", "use bits for exponent; default=8"); content_root->option("-sb ", "use bits for significand, including hidden bit; default=24"); + // conversions could be useful, but for targeting Sail we don't need them auto op_option = content_root->open_option("-op "); op_option->paragraph("floating point operation to generate, must be one of the below; default=mul"); op_option->codeblock( @@ -399,6 +420,7 @@ struct SymFpuPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { + //TODO: fix multiple calls to symfpu in single Yosys instance int eb = 8, sb = 24; string op = "mul"; int inputs = 2; @@ -441,9 +463,13 @@ struct SymFpuPass : public Pass { symfpu_mod = mod; - uf a = symfpu::unpack(format, input_ubv(ID(a), eb+sb)); - uf b = symfpu::unpack(format, input_ubv(ID(b), eb+sb)); - uf c = symfpu::unpack(format, input_ubv(ID(c), eb+sb)); + auto a_bv = input_ubv(ID(a), eb+sb); + auto b_bv = input_ubv(ID(b), eb+sb); + auto c_bv = input_ubv(ID(c), eb+sb); + + uf a = symfpu::unpack(format, a_bv); + uf b = symfpu::unpack(format, b_bv); + uf c = symfpu::unpack(format, c_bv); uf o = symfpu::unpackedFloat::makeNaN(format); if (op.compare("sqrt") == 0) @@ -461,6 +487,55 @@ struct SymFpuPass : public Pass { else log_abort(); + // signaling NaN inputs raise NV + rtlil_traits::setflag("NV", (a.getNaN() && is_sNaN(a_bv, sb)) + || (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2) + || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) + ); + + // invalid operation sets output to NaN + prop invalid_operation(symfpu_mod->ReduceOr(NEW_ID, flag_map["NV"])); + rtlil_traits::invariant(!invalid_operation || o.getNaN()); + output_prop(ID(NV), invalid_operation); + + // div/0 is a (correctly-signed) infinity + prop divide_by_zero(symfpu_mod->ReduceOr(NEW_ID, flag_map["DZ"])); + rtlil_traits::invariant(!divide_by_zero || o.getInf()); + output_prop(ID(DZ), divide_by_zero); + + prop maybe_overflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["maybe_OF"])); + if (op.compare("div") == 0) + // this feels like the division should be skipped but isn't handling + // special cases until the end, so we need to manually check if the + // overflow is valid + rtlil_traits::setflag("OF", maybe_overflow && !(a.getInf() || a.getNaN() || a.getZero())); + else if (op.compare("muladd") == 0) { + // *grumbles* + prop anyInf(a.getInf() || b.getInf() || c.getInf()); + // *grumbling intensifies* + rtlil_traits::setflag("OF", maybe_overflow && !(anyInf || !o.getInf())); + } else + rtlil_traits::setflag("OF", maybe_overflow); + prop overflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["OF"])); + // overflow value depends on rounding mode + // RNE and RNA overflows to (correctly-signed) infinity + rtlil_traits::invariant(!overflow || o.getInf()); + output_prop(ID(OF), overflow); + + // inexactness doesn't have an output value test, but OF and UF imply NX + prop inexact(symfpu_mod->ReduceOr(NEW_ID, flag_map["NX"])); + output_prop(ID(NX), inexact); + + // underflow is non-zero tininess + rtlil_traits::setflag("UF", inexact && o.inSubnormalRange(format, prop(true))); + prop underflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["UF"])); + rtlil_traits::invariant(!underflow || o.inSubnormalRange(format, prop(true))); + output_prop(ID(UF), underflow); + + // over/underflow is definitionally inexact + rtlil_traits::invariant(!overflow || inexact); + rtlil_traits::invariant(!underflow || inexact); + output_ubv(ID(o), symfpu::pack(format, o)); symfpu_mod->fixup_ports(); } diff --git a/tests/Makefile b/tests/Makefile index 4f6c33ae6..26446f156 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -76,6 +76,7 @@ MK_TEST_DIRS += ./aiger MK_TEST_DIRS += ./alumacc MK_TEST_DIRS += ./check_mem MK_TEST_DIRS += ./write_verilog +MK_TEST_DIRS += ./symfpu all: vanilla-test diff --git a/tests/symfpu/.gitignore b/tests/symfpu/.gitignore new file mode 100644 index 000000000..5f4963e8b --- /dev/null +++ b/tests/symfpu/.gitignore @@ -0,0 +1 @@ +*_edges.ys diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv new file mode 100644 index 000000000..943858b9f --- /dev/null +++ b/tests/symfpu/edges.sv @@ -0,0 +1,287 @@ +module edges(); + (* anyseq *) reg [31:0] a, b, c; + reg [31:0] o; + reg NV, DZ, OF, UF, NX; + symfpu mod (.*); + + wire a_sign = a[31]; + wire [30:0] a_unsigned = a[30:0]; + wire [7:0] a_exp = a[30:23]; + wire [22:0] a_sig = a[22:0]; + wire a_zero = a_unsigned == '0; + wire a_special = a_exp == 8'hff; + wire a_inf = a_special && a_sig == '0; + wire a_nan = a_special && a_sig != '0; + wire a_qnan = a_nan && a_sig[22] && a_sig[21:0] == '0; + wire a_snan = a_nan && !a_sig[22]; + wire a_norm = a_exp > 8'h00 && !a_special; + wire a_subnorm = a_exp == 8'h00 && a_sig != '0; + wire a_finite = a_norm || a_subnorm; + + wire b_sign = b[31]; + wire [30:0] b_unsigned = b[30:0]; + wire [7:0] b_exp = b[30:23]; + wire [22:0] b_sig = b[22:0]; + wire b_zero = b_unsigned == '0; + wire b_special = b_exp == 8'hff; + wire b_inf = b_special && b_sig == '0; + wire b_nan = b_special && b_sig != '0; + wire b_qnan = b_nan && b_sig[22]; + wire b_snan = b_nan && !b_sig[22]; + wire b_norm = b_exp > 8'h00 && !b_special; + wire b_subnorm = b_exp == 8'h00 && b_sig != '0; + wire b_finite = b_norm || b_subnorm; + + wire c_sign = c[31]; + wire [30:0] c_unsigned = c[30:0]; + wire [7:0] c_exp = c[30:23]; + wire [22:0] c_sig = c[22:0]; + wire c_zero = c_unsigned == '0; + wire c_special = c_exp == 8'hff; + wire c_inf = c_special && c_sig == '0; + wire c_nan = c_special && c_sig != '0; + wire c_qnan = c_nan && c_sig[22]; + wire c_snan = c_nan && !c_sig[22]; + wire c_norm = c_exp > 8'h00 && !c_special; + wire c_subnorm = c_exp == 8'h00 && c_sig != '0; + wire c_finite = c_norm || c_subnorm; + + wire o_sign = o[31]; + wire [30:0] o_unsigned = o[30:0]; + wire [7:0] o_exp = o[30:23]; + wire [22:0] o_sig = o[22:0]; + wire o_zero = o_unsigned == '0; + wire o_special = o_exp == 8'hff; + wire o_inf = o_special && o_sig == '0; + wire o_nan = o_special && o_sig != '0; + wire o_qnan = o_nan && o_sig[22]; + wire o_snan = o_nan && !o_sig[22]; + wire o_norm = o_exp > 8'h00 && !o_special; + wire o_subnorm = o_exp == 8'h00 && o_sig != '0; + wire o_finite = o_norm || o_subnorm; + +`ifdef MULADD + wire muladd_zero = c_zero; + wire a_is_1 = a == 32'h3f800000; + wire b_is_1 = b == 32'h3f800000; + wire use_lhs = a_is_1 || b_is_1; + wire lhs_sign = b_is_1 ? a_sign : b_sign; + wire [30:0] lhs_unsigned = b_is_1 ? a_unsigned : b_unsigned; + wire [7:0] lhs_exp = b_is_1 ? a_exp : b_exp; + wire [22:0] lhs_sig = b_is_1 ? a_sig : b_sig; + wire lhs_zero = b_is_1 ? a_zero : b_zero; + wire lhs_inf = b_is_1 ? a_inf : b_inf; + wire lhs_nan = b_is_1 ? a_nan : b_nan; + wire lhs_qnan = b_is_1 ? a_qnan : b_qnan; + wire lhs_snan = b_is_1 ? a_snan : b_snan; + wire lhs_norm = b_is_1 ? a_norm : b_norm; + wire lhs_subnorm = b_is_1 ? a_subnorm : b_subnorm; + wire lhs_finite = b_is_1 ? a_finite : b_finite; + + wire rhs_sign = c_sign; + wire [30:0] rhs_unsigned = c_unsigned; + wire [7:0] rhs_exp = c_exp; + wire [22:0] rhs_sig = c_sig; + wire rhs_zero = c_zero; + wire rhs_inf = c_inf; + wire rhs_nan = c_nan; + wire rhs_qnan = c_qnan; + wire rhs_snan = c_snan; + wire rhs_norm = c_norm; + wire rhs_subnorm = c_subnorm; + wire rhs_finite = c_finite; +`else + wire muladd_zero = 1; + wire use_lhs = 1; + wire lhs_sign = a_sign; + wire [30:0] lhs_unsigned = a_unsigned; + wire [7:0] lhs_exp = a_exp; + wire [22:0] lhs_sig = a_sig; + wire lhs_zero = a_zero; + wire lhs_inf = a_inf; + wire lhs_nan = a_nan; + wire lhs_qnan = a_qnan; + wire lhs_snan = a_snan; + wire lhs_norm = a_norm; + wire lhs_subnorm = a_subnorm; + wire lhs_finite = a_finite; + + wire rhs_sign = b_sign; + wire [30:0] rhs_unsigned = b_unsigned; + wire [7:0] rhs_exp = b_exp; + wire [22:0] rhs_sig = b_sig; + wire rhs_zero = b_zero; + wire rhs_inf = b_inf; + wire rhs_nan = b_nan; + wire rhs_qnan = b_qnan; + wire rhs_snan = b_snan; + wire rhs_norm = b_norm; + wire rhs_subnorm = b_subnorm; + wire rhs_finite = b_finite; +`endif + +`ifdef SUB + wire is_sub = lhs_sign == rhs_sign; +`else + wire is_sub = lhs_sign != rhs_sign; +`endif + wire lhs_dominates = lhs_exp > rhs_exp; + wire [7:0] exp_diff = lhs_dominates ? lhs_exp - rhs_exp : rhs_exp - lhs_exp; + + always @* begin + if (a_nan) + // input NaN = output NaN + assert (o_nan); + + if (a_snan) + // signalling NaN raises invalid exception + assert (NV); + + if (a_qnan && b_qnan && c_qnan) + // quiet NaN inputs do not raise invalid exception + assert (!NV); + + if (DZ) + // output = +-inf + assert (o_inf); + + if (NV) + // output = qNaN + assert (o_qnan); + + if (OF) + // overflow is always inexact + assert (NX); + + if (UF) + // underflow is always inexact + assert (NX); + + if (OF) begin + // for RNE, output = +=inf + assert (o_inf); + end + + if (UF) + // output = subnormal + assert (o_subnorm); + + if (o_inf && !OF) + // a non-overflowing infinity is exact + assert (!NX); + + if (o_subnorm && !UF) + // a non-underflowing subnormal is exact + assert (!NX); + +`ifdef DIV + // a = finite, b = 0 + if ((a_norm || a_subnorm) && b_unsigned == '0) + assert (DZ); + // 0/0 or inf/inf + if ((a_zero && b_zero) || (a_inf && b_inf)) + assert (NV); + // dividing by a very small number will overflow + if (a_norm && a_exp > 8'h80 && b == 32'h00000001) + assert (OF); + // dividing by a much smaller number will overflow + if (a_norm && b_finite && lhs_dominates && exp_diff > 8'h80) + assert (OF); + // dividing by a much larger number will hit 0 bias + if (a_finite && b_norm && !lhs_dominates && exp_diff > 8'h7f) begin + assert (o_exp == '0); + // if the divisor is large enough, underflow (or zero) is guaranteed + if (exp_diff > 8'h95) begin + assert (NX); + assert (UF || o_zero); + end + end +`endif + +`ifdef MULS + // 0/inf or inf/0 + if ((a_inf && b_zero) || (a_zero && b_inf)) + assert (NV); + // very large multiplications overflow + if (a_unsigned == 31'h7f400000 && b_unsigned == a_unsigned && !c_special) + assert (OF); + // multiplying a small number by an even smaller number will underflow + if (a_norm && a_exp < 8'h60 && b_subnorm && !c_special) begin + assert (NX); + `ifdef MULADD + assert (UF || (c_zero ? o_zero : o == c)); + `else + assert (UF || o_zero); + `endif + if (o_zero) + assert (o_sign == a_sign ^ b_sign); + end +`endif + +`ifdef ADDSUB + // adder can't underflow, subnormals are always exact + assert (!UF); +`endif + +`ifdef ADDS + if (use_lhs) begin + // inf - inf + if (lhs_inf && rhs_inf && is_sub) + assert (NV); + // very large additions overflow + if (lhs_unsigned == 31'h7f400000 && rhs_unsigned == lhs_unsigned && !is_sub) + assert (OF); + // if the difference in exponent is more than the width of the mantissa, + // the result cannot be exact + if (lhs_finite && rhs_finite && exp_diff > 8'd24) + assert (NX || OF); + if (!UF) begin + // for a small difference in exponent with zero LSB, the result must be + // exact + if (o_finite && lhs_dominates && exp_diff < 8'd08 && rhs_sig[7:0] == 0 && lhs_sig[7:0] == 0) + assert (!NX); + if (exp_diff == 0 && !OF && lhs_sig[7:0] == 0 && rhs_sig[7:0] == 0) + assert (!NX); + end + // there's probably a better general case for this, but a moderate + // difference in exponent with non zero LSB must be inexact + if (o_finite && lhs_dominates && exp_diff > 8'd09 && rhs_sig[7:0] != 0 && lhs_sig[7:0] == 0) + assert (NX); + end +`endif + +`ifdef MULADD + // not sure how to check this in the generic case since we don't have the partial mul + if ((a_inf || b_inf) && !(a_nan || b_nan) && c_inf && (a_sign ^ b_sign ^ c_sign)) + assert (NV); + // normal multiplication, overflow addition + if (a == 31'h5f400000 && b == a && c == 32'h7f400000) begin + assert (OF); + assert (o_inf); // assuming RNE + end + // if multiplication overflows, addition can bring it back in range + if (a == 32'hc3800001 && b == 32'h7b800000 && !c_special) begin + if (c_sign) + // result is negative, so a negative addend can't + assert (OF); + else if (c_exp <= 8'he7) + // addend can't be too small + assert (OF); + else if (c_exp == 8'he8 && c_sig <= 22'h200000) + // this is just the turning point for this particular value + assert (OF); + else + // a large enough positive addend will never overflow (but is + // still likely to be inexact) + assert (!OF); + end +`endif + +`ifdef SQRT + // complex roots are invalid + if (a_sign && (a_norm || a_subnorm)) + assert (NV); +`endif + + end +endmodule \ No newline at end of file diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh new file mode 100755 index 000000000..32692b78b --- /dev/null +++ b/tests/symfpu/run-test.sh @@ -0,0 +1,35 @@ +#!/usr/bin/env bash +set -eu + +source ../gen-tests-makefile.sh + +ops="sqrt add sub mul div muladd" +for op in $ops; do + rm -f ${op}_edges.* +done + +prove_op() { + op=$1 + defs=$2 + ys_file=${op}_edges.ys + echo """\ +symfpu -op $op +sat -prove-asserts -verify +chformal -remove +opt + +read_verilog -sv -formal $defs edges.sv +chformal -lower +prep -top edges -flatten +sat -prove-asserts -verify +""" > $ys_file +} + +prove_op sqrt "-DSQRT" +prove_op add "-DADD -DADDSUB -DADDS" +prove_op sub "-DSUB -DADDSUB -DADDS" +prove_op mul "-DMUL -DMULS" +prove_op div "-DDIV" +prove_op muladd "-DMULADD -DMULS -DADDS" + +generate_mk --yosys-scripts From 2b3956947793c934c2bdb70af76aea03846d0e22 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:25 +1200 Subject: [PATCH 05/41] symfpu: Configurable rounding modes Including tests, but currently only testing rounding modes on multiply. Also missing the ...01 case. --- passes/cmds/symfpu.cc | 47 +++++++++++++++++++++++----- tests/symfpu/edges.sv | 66 ++++++++++++++++++++++++++++++++++++++-- tests/symfpu/run-test.sh | 30 ++++++++++++++++++ 3 files changed, 132 insertions(+), 11 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 7d58146e3..1cfd34b66 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -416,13 +416,25 @@ struct SymFpuPass : public Pass { "muladd | three input fused multiple-add | o = (a*b)+c\n" ); + auto rm_option = content_root->open_option("-rm "); + rm_option->paragraph("rounding mode to generate, must be one of the below; default=RNE"); + rm_option->codeblock( + " | description\n" + "-----+----------------------\n" + "RNE | round ties to even\n" + "RNA | round ties to away\n" + "RTP | round toward positive\n" + "RTN | round toward negative\n" + "RTZ | round toward zero\n" + ); + return true; } void execute(std::vector args, RTLIL::Design *design) override { //TODO: fix multiple calls to symfpu in single Yosys instance int eb = 8, sb = 24; - string op = "mul"; + string op = "mul", rounding = "RNE"; int inputs = 2; log_header(design, "Executing SYMFPU pass.\n"); @@ -452,11 +464,29 @@ struct SymFpuPass : public Pass { log("Generating '%s'\n", op); continue; } + if (args[argidx] == "-rm" && argidx+1 < args.size()) { + rounding = args[++argidx]; + continue; + } break; } extra_args(args, argidx, design); + rm rounding_mode; + if (rounding.compare("RNE") == 0) + rounding_mode = rtlil_traits::RNE(); + else if (rounding.compare("RNA") == 0) + rounding_mode = rtlil_traits::RNA(); + else if (rounding.compare("RTP") == 0) + rounding_mode = rtlil_traits::RTP(); + else if (rounding.compare("RTN") == 0) + rounding_mode = rtlil_traits::RTN(); + else if (rounding.compare("RTZ") == 0) + rounding_mode = rtlil_traits::RTZ(); + else + log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding); + fpt format(eb, sb); auto mod = design->addModule(ID(symfpu)); @@ -473,17 +503,17 @@ struct SymFpuPass : public Pass { uf o = symfpu::unpackedFloat::makeNaN(format); if (op.compare("sqrt") == 0) - o = symfpu::sqrt(format, rtlil_traits::RNE(), a); + o = symfpu::sqrt(format, rounding_mode, a); else if (op.compare("add") == 0) - o = symfpu::add(format, rtlil_traits::RNE(), a, b, prop(true)); + o = symfpu::add(format, rounding_mode, a, b, prop(true)); else if (op.compare("sub") == 0) - o = symfpu::add(format, rtlil_traits::RNE(), a, b, prop(false)); + o = symfpu::add(format, rounding_mode, a, b, prop(false)); else if (op.compare("mul") == 0) - o = symfpu::multiply(format, rtlil_traits::RNE(), a, b); + o = symfpu::multiply(format, rounding_mode, a, b); else if (op.compare("div") == 0) - o = symfpu::divide(format, rtlil_traits::RNE(), a, b); + o = symfpu::divide(format, rounding_mode, a, b); else if (op.compare("muladd") == 0) - o = symfpu::fma(format, rtlil_traits::RNE(), a, b, c); + o = symfpu::fma(format, rounding_mode, a, b, c); else log_abort(); @@ -519,7 +549,8 @@ struct SymFpuPass : public Pass { prop overflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["OF"])); // overflow value depends on rounding mode // RNE and RNA overflows to (correctly-signed) infinity - rtlil_traits::invariant(!overflow || o.getInf()); + if (rounding.compare("RNE") == 0 || rounding.compare("RNA") == 0) + rtlil_traits::invariant(!overflow || o.getInf()); output_prop(ID(OF), overflow); // inexactness doesn't have an output value test, but OF and UF imply NX diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 943858b9f..37a7adf26 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -4,6 +4,11 @@ module edges(); reg NV, DZ, OF, UF, NX; symfpu mod (.*); + wire [31:0] pos_max = 32'h7f7fffff; + wire [31:0] pos_inf = 32'h7f800000; + wire [31:0] neg_max = 32'hff7fffff; + wire [31:0] neg_inf = 32'hff800000; + wire a_sign = a[31]; wire [30:0] a_unsigned = a[30:0]; wire [7:0] a_exp = a[30:23]; @@ -128,6 +133,15 @@ module edges(); wire lhs_dominates = lhs_exp > rhs_exp; wire [7:0] exp_diff = lhs_dominates ? lhs_exp - rhs_exp : rhs_exp - lhs_exp; + wire round_p_001 = 0; + wire round_p_011 = a == 32'h40400000 && b == 32'h40000001; + wire round_n_011 = 0; + wire round_n_011 = a == 32'hc0400000 && b == 32'h40000001; + + wire [30:0] rounded_100 = 31'h40C00002; + wire [30:0] rounded_010 = 31'h40C00001; + wire [30:0] rounded_000 = 31'h40C00000; + always @* begin if (a_nan) // input NaN = output NaN @@ -157,10 +171,29 @@ module edges(); // underflow is always inexact assert (NX); - if (OF) begin - // for RNE, output = +=inf +`ifdef RNE + if (OF) // output = +-inf assert (o_inf); - end +`elsif RNA + if (OF) // output = +-inf + assert (o_inf); +`elsif RTP + if (OF) // output = +inf or -max + // RTP add is raising inexact overflow for NaN input + assert (o == pos_inf || o == neg_max); + if (o == neg_inf) + assert (!OF); +`elsif RTN + if (OF) // output = +max or -inf + assert (o == pos_max || o == neg_inf); + if (o == pos_inf) + assert (!OF); +`elsif RTZ + if (OF) // output = +-max + assert (o == pos_max || o == neg_max); + if (o_inf) // cannot overflow to infinity + assert (!OF); +`endif if (UF) // output = subnormal @@ -223,6 +256,33 @@ module edges(); assert (!UF); `endif +`ifdef RNE + if (round_p_001) assert (o_unsigned == rounded_000); + if (round_p_011) assert (o_unsigned == rounded_100); + if (round_n_011) assert (o_unsigned == rounded_000); + if (round_n_011) assert (o_unsigned == rounded_100); +`elsif RNA + if (round_p_001) assert (o_unsigned == rounded_010); + if (round_p_011) assert (o_unsigned == rounded_100); + if (round_n_011) assert (o_unsigned == rounded_010); + if (round_n_011) assert (o_unsigned == rounded_100); +`elsif RTP + if (round_p_001) assert (o_unsigned == rounded_010); + if (round_p_011) assert (o_unsigned == rounded_100); + if (round_n_011) assert (o_unsigned == rounded_000); + if (round_n_011) assert (o_unsigned == rounded_010); +`elsif RTN + if (round_p_001) assert (o_unsigned == rounded_000); + if (round_p_011) assert (o_unsigned == rounded_010); + if (round_n_011) assert (o_unsigned == rounded_010); + if (round_n_011) assert (o_unsigned == rounded_100); +`elsif RTZ + if (round_p_001) assert (o_unsigned == rounded_000); + if (round_p_011) assert (o_unsigned == rounded_010); + if (round_n_011) assert (o_unsigned == rounded_000); + if (round_n_011) assert (o_unsigned == rounded_010); +`endif + `ifdef ADDS if (use_lhs) begin // inf - inf diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 32692b78b..70d08ede2 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -3,6 +3,7 @@ set -eu source ../gen-tests-makefile.sh +# operators ops="sqrt add sub mul div muladd" for op in $ops; do rm -f ${op}_edges.* @@ -32,4 +33,33 @@ prove_op mul "-DMUL -DMULS" prove_op div "-DDIV" prove_op muladd "-DMULADD -DMULS -DADDS" +# rounding modes +rms="RNE RNA RTP RTN RTZ" +for rm in $rms; do + rm -f ${rm}_edges.* +done + +prove_rm() { + rm=$1 + defs=$2 + ys_file=${rm}_edges.ys + echo """\ +symfpu -rm $rm +sat -prove-asserts -verify +chformal -remove +opt + +read_verilog -sv -formal $defs edges.sv +chformal -lower +prep -top edges -flatten +sat -prove-asserts -verify +""" > $ys_file +} + +prove_rm RNE "-DRNE" +prove_rm RNA "-DRNA" +prove_rm RTP "-DRTP" +prove_rm RTN "-DRTN" +prove_rm RTZ "-DRTZ" + generate_mk --yosys-scripts From e44aeda246d72fd0e2a7cbcd5fd73aa8a80dec80 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:26 +1200 Subject: [PATCH 06/41] symfpu: Verifying rounding modes Works for everything but muladd. Which I saw coming, but am still frustrated by. --- libs/symfpu | 2 +- tests/symfpu/edges.sv | 73 ++++++++++++++++++++++++++++++---------- tests/symfpu/run-test.sh | 59 ++++++++++---------------------- 3 files changed, 75 insertions(+), 59 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index ac3816506..7ef44ec4a 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit ac38165068f507d2b46ad16b870272f0ca5a6c0a +Subproject commit 7ef44ec4a91de1635b3c837dc00ea5b570b3e871 diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 37a7adf26..e40b1b9b6 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -64,6 +64,7 @@ module edges(); wire o_norm = o_exp > 8'h00 && !o_special; wire o_subnorm = o_exp == 8'h00 && o_sig != '0; wire o_finite = o_norm || o_subnorm; + wire o_unclamped = o_finite && o_unsigned != 31'h7f7fffff; `ifdef MULADD wire muladd_zero = c_zero; @@ -133,20 +134,50 @@ module edges(); wire lhs_dominates = lhs_exp > rhs_exp; wire [7:0] exp_diff = lhs_dominates ? lhs_exp - rhs_exp : rhs_exp - lhs_exp; - wire round_p_001 = 0; - wire round_p_011 = a == 32'h40400000 && b == 32'h40000001; - wire round_n_011 = 0; - wire round_n_011 = a == 32'hc0400000 && b == 32'h40000001; + wire round_p_001, round_p_011, round_n_001, round_n_011; + wire [30:0] rounded_100, rounded_010, rounded_000; - wire [30:0] rounded_100 = 31'h40C00002; - wire [30:0] rounded_010 = 31'h40C00001; - wire [30:0] rounded_000 = 31'h40C00000; +`ifdef MUL + assign round_p_001 = 0; + assign round_p_011 = a == 32'h40400000 && b == 32'h40000001; + assign round_n_001 = 0; + assign round_n_011 = a == 32'hc0400000 && b == 32'h40000001; + + assign rounded_100 = 31'h40C00002; + assign rounded_010 = 31'h40C00001; + assign rounded_000 = 31'h40C00000; +`elsif ADD + assign round_p_001 = a == 32'h4c000000 && b == 32'h40000000; + assign round_p_011 = a == 32'h4c000001 && b == 32'h40000000; + assign round_n_001 = a == 32'hcc000000 && b == 32'hc0000000; + assign round_n_011 = a == 32'hcc000001 && b == 32'hc0000000; + + assign rounded_100 = 31'h4C000002; + assign rounded_010 = 31'h4C000001; + assign rounded_000 = 31'h4C000000; +`else + assign round_p_001 = 0; + assign round_p_011 = 0; + assign round_n_001 = 0; + assign round_n_011 = 0; + + assign rounded_100 = '0; + assign rounded_010 = '0; + assign rounded_000 = '0; +`endif always @* begin - if (a_nan) + if (a_nan || b_nan || c_nan) begin // input NaN = output NaN assert (o_nan); + // NaN inputs give NaN outputs, do not raise exceptions (unless signaling NV) + // assert (!DZ); + // assert (!OF); + // assert (!UF); + // assert (!NX); + end + if (a_snan) // signalling NaN raises invalid exception assert (NV); @@ -179,7 +210,6 @@ module edges(); assert (o_inf); `elsif RTP if (OF) // output = +inf or -max - // RTP add is raising inexact overflow for NaN input assert (o == pos_inf || o == neg_max); if (o == neg_inf) assert (!OF); @@ -208,6 +238,7 @@ module edges(); assert (!NX); `ifdef DIV + assume (c_zero); // a = finite, b = 0 if ((a_norm || a_subnorm) && b_unsigned == '0) assert (DZ); @@ -231,6 +262,10 @@ module edges(); end `endif +`ifdef MUL + assume (c_zero); +`endif + `ifdef MULS // 0/inf or inf/0 if ((a_inf && b_zero) || (a_zero && b_inf)) @@ -242,16 +277,18 @@ module edges(); if (a_norm && a_exp < 8'h60 && b_subnorm && !c_special) begin assert (NX); `ifdef MULADD - assert (UF || (c_zero ? o_zero : o == c)); + // within rounding + assert (UF || (c_zero ? o_zero : (o == c || o == c+1 || o == c-1))); `else assert (UF || o_zero); - `endif if (o_zero) assert (o_sign == a_sign ^ b_sign); + `endif end `endif `ifdef ADDSUB + assume (c_zero); // adder can't underflow, subnormals are always exact assert (!UF); `endif @@ -259,27 +296,27 @@ module edges(); `ifdef RNE if (round_p_001) assert (o_unsigned == rounded_000); if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_011) assert (o_unsigned == rounded_000); + if (round_n_001) assert (o_unsigned == rounded_000); if (round_n_011) assert (o_unsigned == rounded_100); `elsif RNA if (round_p_001) assert (o_unsigned == rounded_010); if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_011) assert (o_unsigned == rounded_010); + if (round_n_001) assert (o_unsigned == rounded_010); if (round_n_011) assert (o_unsigned == rounded_100); `elsif RTP if (round_p_001) assert (o_unsigned == rounded_010); if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_011) assert (o_unsigned == rounded_000); + if (round_n_001) assert (o_unsigned == rounded_000); if (round_n_011) assert (o_unsigned == rounded_010); `elsif RTN if (round_p_001) assert (o_unsigned == rounded_000); if (round_p_011) assert (o_unsigned == rounded_010); - if (round_n_011) assert (o_unsigned == rounded_010); + if (round_n_001) assert (o_unsigned == rounded_010); if (round_n_011) assert (o_unsigned == rounded_100); `elsif RTZ if (round_p_001) assert (o_unsigned == rounded_000); if (round_p_011) assert (o_unsigned == rounded_010); - if (round_n_011) assert (o_unsigned == rounded_000); + if (round_n_001) assert (o_unsigned == rounded_000); if (round_n_011) assert (o_unsigned == rounded_010); `endif @@ -298,7 +335,7 @@ module edges(); if (!UF) begin // for a small difference in exponent with zero LSB, the result must be // exact - if (o_finite && lhs_dominates && exp_diff < 8'd08 && rhs_sig[7:0] == 0 && lhs_sig[7:0] == 0) + if (o_unclamped && lhs_dominates && exp_diff < 8'd08 && rhs_sig[7:0] == 0 && lhs_sig[7:0] == 0) assert (!NX); if (exp_diff == 0 && !OF && lhs_sig[7:0] == 0 && rhs_sig[7:0] == 0) assert (!NX); @@ -338,6 +375,8 @@ module edges(); `endif `ifdef SQRT + assume (b_zero); + assume (c_zero); // complex roots are invalid if (a_sign && (a_norm || a_subnorm)) assert (NV); diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 70d08ede2..34f850657 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -3,63 +3,40 @@ set -eu source ../gen-tests-makefile.sh -# operators -ops="sqrt add sub mul div muladd" -for op in $ops; do - rm -f ${op}_edges.* -done +rm -f *_edges.* -prove_op() { +prove_rm() { op=$1 - defs=$2 - ys_file=${op}_edges.ys + rm=$2 + defs=$3 + ys_file=${op}_${rm}_edges.ys echo """\ -symfpu -op $op +symfpu -op $op -rm $rm sat -prove-asserts -verify chformal -remove opt -read_verilog -sv -formal $defs edges.sv +read_verilog -sv -formal $defs -D${rm} edges.sv chformal -lower prep -top edges -flatten -sat -prove-asserts -verify +sat -set-assumes -prove-asserts -verify """ > $ys_file } +prove_op() { + op=$1 + defs=$2 + rms="RNE RNA RTP RTN RTZ" + for rm in $rms; do + prove_rm $op $rm "$defs" + done +} + prove_op sqrt "-DSQRT" prove_op add "-DADD -DADDSUB -DADDS" prove_op sub "-DSUB -DADDSUB -DADDS" prove_op mul "-DMUL -DMULS" prove_op div "-DDIV" -prove_op muladd "-DMULADD -DMULS -DADDS" - -# rounding modes -rms="RNE RNA RTP RTN RTZ" -for rm in $rms; do - rm -f ${rm}_edges.* -done - -prove_rm() { - rm=$1 - defs=$2 - ys_file=${rm}_edges.ys - echo """\ -symfpu -rm $rm -sat -prove-asserts -verify -chformal -remove -opt - -read_verilog -sv -formal $defs edges.sv -chformal -lower -prep -top edges -flatten -sat -prove-asserts -verify -""" > $ys_file -} - -prove_rm RNE "-DRNE" -prove_rm RNA "-DRNA" -prove_rm RTP "-DRTP" -prove_rm RTN "-DRTN" -prove_rm RTZ "-DRTZ" +# prove_op muladd "-DMULADD -DMULS -DADDS" generate_mk --yosys-scripts From 2dcaa944bfd96d28ed340d806a7ef94c66eb49cf Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:26 +1200 Subject: [PATCH 07/41] symfpu: floatWithStatusFlags Now with verified muladd exceptions. --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 73 ++++++++++------------------------------ tests/symfpu/edges.sv | 25 +++++++++----- tests/symfpu/run-test.sh | 2 +- 4 files changed, 37 insertions(+), 65 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 7ef44ec4a..3be4ad042 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 7ef44ec4a91de1635b3c837dc00ea5b570b3e871 +Subproject commit 3be4ad0421f67483795d2d8f789a38d4cc303c3a diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 1cfd34b66..50587bdd4 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -78,6 +78,7 @@ using ubv = rtlil_traits::ubv; using sbv = rtlil_traits::sbv; using symfpu::ite; using uf = symfpu::unpackedFloat; +using uf_flagged = symfpu::floatWithStatusFlags; PRIVATE_NAMESPACE_END @@ -500,74 +501,36 @@ struct SymFpuPass : public Pass { uf a = symfpu::unpack(format, a_bv); uf b = symfpu::unpack(format, b_bv); uf c = symfpu::unpack(format, c_bv); - uf o = symfpu::unpackedFloat::makeNaN(format); + uf_flagged o_flagged(symfpu::unpackedFloat::makeNaN(format)); - if (op.compare("sqrt") == 0) - o = symfpu::sqrt(format, rounding_mode, a); - else if (op.compare("add") == 0) - o = symfpu::add(format, rounding_mode, a, b, prop(true)); + if (op.compare("add") == 0) + o_flagged = uf_flagged(symfpu::add_flagged(format, rounding_mode, a, b, prop(true))); else if (op.compare("sub") == 0) - o = symfpu::add(format, rounding_mode, a, b, prop(false)); + o_flagged = uf_flagged(symfpu::add_flagged(format, rounding_mode, a, b, prop(false))); else if (op.compare("mul") == 0) - o = symfpu::multiply(format, rounding_mode, a, b); + o_flagged = uf_flagged(symfpu::multiply_flagged(format, rounding_mode, a, b)); else if (op.compare("div") == 0) - o = symfpu::divide(format, rounding_mode, a, b); + o_flagged = uf_flagged(symfpu::divide_flagged(format, rounding_mode, a, b)); + else if (op.compare("sqrt") == 0) + o_flagged = uf_flagged(symfpu::sqrt_flagged(format, rounding_mode, a)); else if (op.compare("muladd") == 0) - o = symfpu::fma(format, rounding_mode, a, b, c); - else + o_flagged = symfpu::fma_flagged(format, rounding_mode, a, b, c); + else log_abort(); // signaling NaN inputs raise NV - rtlil_traits::setflag("NV", (a.getNaN() && is_sNaN(a_bv, sb)) + prop signals_invalid((a.getNaN() && is_sNaN(a_bv, sb)) || (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2) || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) ); - // invalid operation sets output to NaN - prop invalid_operation(symfpu_mod->ReduceOr(NEW_ID, flag_map["NV"])); - rtlil_traits::invariant(!invalid_operation || o.getNaN()); - output_prop(ID(NV), invalid_operation); + output_prop(ID(NV), o_flagged.nv || signals_invalid); + output_prop(ID(DZ), o_flagged.dz); + output_prop(ID(OF), o_flagged.of); + output_prop(ID(UF), o_flagged.uf); + output_prop(ID(NX), o_flagged.nx); - // div/0 is a (correctly-signed) infinity - prop divide_by_zero(symfpu_mod->ReduceOr(NEW_ID, flag_map["DZ"])); - rtlil_traits::invariant(!divide_by_zero || o.getInf()); - output_prop(ID(DZ), divide_by_zero); - - prop maybe_overflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["maybe_OF"])); - if (op.compare("div") == 0) - // this feels like the division should be skipped but isn't handling - // special cases until the end, so we need to manually check if the - // overflow is valid - rtlil_traits::setflag("OF", maybe_overflow && !(a.getInf() || a.getNaN() || a.getZero())); - else if (op.compare("muladd") == 0) { - // *grumbles* - prop anyInf(a.getInf() || b.getInf() || c.getInf()); - // *grumbling intensifies* - rtlil_traits::setflag("OF", maybe_overflow && !(anyInf || !o.getInf())); - } else - rtlil_traits::setflag("OF", maybe_overflow); - prop overflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["OF"])); - // overflow value depends on rounding mode - // RNE and RNA overflows to (correctly-signed) infinity - if (rounding.compare("RNE") == 0 || rounding.compare("RNA") == 0) - rtlil_traits::invariant(!overflow || o.getInf()); - output_prop(ID(OF), overflow); - - // inexactness doesn't have an output value test, but OF and UF imply NX - prop inexact(symfpu_mod->ReduceOr(NEW_ID, flag_map["NX"])); - output_prop(ID(NX), inexact); - - // underflow is non-zero tininess - rtlil_traits::setflag("UF", inexact && o.inSubnormalRange(format, prop(true))); - prop underflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["UF"])); - rtlil_traits::invariant(!underflow || o.inSubnormalRange(format, prop(true))); - output_prop(ID(UF), underflow); - - // over/underflow is definitionally inexact - rtlil_traits::invariant(!overflow || inexact); - rtlil_traits::invariant(!underflow || inexact); - - output_ubv(ID(o), symfpu::pack(format, o)); + output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); symfpu_mod->fixup_ports(); } } SymFpuPass; diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index e40b1b9b6..ba40140b4 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -166,16 +166,26 @@ module edges(); assign rounded_000 = '0; `endif +`ifdef RTP + wire c_muladd_turning = c_sig == '0; +`elsif RTN + wire c_muladd_turning = c_sig < 23'h400000; +`elsif RTZ + wire c_muladd_turning = c_sig == '0; +`else // RNA || RNE (default) + wire c_muladd_turning = c_sig <= 23'h200000; +`endif + always @* begin if (a_nan || b_nan || c_nan) begin // input NaN = output NaN assert (o_nan); // NaN inputs give NaN outputs, do not raise exceptions (unless signaling NV) - // assert (!DZ); - // assert (!OF); - // assert (!UF); - // assert (!NX); + assert (!DZ); + assert (!OF); + assert (!UF); + assert (!NX); end if (a_snan) @@ -226,8 +236,8 @@ module edges(); `endif if (UF) - // output = subnormal - assert (o_subnorm); + // output = subnormal or zero + assert (o_subnorm || o_zero); if (o_inf && !OF) // a non-overflowing infinity is exact @@ -354,7 +364,6 @@ module edges(); // normal multiplication, overflow addition if (a == 31'h5f400000 && b == a && c == 32'h7f400000) begin assert (OF); - assert (o_inf); // assuming RNE end // if multiplication overflows, addition can bring it back in range if (a == 32'hc3800001 && b == 32'h7b800000 && !c_special) begin @@ -364,7 +373,7 @@ module edges(); else if (c_exp <= 8'he7) // addend can't be too small assert (OF); - else if (c_exp == 8'he8 && c_sig <= 22'h200000) + else if (c_exp == 8'he8 && c_muladd_turning) // this is just the turning point for this particular value assert (OF); else diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 34f850657..e0346aecf 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -37,6 +37,6 @@ prove_op add "-DADD -DADDSUB -DADDS" prove_op sub "-DSUB -DADDSUB -DADDS" prove_op mul "-DMUL -DMULS" prove_op div "-DDIV" -# prove_op muladd "-DMULADD -DMULS -DADDS" +prove_op muladd "-DMULADD -DMULS -DADDS" generate_mk --yosys-scripts From 56e61ee8392991b25db801c7fa95871825561b52 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:26 +1200 Subject: [PATCH 08/41] symfpu: Tidying output Also switching to cleaner library branch --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 54 ++++++++++++++++++++----------------------- 2 files changed, 26 insertions(+), 30 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 3be4ad042..1452b0b39 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 3be4ad0421f67483795d2d8f789a38d4cc303c3a +Subproject commit 1452b0b39c40c1a22dcbb0cc5b22ab628247ee5b diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 50587bdd4..fb7a09377 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -381,13 +381,6 @@ template prop is_sNaN(bv bitvector, int sb) { return bitvector.extract(sb-2, sb-2).isAllZeros(); } -std::map flag_map; - -void rtlil_traits::setflag(const string &name, const prop &cond) -{ - flag_map[name].append(cond.bit); -} - struct SymFpuPass : public Pass { SymFpuPass() : Pass("symfpu", "SymFPU based floating point netlist generator") {} bool formatted_help() override @@ -501,22 +494,6 @@ struct SymFpuPass : public Pass { uf a = symfpu::unpack(format, a_bv); uf b = symfpu::unpack(format, b_bv); uf c = symfpu::unpack(format, c_bv); - uf_flagged o_flagged(symfpu::unpackedFloat::makeNaN(format)); - - if (op.compare("add") == 0) - o_flagged = uf_flagged(symfpu::add_flagged(format, rounding_mode, a, b, prop(true))); - else if (op.compare("sub") == 0) - o_flagged = uf_flagged(symfpu::add_flagged(format, rounding_mode, a, b, prop(false))); - else if (op.compare("mul") == 0) - o_flagged = uf_flagged(symfpu::multiply_flagged(format, rounding_mode, a, b)); - else if (op.compare("div") == 0) - o_flagged = uf_flagged(symfpu::divide_flagged(format, rounding_mode, a, b)); - else if (op.compare("sqrt") == 0) - o_flagged = uf_flagged(symfpu::sqrt_flagged(format, rounding_mode, a)); - else if (op.compare("muladd") == 0) - o_flagged = symfpu::fma_flagged(format, rounding_mode, a, b, c); - else - log_abort(); // signaling NaN inputs raise NV prop signals_invalid((a.getNaN() && is_sNaN(a_bv, sb)) @@ -524,13 +501,32 @@ struct SymFpuPass : public Pass { || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) ); - output_prop(ID(NV), o_flagged.nv || signals_invalid); - output_prop(ID(DZ), o_flagged.dz); - output_prop(ID(OF), o_flagged.of); - output_prop(ID(UF), o_flagged.uf); - output_prop(ID(NX), o_flagged.nx); + // calling this more than once will fail + auto output_fpu = [&signals_invalid, &format](const uf_flagged &o_flagged) { + output_prop(ID(NV), o_flagged.nv || signals_invalid); + output_prop(ID(DZ), o_flagged.dz); + output_prop(ID(OF), o_flagged.of); + output_prop(ID(UF), o_flagged.uf); + output_prop(ID(NX), o_flagged.nx); + + output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); + }; + + if (op.compare("add") == 0) + output_fpu(symfpu::add_flagged(format, rounding_mode, a, b, prop(true))); + else if (op.compare("sub") == 0) + output_fpu(symfpu::add_flagged(format, rounding_mode, a, b, prop(false))); + else if (op.compare("mul") == 0) + output_fpu(symfpu::multiply_flagged(format, rounding_mode, a, b)); + else if (op.compare("div") == 0) + output_fpu(symfpu::divide_flagged(format, rounding_mode, a, b)); + else if (op.compare("sqrt") == 0) + output_fpu(symfpu::sqrt_flagged(format, rounding_mode, a)); + else if (op.compare("muladd") == 0) + output_fpu(symfpu::fma_flagged(format, rounding_mode, a, b, c)); + else + log_abort(); - output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); symfpu_mod->fixup_ports(); } } SymFpuPass; From 717f7c5d3a39e1e769658c3a015016bf639e2c16 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:27 +1200 Subject: [PATCH 09/41] symfpu: Dynamic rounding mode --- passes/cmds/symfpu.cc | 89 +++++++++++++++++++--------- tests/symfpu/edges.sv | 124 +++++++++++++++++++++++---------------- tests/symfpu/run-test.sh | 10 ++-- 3 files changed, 140 insertions(+), 83 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index fb7a09377..05ee59f2a 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -79,6 +79,7 @@ using sbv = rtlil_traits::sbv; using symfpu::ite; using uf = symfpu::unpackedFloat; using uf_flagged = symfpu::floatWithStatusFlags; +using uf_flagged_ite = symfpu::ite; PRIVATE_NAMESPACE_END @@ -411,16 +412,18 @@ struct SymFpuPass : public Pass { ); auto rm_option = content_root->open_option("-rm "); - rm_option->paragraph("rounding mode to generate, must be one of the below; default=RNE"); + rm_option->paragraph("rounding mode to generate, must be one of the below; default=DYN"); rm_option->codeblock( - " | description\n" - "-----+----------------------\n" - "RNE | round ties to even\n" - "RNA | round ties to away\n" - "RTP | round toward positive\n" - "RTN | round toward negative\n" - "RTZ | round toward zero\n" + " | rm | description\n" + "-----+--------+----------------------\n" + "RNE | 00001 | round ties to even\n" + "RNA | 00010 | round ties to away\n" + "RTP | 00100 | round toward positive\n" + "RTN | 01000 | round toward negative\n" + "RTZ | 10000 | round toward zero\n" + "DYN | xxxxx | round based on 'rm' input signal\n" ); + rm_option->paragraph("Note: when not using DYN mode, the 'rm' input is ignored."); return true; } @@ -428,7 +431,7 @@ struct SymFpuPass : public Pass { { //TODO: fix multiple calls to symfpu in single Yosys instance int eb = 8, sb = 24; - string op = "mul", rounding = "RNE"; + string op = "mul", rounding = "DYN"; int inputs = 2; log_header(design, "Executing SYMFPU pass.\n"); @@ -470,14 +473,16 @@ struct SymFpuPass : public Pass { rm rounding_mode; if (rounding.compare("RNE") == 0) rounding_mode = rtlil_traits::RNE(); - else if (rounding.compare("RNA") == 0) + else if (rounding.compare("RNA") == 0) rounding_mode = rtlil_traits::RNA(); - else if (rounding.compare("RTP") == 0) + else if (rounding.compare("RTP") == 0) rounding_mode = rtlil_traits::RTP(); - else if (rounding.compare("RTN") == 0) + else if (rounding.compare("RTN") == 0) rounding_mode = rtlil_traits::RTN(); - else if (rounding.compare("RTZ") == 0) + else if (rounding.compare("RTZ") == 0) rounding_mode = rtlil_traits::RTZ(); + else if (rounding.compare("DYN") == 0) + rounding_mode = {}; else log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding); @@ -495,12 +500,38 @@ struct SymFpuPass : public Pass { uf b = symfpu::unpack(format, b_bv); uf c = symfpu::unpack(format, c_bv); + auto rm_wire = symfpu_mod->addWire(ID(rm), 5); + rm_wire->port_input = true; + SigSpec rm_sig(rm_wire); + prop rm_RNE(rm_sig[0]); + prop rm_RNA(rm_sig[1]); + prop rm_RTP(rm_sig[2]); + prop rm_RTN(rm_sig[3]); + prop rm_RTZ(rm_sig[4]); + // signaling NaN inputs raise NV prop signals_invalid((a.getNaN() && is_sNaN(a_bv, sb)) || (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2) || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) ); + auto make_op = [&op, &format, &a, &b, &c](rm rounding_mode) { + if (op.compare("add") == 0) + return symfpu::add_flagged(format, rounding_mode, a, b, prop(true)); + else if (op.compare("sub") == 0) + return symfpu::add_flagged(format, rounding_mode, a, b, prop(false)); + else if (op.compare("mul") == 0) + return symfpu::multiply_flagged(format, rounding_mode, a, b); + else if (op.compare("div") == 0) + return symfpu::divide_flagged(format, rounding_mode, a, b); + else if (op.compare("sqrt") == 0) + return symfpu::sqrt_flagged(format, rounding_mode, a); + else if (op.compare("muladd") == 0) + return symfpu::fma_flagged(format, rounding_mode, a, b, c); + else + log_abort(); + }; + // calling this more than once will fail auto output_fpu = [&signals_invalid, &format](const uf_flagged &o_flagged) { output_prop(ID(NV), o_flagged.nv || signals_invalid); @@ -512,20 +543,24 @@ struct SymFpuPass : public Pass { output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); }; - if (op.compare("add") == 0) - output_fpu(symfpu::add_flagged(format, rounding_mode, a, b, prop(true))); - else if (op.compare("sub") == 0) - output_fpu(symfpu::add_flagged(format, rounding_mode, a, b, prop(false))); - else if (op.compare("mul") == 0) - output_fpu(symfpu::multiply_flagged(format, rounding_mode, a, b)); - else if (op.compare("div") == 0) - output_fpu(symfpu::divide_flagged(format, rounding_mode, a, b)); - else if (op.compare("sqrt") == 0) - output_fpu(symfpu::sqrt_flagged(format, rounding_mode, a)); - else if (op.compare("muladd") == 0) - output_fpu(symfpu::fma_flagged(format, rounding_mode, a, b, c)); - else - log_abort(); + if (rounding.compare("DYN") != 0) + output_fpu(make_op(rounding_mode)); + else { + auto out_RNE = make_op(rtlil_traits::RNE()); + auto out_RNA = make_op(rtlil_traits::RNA()); + auto out_RTP = make_op(rtlil_traits::RTP()); + auto out_RTN = make_op(rtlil_traits::RTN()); + auto out_RTZ = make_op(rtlil_traits::RTZ()); + output_fpu( + uf_flagged_ite::iteOp(rm_RNE, out_RNE, + uf_flagged_ite::iteOp(rm_RNA, out_RNA, + uf_flagged_ite::iteOp(rm_RTP, out_RTP, + uf_flagged_ite::iteOp(rm_RTN, out_RTN, + uf_flagged_ite::iteOp(rm_RTZ, out_RTZ, + uf_flagged::makeNaN(format, prop(true))))))) + ); + } + symfpu_mod->fixup_ports(); } diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index ba40140b4..eecb60bad 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -1,5 +1,6 @@ module edges(); (* anyseq *) reg [31:0] a, b, c; + (* anyseq *) reg [4:0] rm; reg [31:0] o; reg NV, DZ, OF, UF, NX; symfpu mod (.*); @@ -166,15 +167,16 @@ module edges(); assign rounded_000 = '0; `endif -`ifdef RTP - wire c_muladd_turning = c_sig == '0; -`elsif RTN - wire c_muladd_turning = c_sig < 23'h400000; -`elsif RTZ - wire c_muladd_turning = c_sig == '0; -`else // RNA || RNE (default) - wire c_muladd_turning = c_sig <= 23'h200000; -`endif + wire rm_RNE = rm[0] == 1'b1; + wire rm_RNA = rm[1:0] == 2'b10; + wire rm_RTP = rm[2:0] == 3'b100; + wire rm_RTN = rm[3:0] == 4'b1000; + wire rm_RTZ = rm[4:0] == 5'b10000; + + wire c_muladd_turning = rm_RNE || rm_RNA ? c_sig <= 23'h200000 : + rm_RTP ? c_sig == '0 : + rm_RTN ? c_sig < 23'h400000 : + c_sig == '0; always @* begin if (a_nan || b_nan || c_nan) begin @@ -212,29 +214,6 @@ module edges(); // underflow is always inexact assert (NX); -`ifdef RNE - if (OF) // output = +-inf - assert (o_inf); -`elsif RNA - if (OF) // output = +-inf - assert (o_inf); -`elsif RTP - if (OF) // output = +inf or -max - assert (o == pos_inf || o == neg_max); - if (o == neg_inf) - assert (!OF); -`elsif RTN - if (OF) // output = +max or -inf - assert (o == pos_max || o == neg_inf); - if (o == pos_inf) - assert (!OF); -`elsif RTZ - if (OF) // output = +-max - assert (o == pos_max || o == neg_max); - if (o_inf) // cannot overflow to infinity - assert (!OF); -`endif - if (UF) // output = subnormal or zero assert (o_subnorm || o_zero); @@ -304,32 +283,73 @@ module edges(); `endif `ifdef RNE - if (round_p_001) assert (o_unsigned == rounded_000); - if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_001) assert (o_unsigned == rounded_000); - if (round_n_011) assert (o_unsigned == rounded_100); + assume (rm_RNE); `elsif RNA - if (round_p_001) assert (o_unsigned == rounded_010); - if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_001) assert (o_unsigned == rounded_010); - if (round_n_011) assert (o_unsigned == rounded_100); + assume (rm_RNA); `elsif RTP - if (round_p_001) assert (o_unsigned == rounded_010); - if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_001) assert (o_unsigned == rounded_000); - if (round_n_011) assert (o_unsigned == rounded_010); + assume (rm_RTP); `elsif RTN - if (round_p_001) assert (o_unsigned == rounded_000); - if (round_p_011) assert (o_unsigned == rounded_010); - if (round_n_001) assert (o_unsigned == rounded_010); - if (round_n_011) assert (o_unsigned == rounded_100); + assume (rm_RTN); `elsif RTZ - if (round_p_001) assert (o_unsigned == rounded_000); - if (round_p_011) assert (o_unsigned == rounded_010); - if (round_n_001) assert (o_unsigned == rounded_000); - if (round_n_011) assert (o_unsigned == rounded_010); + assume (rm_RTZ); +`else + assume ($onehot(rm)); `endif + if (OF) + // rounding mode determines if overflow value is inf or max + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_inf); + 5'bzzz10 /* RNA */: assert (o_inf); + 5'bzz100 /* RTP */: assert (o == pos_inf || o == neg_max); + 5'bz1000 /* RTN */: assert (o == pos_max || o == neg_inf); + 5'b10000 /* RTZ */: assert (o == pos_max || o == neg_max); + endcase + + // RTx modes cannot overflow to the far infinity + if (rm_RTP && o == neg_inf) + assert (!OF); + if (rm_RTN && o == pos_inf) + assert (!OF); + + // RTZ cannot overflow to either + if (rm_RTZ && o_inf) + assert (!OF); + + // test rounding + if (round_p_001) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_000); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_010); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_010); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_000); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_000); + endcase + if (round_p_011) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_100); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_100); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_100); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_010); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_010); + endcase + if (round_n_001) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_000); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_010); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_000); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_010); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_000); + endcase + if (round_n_011) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_100); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_100); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_010); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_100); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_010); + endcase + `ifdef ADDS if (use_lhs) begin // inf - inf diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index e0346aecf..36db8f395 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -10,9 +10,11 @@ prove_rm() { rm=$2 defs=$3 ys_file=${op}_${rm}_edges.ys + echo "symfpu -op $op -rm $rm" > $ys_file + if [[ $rm != "DYN" ]] then + echo "sat -prove-asserts -verify" >> $ys_file + fi echo """\ -symfpu -op $op -rm $rm -sat -prove-asserts -verify chformal -remove opt @@ -20,13 +22,13 @@ read_verilog -sv -formal $defs -D${rm} edges.sv chformal -lower prep -top edges -flatten sat -set-assumes -prove-asserts -verify -""" > $ys_file +""" >> $ys_file } prove_op() { op=$1 defs=$2 - rms="RNE RNA RTP RTN RTZ" + rms="RNE RNA RTP RTN RTZ DYN" for rm in $rms; do prove_rm $op $rm "$defs" done From 70dad5a06e427fefae6b5b48557244486fb98d40 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:27 +1200 Subject: [PATCH 10/41] Don't raise DZ when left is inf --- libs/symfpu | 2 +- tests/symfpu/edges.sv | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 1452b0b39..f5eccd093 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 1452b0b39c40c1a22dcbb0cc5b22ab628247ee5b +Subproject commit f5eccd09323fba1a7ee78df2e7bb43dc5509dfe5 diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index eecb60bad..9959ad1bd 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -228,9 +228,8 @@ module edges(); `ifdef DIV assume (c_zero); - // a = finite, b = 0 - if ((a_norm || a_subnorm) && b_unsigned == '0) - assert (DZ); + // div/zero when a = finite, b = 0 + assert (!DZ || ((a_norm || a_subnorm) && b_unsigned == '0)); // 0/0 or inf/inf if ((a_zero && b_zero) || (a_inf && b_inf)) assert (NV); From 5751023b6cc9a930536a3f0ff24e768386db8a06 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:27 +1200 Subject: [PATCH 11/41] tests/symfpu: UF to ebmin is valid --- tests/symfpu/edges.sv | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 9959ad1bd..d0e388f5f 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -66,6 +66,7 @@ module edges(); wire o_subnorm = o_exp == 8'h00 && o_sig != '0; wire o_finite = o_norm || o_subnorm; wire o_unclamped = o_finite && o_unsigned != 31'h7f7fffff; + wire o_ebmin = o_exp == 8'h01 && o_sig == '0; `ifdef MULADD wire muladd_zero = c_zero; @@ -215,8 +216,8 @@ module edges(); assert (NX); if (UF) - // output = subnormal or zero - assert (o_subnorm || o_zero); + // output = subnormal or zero or +-e^bmin + assert (o_subnorm || o_zero || o_ebmin); if (o_inf && !OF) // a non-overflowing infinity is exact @@ -228,8 +229,8 @@ module edges(); `ifdef DIV assume (c_zero); - // div/zero when a = finite, b = 0 - assert (!DZ || ((a_norm || a_subnorm) && b_unsigned == '0)); + // div/zero only when a is finite + assert (DZ ^~ (a_finite && b_zero)); // 0/0 or inf/inf if ((a_zero && b_zero) || (a_inf && b_inf)) assert (NV); @@ -305,15 +306,19 @@ module edges(); 5'b10000 /* RTZ */: assert (o == pos_max || o == neg_max); endcase - // RTx modes cannot overflow to the far infinity - if (rm_RTP && o == neg_inf) - assert (!OF); - if (rm_RTN && o == pos_inf) - assert (!OF); + // RTx modes cannot underflow to the opposite ebmin (or either for RTZ) + if (UF && o_ebmin) + if (o_sign) + assert (rm_RNE || rm_RNA || rm_RTN); + else + assert (rm_RNE || rm_RNA || rm_RTP); - // RTZ cannot overflow to either - if (rm_RTZ && o_inf) - assert (!OF); + // and the same for overflowing to infinities + if (OF && o_inf) + if (o_sign) + assert (rm_RNE || rm_RNA || rm_RTN); + else + assert (rm_RNE || rm_RNA || rm_RTP); // test rounding if (round_p_001) From b818e1c8ca8d708fd56524d682945babbb2abb88 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:28 +1200 Subject: [PATCH 12/41] Fix tininess when rounding to ebmin --- libs/symfpu | 2 +- tests/symfpu/edges.sv | 16 +++++++++++++++- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index f5eccd093..7fce38f94 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit f5eccd09323fba1a7ee78df2e7bb43dc5509dfe5 +Subproject commit 7fce38f94fa0730b3010443eb9a1390c91e5fba0 diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index d0e388f5f..90b8b0de7 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -249,13 +249,27 @@ module edges(); assert (UF || o_zero); end end + // an unrounded result between +-e^bmin is still an underflow when rounded to ebmin + if (a_unsigned == 31'h0031b7be && b_unsigned == 31'h3ec6def9) + assert (UF); `endif `ifdef MUL assume (c_zero); + // an unrounded result between +-e^bmin is still an underflow when rounded to ebmin + if (a_unsigned == 31'h0ffffffd && b_unsigned == 31'h30000001) begin + assert (UF); + // but it's only ebmin when rounded towards the nearest infinity + assert (o_ebmin ^~ (o_sign ? rm_RTN : rm_RTP)); + end `endif `ifdef MULS + if (a_unsigned == 31'h0ffffffd && b_unsigned == 31'h30000001 && c_subnorm) + if (!c_sign ^ b_sign ^ a_sign) + assert (!UF); + else + assert (UF); // 0/inf or inf/0 if ((a_inf && b_zero) || (a_zero && b_inf)) assert (NV); @@ -263,7 +277,7 @@ module edges(); if (a_unsigned == 31'h7f400000 && b_unsigned == a_unsigned && !c_special) assert (OF); // multiplying a small number by an even smaller number will underflow - if (a_norm && a_exp < 8'h60 && b_subnorm && !c_special) begin + if (a_norm && a_exp < 8'h68 && b_subnorm && !c_special) begin assert (NX); `ifdef MULADD // within rounding From 3f22dabb8dc462f43e63ab9a93025dbb1425527e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:28 +1200 Subject: [PATCH 13/41] tests/symfpu: Add cover checks Include mask/map for abc inputs (and switch to `anyconst` instead of `anyseq`). Add false divide check for mantissa. Covers aren't currently being tested by anything (and have to be removed for `sat`), but I've been using it locally with SBY to confirm that the different edge cases are able to be verified (e.g. when verifying HardFloat against symfpu while using the masked inputs to reduce solver time). --- tests/symfpu/edges.sv | 176 ++++++++++++++++++++++++++++++++++++++- tests/symfpu/run-test.sh | 1 + 2 files changed, 174 insertions(+), 3 deletions(-) diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 90b8b0de7..4b65c18f8 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -1,5 +1,29 @@ -module edges(); - (* anyseq *) reg [31:0] a, b, c; +module edges(input clk); + +`ifdef MASK + (* anyconst *) reg [31:0] a_in, b_in, c_in; + wire [31:0] a, b, c; + assign a = a_in & 32'hffc42108; + assign b = b_in & 32'hfff80001; + assign c = c_in & 32'hfff80001; +`elsif MAP + (* anyconst *) reg [31:0] a_pre, b_pre, c_pre; + wire [31:0] a_in, b_in, c_in; + // assuming 8/24 + assign a_in[31:22] = a_pre[31:22]; + assign b_in[31:22] = b_pre[31:22]; + assign a_in[21:0] = (a_pre[21:0] & 22'h042100) | (|(a_pre[21:0] & ~22'h042100) << 3); + assign b_in[21:0] = (b_pre[21:0] & 22'h380000) | (|(b_pre[21:0] & ~22'h380000) << 0); + assign c_in = c_pre; + + wire [31:0] a, b, c; + assign a = a_in & 32'hffc42108; + assign b = b_in & 32'hfff80001; + assign c = c_in & 32'hfff80001; +`else + (* anyconst *) reg [31:0] a, b, c; +`endif + (* anyseq *) reg [4:0] rm; reg [31:0] o; reg NV, DZ, OF, UF, NX; @@ -65,9 +89,14 @@ module edges(); wire o_norm = o_exp > 8'h00 && !o_special; wire o_subnorm = o_exp == 8'h00 && o_sig != '0; wire o_finite = o_norm || o_subnorm; - wire o_unclamped = o_finite && o_unsigned != 31'h7f7fffff; + wire o_clamped = o_unsigned == 31'h7f7fffff; + wire o_unclamped = o_finite && !o_clamped; wire o_ebmin = o_exp == 8'h01 && o_sig == '0; + (* keep *) wire [25:0] a_faux = {2'b10, !a_subnorm, a_sig}; + (* keep *) wire [25:0] b_faux = {2'b00, !b_subnorm, b_sig}; + (* keep *) wire [25:0] o_faux = (a_faux - b_faux); + `ifdef MULADD wire muladd_zero = c_zero; wire a_is_1 = a == 32'h3f800000; @@ -180,6 +209,93 @@ module edges(); c_sig == '0; always @* begin + // all classes of input are possible (for all inputs) + cover (a_sign); + cover (!a_sign); + cover (a_zero); + cover (a_norm); + cover (a_subnorm); + cover (a_inf); + cover (a_qnan); + cover (a_snan); + + cover (b_sign); + cover (!b_sign); + cover (b_zero); + cover (b_norm); + cover (b_subnorm); + cover (b_inf); + cover (b_qnan); + cover (b_snan); + +`ifdef MULADD + cover (c_sign); + cover (!c_sign); + cover (c_zero); + cover (c_norm); + cover (c_subnorm); + cover (c_inf); + cover (c_qnan); + cover (c_snan); +`endif + + // all flags are possible + cover (NV); +`ifdef DIV + // only div can div/zero + cover (DZ); +`endif + cover (OF); +`ifndef ADDSUB + // add/sub can't underflow + cover (UF); +`endif + cover (NX); + cover (!NV); + cover (!DZ); + cover (!OF); + cover (!UF); + cover (!NX); + + // all classes of output are possible + cover (o_sign); + cover (!o_sign); + cover (o_zero); + cover (o_norm); + cover (o_subnorm); + cover (o_inf); + cover (o_nan); + cover (o_ebmin); + + if (OF) begin + cover (o_inf); + cover (o_clamped); + end else begin + cover (o_inf); + cover (o_clamped); + end + + if (UF) begin +`ifndef ADDSUB + cover (o_zero); + cover (o_ebmin); + cover (o_subnorm); +`endif + end else begin + cover (o_zero); + cover (o_ebmin); + cover (o_subnorm); + end + + if (NX) begin + cover (o_norm); + cover (o_inf); +`ifndef ADDSUB + cover (o_subnorm); + cover (o_zero); +`endif + end + if (a_nan || b_nan || c_nan) begin // input NaN = output NaN assert (o_nan); @@ -252,6 +368,11 @@ module edges(); // an unrounded result between +-e^bmin is still an underflow when rounded to ebmin if (a_unsigned == 31'h0031b7be && b_unsigned == 31'h3ec6def9) assert (UF); + `ifdef ALT_DIV + if (!NV && !NX && !a_special && b_finite && o_norm) + // if o is subnorm then it can be shifted arbitrarily depending on exponent difference + assert (o_sig == (o_faux[25] ? o_faux[24:2] : o_faux[23:1])); + `endif `endif `ifdef MUL @@ -428,6 +549,55 @@ module edges(); if (a_sign && (a_norm || a_subnorm)) assert (NV); `endif + end + reg skip = 1; + always @(posedge clk) begin + if (skip) begin + skip <= 0; + end else begin + // same input, different rounding mode + if ($stable(a) && $stable(b) && $stable(c)) begin + // inf edge cases + cover ($rose(o_inf)); + if ($rose(o_inf)) begin + cover ($rose(rm_RNE)); + cover ($rose(rm_RNA)); + cover ($rose(rm_RTN)); + cover ($rose(rm_RTP)); + // rm_RTZ can never round to inf + end + +`ifndef ADDSUB + // these aren't applicable to addsub since we they rely on underflow + // ebmin edge cases + cover ($rose(o_ebmin)); + if ($rose(o_ebmin)) begin + cover ($rose(rm_RNE)); + cover ($rose(rm_RNA)); + cover ($rose(rm_RTN)); + cover ($rose(rm_RTP)); + cover ($rose(rm_RTZ)); + end + + // zero edge cases + cover ($rose(o_zero)); + if ($rose(o_zero)) begin + cover ($rose(rm_RNE)); + cover ($rose(rm_RNA)); + cover ($rose(rm_RTN)); + cover ($rose(rm_RTP)); + cover ($rose(rm_RTZ)); + end +`endif + +`ifndef DIV + cover ($rose(OF)); +`endif +`ifdef TININESS_AFTER + cover ($rose(UF)); +`endif + end + end end endmodule \ No newline at end of file diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 36db8f395..b262c26af 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -19,6 +19,7 @@ chformal -remove opt read_verilog -sv -formal $defs -D${rm} edges.sv +chformal -remove -cover chformal -lower prep -top edges -flatten sat -set-assumes -prove-asserts -verify From db676a2eaeda9f2ffe493ecb940a58a6f4d25670 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:28 +1200 Subject: [PATCH 14/41] symfpu: Add altdiv --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 3 +++ tests/symfpu/run-test.sh | 1 + 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/libs/symfpu b/libs/symfpu index 7fce38f94..04da5d228 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 7fce38f94fa0730b3010443eb9a1390c91e5fba0 +Subproject commit 04da5d2283989b51fe0ab44472cc598c9c50c83f diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 05ee59f2a..90b83ca25 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -452,6 +452,7 @@ struct SymFpuPass : public Pass { else if (op.compare("add") == 0 || op.compare("sub") == 0 || op.compare("mul") == 0 + || op.compare("altdiv") == 0 // currently undocumented || op.compare("div") == 0) inputs = 2; else if (op.compare("muladd") == 0) @@ -528,6 +529,8 @@ struct SymFpuPass : public Pass { return symfpu::sqrt_flagged(format, rounding_mode, a); else if (op.compare("muladd") == 0) return symfpu::fma_flagged(format, rounding_mode, a, b, c); + else if (op.compare("altdiv") == 0) + return symfpu::falseDivide_flagged(format, rounding_mode, a, b); else log_abort(); }; diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index b262c26af..512a0568e 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -41,5 +41,6 @@ prove_op sub "-DSUB -DADDSUB -DADDS" prove_op mul "-DMUL -DMULS" prove_op div "-DDIV" prove_op muladd "-DMULADD -DMULS -DADDS" +prove_op altdiv "-DDIV -DALTDIV" generate_mk --yosys-scripts From 91928a73299aee87d4c7db4bf0984b2344282f87 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:29 +1200 Subject: [PATCH 15/41] symfpu: Add alt2div `altdiv` but without denormalization, because as it turns out HardFloat unpacks subnorms in the same way, so lets just support both styles. --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 04da5d228..95b27d8f2 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 04da5d2283989b51fe0ab44472cc598c9c50c83f +Subproject commit 95b27d8f2f7cd965e13ca5ff33fd7b47c410b561 diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 90b83ca25..b35270bd4 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -453,6 +453,7 @@ struct SymFpuPass : public Pass { || op.compare("sub") == 0 || op.compare("mul") == 0 || op.compare("altdiv") == 0 // currently undocumented + || op.compare("alt2div") == 0 // currently undocumented || op.compare("div") == 0) inputs = 2; else if (op.compare("muladd") == 0) @@ -530,7 +531,9 @@ struct SymFpuPass : public Pass { else if (op.compare("muladd") == 0) return symfpu::fma_flagged(format, rounding_mode, a, b, c); else if (op.compare("altdiv") == 0) - return symfpu::falseDivide_flagged(format, rounding_mode, a, b); + return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(true)); + else if (op.compare("alt2div") == 0) + return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(false)); else log_abort(); }; From 9943484dbc2b73fdc32d991e6bf71abcb59b8c84 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:29 +1200 Subject: [PATCH 16/41] symfpu: Add altsqrt No denormalization here. That can be a problem for later (or not at all). --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 95b27d8f2..50cca8075 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 95b27d8f2f7cd965e13ca5ff33fd7b47c410b561 +Subproject commit 50cca80758d16bf72161d4d2eafb7b7c18ab44ba diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index b35270bd4..478bbd696 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -447,7 +447,8 @@ struct SymFpuPass : public Pass { } if (args[argidx] == "-op" && argidx+1 < args.size()) { op = args[++argidx]; - if (op.compare("sqrt") == 0) + if (op.compare("sqrt") == 0 + || op.compare("altsqrt") == 0) // currently undocumented inputs = 1; else if (op.compare("add") == 0 || op.compare("sub") == 0 @@ -534,6 +535,8 @@ struct SymFpuPass : public Pass { return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(true)); else if (op.compare("alt2div") == 0) return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(false)); + else if (op.compare("altsqrt") == 0) + return symfpu::falseSqrt_flagged(format, rounding_mode, a); else log_abort(); }; From b66c0dcc9723d430a2530487ef64641bd97b0ec1 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:29 +1200 Subject: [PATCH 17/41] tests/symfpu: Testing sqrt Coverage supports `sqrt`, including new general rounding detection instead of just inf/ebmin/zero (since they aren't possible with `sqrt`). More `sqrt` assertions, as well as the addition of `altsqrt` verification. Some adjustments of macros. --- tests/symfpu/edges.sv | 134 +++++++++++++++++++++++++++++++++------ tests/symfpu/run-test.sh | 8 ++- 2 files changed, 119 insertions(+), 23 deletions(-) diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 4b65c18f8..f4c2b5a72 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -48,6 +48,9 @@ module edges(input clk); wire a_subnorm = a_exp == 8'h00 && a_sig != '0; wire a_finite = a_norm || a_subnorm; + wire signed [8:0] a_sexp = $signed({1'b0, a_exp}) - 8'h7f; + wire signed [8:0] half_a_sexp = a_sexp >>> 1; + wire b_sign = b[31]; wire [30:0] b_unsigned = b[30:0]; wire [7:0] b_exp = b[30:23]; @@ -93,6 +96,8 @@ module edges(input clk); wire o_unclamped = o_finite && !o_clamped; wire o_ebmin = o_exp == 8'h01 && o_sig == '0; + wire signed [8:0] o_sexp = $signed({1'b0, o_exp}) - 8'h7f; + (* keep *) wire [25:0] a_faux = {2'b10, !a_subnorm, a_sig}; (* keep *) wire [25:0] b_faux = {2'b00, !b_subnorm, b_sig}; (* keep *) wire [25:0] o_faux = (a_faux - b_faux); @@ -219,6 +224,8 @@ module edges(input clk); cover (a_qnan); cover (a_snan); +`ifndef SQRTS +// sqrt has no b input cover (b_sign); cover (!b_sign); cover (b_zero); @@ -227,8 +234,10 @@ module edges(input clk); cover (b_inf); cover (b_qnan); cover (b_snan); +`endif `ifdef MULADD +// only muladd has c input cover (c_sign); cover (!c_sign); cover (c_zero); @@ -241,14 +250,17 @@ module edges(input clk); // all flags are possible cover (NV); -`ifdef DIV - // only div can div/zero +`ifdef DIVS +// only div can div/zero cover (DZ); `endif +`ifndef SQRTS +// sqrt can't overflow or underflow cover (OF); -`ifndef ADDSUB - // add/sub can't underflow + `ifndef ADDSUB + // add/sub can't underflow cover (UF); + `endif `endif cover (NX); cover (!NV); @@ -262,11 +274,15 @@ module edges(input clk); cover (!o_sign); cover (o_zero); cover (o_norm); - cover (o_subnorm); cover (o_inf); cover (o_nan); +`ifndef SQRTS +// subnormal outputs not possible for 8/24 sqrt + cover (o_subnorm); cover (o_ebmin); +`endif +`ifndef SQRTS if (OF) begin cover (o_inf); cover (o_clamped); @@ -276,11 +292,11 @@ module edges(input clk); end if (UF) begin -`ifndef ADDSUB + `ifndef ADDSUB cover (o_zero); cover (o_ebmin); cover (o_subnorm); -`endif + `endif end else begin cover (o_zero); cover (o_ebmin); @@ -290,11 +306,12 @@ module edges(input clk); if (NX) begin cover (o_norm); cover (o_inf); -`ifndef ADDSUB + `ifndef ADDSUB cover (o_subnorm); cover (o_zero); -`endif + `endif end +`endif if (a_nan || b_nan || c_nan) begin // input NaN = output NaN @@ -343,7 +360,7 @@ module edges(input clk); // a non-underflowing subnormal is exact assert (!NX); -`ifdef DIV +`ifdef DIVS assume (c_zero); // div/zero only when a is finite assert (DZ ^~ (a_finite && b_zero)); @@ -368,7 +385,7 @@ module edges(input clk); // an unrounded result between +-e^bmin is still an underflow when rounded to ebmin if (a_unsigned == 31'h0031b7be && b_unsigned == 31'h3ec6def9) assert (UF); - `ifdef ALT_DIV + `ifdef ALTDIV if (!NV && !NX && !a_special && b_finite && o_norm) // if o is subnorm then it can be shifted arbitrarily depending on exponent difference assert (o_sig == (o_faux[25] ? o_faux[24:2] : o_faux[23:1])); @@ -542,12 +559,51 @@ module edges(input clk); end `endif -`ifdef SQRT +`ifdef SQRTS assume (b_zero); assume (c_zero); + assert (!UF); + assert (!OF); // complex roots are invalid - if (a_sign && (a_norm || a_subnorm)) - assert (NV); + if (a_sign) begin + if (a_norm || a_subnorm) + assert (NV); + end else begin + // root exponents for normal numbers are trivial + if (a_norm) begin + // root of a normal is always normal + assert (o_norm); + if (rm_RTZ) + assert (o_sexp == half_a_sexp); + else + assert (o_sexp == half_a_sexp || o_sexp == (half_a_sexp + 1)); + `ifdef ALTSQRT + if (o_sexp == half_a_sexp) begin + if (NX) begin + assert (a_sig[0] == 1'b1); + if (rm_RTZ || rm_RTN) begin + assert (o_sig[22] == 1'b1); + assert (o_sig[21:0] == a_sig >> 1); + end else begin + assert (o_sig[22] != &a_sig); + if (rm_RNE && a_sig[1] == 1'b0) begin + assert (o_sig[21:0] == a_sig >> 1); + end else begin + assert (o_sig[21:0] == (a_sig[22:1]+1'b1)); + end + end + end else begin + assert (a_sig[0] == 1'b0); + assert (o_sig[22] == a_sig[0]); + assert (o_sig[21:0] == a_sig >> 1); + end + end + `endif + end else if (a_subnorm) begin + // root of a subnormal is either normal or an exact subnormal + assert (o_norm || !NX); + end + end `endif end @@ -558,6 +614,43 @@ module edges(input clk); end else begin // same input, different rounding mode if ($stable(a) && $stable(b) && $stable(c)) begin + // general rounding + cover (NX && rm_RNE && o_sig[1:0] == 2'b00); + cover (NX && rm_RNE && o_sig[1:0] == 2'b10); + if (NX && $fell(rm_RNE)) begin + if ($past(o_sig[1:0]) == 2'b00) begin // should be rounding from 001 + if (o_sign) begin +`ifndef SQRTS + cover ($rose(rm_RNA) && o_sig[1:0] == 2'b01); + cover ($rose(rm_RTP) && o_sig[1:0] == 2'b00); + cover ($rose(rm_RTN) && o_sig[1:0] == 2'b01); + cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b00); +`endif + end else begin + cover ($rose(rm_RNA) && o_sig[1:0] == 2'b01); + cover ($rose(rm_RTP) && o_sig[1:0] == 2'b01); + cover ($rose(rm_RTN) && o_sig[1:0] == 2'b00); + cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b00); + end + end else if ($past(o_sig[1:0]) == 2'b10) begin // should be rounding from 011 + if (o_sign) begin +`ifndef SQRTS + cover ($rose(rm_RNA) && o_sig[1:0] == 2'b10); + cover ($rose(rm_RTP) && o_sig[1:0] == 2'b01); + cover ($rose(rm_RTN) && o_sig[1:0] == 2'b10); + cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b01); +`endif + end else begin + cover ($rose(rm_RNA) && o_sig[1:0] == 2'b10); + cover ($rose(rm_RTP) && o_sig[1:0] == 2'b10); + cover ($rose(rm_RTN) && o_sig[1:0] == 2'b01); + cover ($rose(rm_RTZ) && o_sig[1:0] == 2'b01); + end + end + end + +`ifndef SQRTS +// none of these are applicable for sqrt since we can't underflow or overflow // inf edge cases cover ($rose(o_inf)); if ($rose(o_inf)) begin @@ -568,8 +661,8 @@ module edges(input clk); // rm_RTZ can never round to inf end -`ifndef ADDSUB - // these aren't applicable to addsub since we they rely on underflow + `ifndef ADDSUB + // these aren't applicable to addsub since we they rely on underflow // ebmin edge cases cover ($rose(o_ebmin)); if ($rose(o_ebmin)) begin @@ -589,13 +682,14 @@ module edges(input clk); cover ($rose(rm_RTP)); cover ($rose(rm_RTZ)); end -`endif + `endif -`ifndef DIV + `ifndef DIV cover ($rose(OF)); -`endif -`ifdef TININESS_AFTER + `endif + `ifdef TININESS_AFTER cover ($rose(UF)); + `endif `endif end end diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 512a0568e..42832da38 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -35,12 +35,14 @@ prove_op() { done } -prove_op sqrt "-DSQRT" +prove_op sqrt "-DSQRT -DSQRTS" prove_op add "-DADD -DADDSUB -DADDS" prove_op sub "-DSUB -DADDSUB -DADDS" prove_op mul "-DMUL -DMULS" -prove_op div "-DDIV" +prove_op div "-DDIV -DDIVS" prove_op muladd "-DMULADD -DMULS -DADDS" -prove_op altdiv "-DDIV -DALTDIV" + +prove_op altdiv "-DALTDIV -DDIVS" +prove_op altsqrt "-DALTSQRT -DSQRTS" generate_mk --yosys-scripts From 4134436a9fc4cbd86f6bff7a667117f916335083 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:29 +1200 Subject: [PATCH 18/41] tests/symfpu: Extra muladd tests Switch inputs back to `anyseq`, and add coverage for muladd with constant multiplier output and varying addend (also an assertion). Use an `ifdef` to control clocked properties (because of the assertion, it's no longer just covers that are clocked). --- tests/symfpu/edges.sv | 34 ++++++++++++++++++++++++++++++---- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index f4c2b5a72..fd2170991 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -1,13 +1,13 @@ module edges(input clk); `ifdef MASK - (* anyconst *) reg [31:0] a_in, b_in, c_in; + (* anyseq *) reg [31:0] a_in, b_in, c_in; wire [31:0] a, b, c; assign a = a_in & 32'hffc42108; assign b = b_in & 32'hfff80001; assign c = c_in & 32'hfff80001; `elsif MAP - (* anyconst *) reg [31:0] a_pre, b_pre, c_pre; + (* anyseq *) reg [31:0] a_pre, b_pre, c_pre; wire [31:0] a_in, b_in, c_in; // assuming 8/24 assign a_in[31:22] = a_pre[31:22]; @@ -21,7 +21,7 @@ module edges(input clk); assign b = b_in & 32'hfff80001; assign c = c_in & 32'hfff80001; `else - (* anyconst *) reg [31:0] a, b, c; + (* anyseq *) reg [31:0] a, b, c; `endif (* anyseq *) reg [4:0] rm; @@ -607,6 +607,7 @@ module edges(input clk); `endif end +`ifdef EDGE_EVENTS reg skip = 1; always @(posedge clk) begin if (skip) begin @@ -690,8 +691,33 @@ module edges(input clk); `ifdef TININESS_AFTER cover ($rose(UF)); `endif +`endif +`ifdef MULADD + // same multiplier output, different addend + end else if ($stable(a) && $stable(b) && $stable(rm)) begin + // we can get boundary cases + cover ($rose(o_inf)); + cover ($rose(o_ebmin)); + cover ($rose(o_zero)); + + // multiplication with an exception can be recovered by addend + if ($fell(c_zero)) begin + cover ($fell(OF)); + cover ($fell(UF)); + cover ($fell(NX)); + // unless it was an invalid multiplication + if ($past(NV)) + assert (NV); + end + + // flags are always determined after addition + cover ($rose(OF)); + cover ($rose(UF)); + cover ($rose(NV)); + cover ($rose(NX)); `endif end end end -endmodule \ No newline at end of file +`endif +endmodule From 16f6e8dc6aaeb974683ca87209bf21ed30fd5fcd Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:30 +1200 Subject: [PATCH 19/41] Add symfpu -classify Add description text for standard `symfpu` signature. --- passes/cmds/symfpu.cc | 178 +++++++++++++++++++++++++----------------- 1 file changed, 108 insertions(+), 70 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 478bbd696..b016413b6 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -29,6 +29,7 @@ #include "libs/symfpu/core/packing.h" #include "libs/symfpu/core/sqrt.h" #include "libs/symfpu/core/unpackedFloat.h" +#include "libs/symfpu/core/classify.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -391,9 +392,17 @@ struct SymFpuPass : public Pass { auto content_root = help->get_root(); - content_root->usage("symfpu [options]"); - content_root->paragraph("TODO"); + content_root->usage("symfpu [size] [-op ] [-rm ]"); + content_root->paragraph( + "Generates netlist for given floating point operation with floating point inputs" + "a, b, c, floating point output o, 5-bit input rm (rounding mode), and " + "5 single-bit outputs NV (invalid operation), DZ (divide by zero), OF (overflow), " + "UF (underflow), and NX (inexact)." + ); + content_root->paragraph( + "Operations use single precision float unless [size] options are provided:" + ); content_root->option("-eb ", "use bits for exponent; default=8"); content_root->option("-sb ", "use bits for significand, including hidden bit; default=24"); @@ -425,6 +434,13 @@ struct SymFpuPass : public Pass { ); rm_option->paragraph("Note: when not using DYN mode, the 'rm' input is ignored."); + content_root->usage("symfpu -classify [size]"); + content_root->paragraph( + "Generates netlist for floating point classification of input a. Outputs " + "8 single-bit signals, isNormal, isSubnormal, isZero, isInfinite, isNaN, " + "isPositive, isNegative, and isFinite." + ); + return true; } void execute(std::vector args, RTLIL::Design *design) override @@ -433,6 +449,7 @@ struct SymFpuPass : public Pass { int eb = 8, sb = 24; string op = "mul", rounding = "DYN"; int inputs = 2; + bool classify = false; log_header(design, "Executing SYMFPU pass.\n"); size_t argidx; @@ -468,11 +485,22 @@ struct SymFpuPass : public Pass { rounding = args[++argidx]; continue; } + if (args[argidx] == "-classify") { + classify = true; + continue; + } break; } extra_args(args, argidx, design); + if (classify) { + if (rounding.compare("DYN") != 0) + log_cmd_error("symfpu -classify does not support rounding modes.\n"); + if (op.compare("mul") != 0) + log_cmd_error("symfpu -classify does not support operator selection.\n"); + } + rm rounding_mode; if (rounding.compare("RNE") == 0) rounding_mode = rtlil_traits::RNE(); @@ -496,80 +524,90 @@ struct SymFpuPass : public Pass { symfpu_mod = mod; auto a_bv = input_ubv(ID(a), eb+sb); - auto b_bv = input_ubv(ID(b), eb+sb); - auto c_bv = input_ubv(ID(c), eb+sb); - uf a = symfpu::unpack(format, a_bv); - uf b = symfpu::unpack(format, b_bv); - uf c = symfpu::unpack(format, c_bv); - auto rm_wire = symfpu_mod->addWire(ID(rm), 5); - rm_wire->port_input = true; - SigSpec rm_sig(rm_wire); - prop rm_RNE(rm_sig[0]); - prop rm_RNA(rm_sig[1]); - prop rm_RTP(rm_sig[2]); - prop rm_RTN(rm_sig[3]); - prop rm_RTZ(rm_sig[4]); + if (classify) { + output_prop(ID(isNormal), symfpu::isNormal(format, a)); + output_prop(ID(isSubnormal), symfpu::isSubnormal(format, a)); + output_prop(ID(isZero), symfpu::isZero(format, a)); + output_prop(ID(isInfinite), symfpu::isInfinite(format, a)); + output_prop(ID(isNaN), symfpu::isNaN(format, a)); + output_prop(ID(isPositive), symfpu::isPositive(format, a)); + output_prop(ID(isNegative), symfpu::isNegative(format, a)); + output_prop(ID(isFinite), symfpu::isFinite(format, a)); + } else { + auto b_bv = input_ubv(ID(b), eb+sb); + auto c_bv = input_ubv(ID(c), eb+sb); + uf b = symfpu::unpack(format, b_bv); + uf c = symfpu::unpack(format, c_bv); - // signaling NaN inputs raise NV - prop signals_invalid((a.getNaN() && is_sNaN(a_bv, sb)) - || (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2) - || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) - ); + auto rm_wire = symfpu_mod->addWire(ID(rm), 5); + rm_wire->port_input = true; + SigSpec rm_sig(rm_wire); + prop rm_RNE(rm_sig[0]); + prop rm_RNA(rm_sig[1]); + prop rm_RTP(rm_sig[2]); + prop rm_RTN(rm_sig[3]); + prop rm_RTZ(rm_sig[4]); - auto make_op = [&op, &format, &a, &b, &c](rm rounding_mode) { - if (op.compare("add") == 0) - return symfpu::add_flagged(format, rounding_mode, a, b, prop(true)); - else if (op.compare("sub") == 0) - return symfpu::add_flagged(format, rounding_mode, a, b, prop(false)); - else if (op.compare("mul") == 0) - return symfpu::multiply_flagged(format, rounding_mode, a, b); - else if (op.compare("div") == 0) - return symfpu::divide_flagged(format, rounding_mode, a, b); - else if (op.compare("sqrt") == 0) - return symfpu::sqrt_flagged(format, rounding_mode, a); - else if (op.compare("muladd") == 0) - return symfpu::fma_flagged(format, rounding_mode, a, b, c); - else if (op.compare("altdiv") == 0) - return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(true)); - else if (op.compare("alt2div") == 0) - return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(false)); - else if (op.compare("altsqrt") == 0) - return symfpu::falseSqrt_flagged(format, rounding_mode, a); - else - log_abort(); - }; - - // calling this more than once will fail - auto output_fpu = [&signals_invalid, &format](const uf_flagged &o_flagged) { - output_prop(ID(NV), o_flagged.nv || signals_invalid); - output_prop(ID(DZ), o_flagged.dz); - output_prop(ID(OF), o_flagged.of); - output_prop(ID(UF), o_flagged.uf); - output_prop(ID(NX), o_flagged.nx); - - output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); - }; - - if (rounding.compare("DYN") != 0) - output_fpu(make_op(rounding_mode)); - else { - auto out_RNE = make_op(rtlil_traits::RNE()); - auto out_RNA = make_op(rtlil_traits::RNA()); - auto out_RTP = make_op(rtlil_traits::RTP()); - auto out_RTN = make_op(rtlil_traits::RTN()); - auto out_RTZ = make_op(rtlil_traits::RTZ()); - output_fpu( - uf_flagged_ite::iteOp(rm_RNE, out_RNE, - uf_flagged_ite::iteOp(rm_RNA, out_RNA, - uf_flagged_ite::iteOp(rm_RTP, out_RTP, - uf_flagged_ite::iteOp(rm_RTN, out_RTN, - uf_flagged_ite::iteOp(rm_RTZ, out_RTZ, - uf_flagged::makeNaN(format, prop(true))))))) + // signaling NaN inputs raise NV + prop signals_invalid((a.getNaN() && is_sNaN(a_bv, sb)) + || (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2) + || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) ); + + auto make_op = [&op, &format, &a, &b, &c](rm rounding_mode) { + if (op.compare("add") == 0) + return symfpu::add_flagged(format, rounding_mode, a, b, prop(true)); + else if (op.compare("sub") == 0) + return symfpu::add_flagged(format, rounding_mode, a, b, prop(false)); + else if (op.compare("mul") == 0) + return symfpu::multiply_flagged(format, rounding_mode, a, b); + else if (op.compare("div") == 0) + return symfpu::divide_flagged(format, rounding_mode, a, b); + else if (op.compare("sqrt") == 0) + return symfpu::sqrt_flagged(format, rounding_mode, a); + else if (op.compare("muladd") == 0) + return symfpu::fma_flagged(format, rounding_mode, a, b, c); + else if (op.compare("altdiv") == 0) + return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(true)); + else if (op.compare("alt2div") == 0) + return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(false)); + else if (op.compare("altsqrt") == 0) + return symfpu::falseSqrt_flagged(format, rounding_mode, a); + else + log_abort(); + }; + + // calling this more than once will fail + auto output_fpu = [&signals_invalid, &format](const uf_flagged &o_flagged) { + output_prop(ID(NV), o_flagged.nv || signals_invalid); + output_prop(ID(DZ), o_flagged.dz); + output_prop(ID(OF), o_flagged.of); + output_prop(ID(UF), o_flagged.uf); + output_prop(ID(NX), o_flagged.nx); + + output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); + }; + + if (rounding.compare("DYN") != 0) + output_fpu(make_op(rounding_mode)); + else { + auto out_RNE = make_op(rtlil_traits::RNE()); + auto out_RNA = make_op(rtlil_traits::RNA()); + auto out_RTP = make_op(rtlil_traits::RTP()); + auto out_RTN = make_op(rtlil_traits::RTN()); + auto out_RTZ = make_op(rtlil_traits::RTZ()); + output_fpu( + uf_flagged_ite::iteOp(rm_RNE, out_RNE, + uf_flagged_ite::iteOp(rm_RNA, out_RNA, + uf_flagged_ite::iteOp(rm_RTP, out_RTP, + uf_flagged_ite::iteOp(rm_RTN, out_RTN, + uf_flagged_ite::iteOp(rm_RTZ, out_RTZ, + uf_flagged::makeNaN(format, prop(true))))))) + ); + } } - symfpu_mod->fixup_ports(); } From 7a6b36b670a752faf7177cc2575337a56dc590ec Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:30 +1200 Subject: [PATCH 20/41] symfpu: Add -compare mode Also `min` and `max` ops. RISC-V uses IEEE 754-2019 semantics where `min(+0,-0) == -0` and `max(+0,-0) == +0` so we do the same here. We could make it optional, but as I understand it the newer behavior is still backwards compatible (since previously it was valid to have selected either). --- passes/cmds/symfpu.cc | 50 +++++++++++++++++++++++++++++++++++++++---- 1 file changed, 46 insertions(+), 4 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index b016413b6..fa2860135 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -30,6 +30,7 @@ #include "libs/symfpu/core/sqrt.h" #include "libs/symfpu/core/unpackedFloat.h" #include "libs/symfpu/core/classify.h" +#include "libs/symfpu/core/compare.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -417,6 +418,8 @@ struct SymFpuPass : public Pass { "sub | two input subtraction | o = a-b\n" "mul | two input multiplication | o = a*b\n" "div | two input divison | o = a/b\n" + "min | two input minimum | o = min(a,b)\n" + "max | two input maximum | o = max(a,b)\n" "muladd | three input fused multiple-add | o = (a*b)+c\n" ); @@ -441,6 +444,13 @@ struct SymFpuPass : public Pass { "isPositive, isNegative, and isFinite." ); + content_root->usage("symfpu -compare [size]"); + content_root->paragraph( + "Generates netlist for floating point comparison of inputs a and b. Outputs " + "6 single-bit signals, smtlibEqual, ieee754Equal, lessThan, lessThanOrEqual, " + "sNV (invalid signaling comparison), and qNV (invalid quiet comparison)." + ); + return true; } void execute(std::vector args, RTLIL::Design *design) override @@ -449,7 +459,7 @@ struct SymFpuPass : public Pass { int eb = 8, sb = 24; string op = "mul", rounding = "DYN"; int inputs = 2; - bool classify = false; + bool classify = false, compare = false; log_header(design, "Executing SYMFPU pass.\n"); size_t argidx; @@ -472,6 +482,8 @@ struct SymFpuPass : public Pass { || op.compare("mul") == 0 || op.compare("altdiv") == 0 // currently undocumented || op.compare("alt2div") == 0 // currently undocumented + || op.compare("min") == 0 + || op.compare("max") == 0 || op.compare("div") == 0) inputs = 2; else if (op.compare("muladd") == 0) @@ -489,15 +501,31 @@ struct SymFpuPass : public Pass { classify = true; continue; } + if (args[argidx] == "-compare") { + compare = true; + continue; + } break; } extra_args(args, argidx, design); - if (classify) { - if (rounding.compare("DYN") != 0) + if (compare && classify) + log_cmd_error("-classify and -compare flags are incompatible.\n"); + + if (rounding.compare("DYN") != 0) { + if (compare) + log_cmd_error("symfpu -compare does not support rounding modes.\n"); + if (classify) log_cmd_error("symfpu -classify does not support rounding modes.\n"); - if (op.compare("mul") != 0) + if (op.compare("min") == 0 || op.compare("max") == 0) + log_cmd_error("min/max operations do not support rounding modes.\n"); + } + + if (op.compare("mul") != 0) { + if (compare) + log_cmd_error("symfpu -compare does not support operator selection.\n"); + if (classify) log_cmd_error("symfpu -classify does not support operator selection.\n"); } @@ -535,6 +563,15 @@ struct SymFpuPass : public Pass { output_prop(ID(isPositive), symfpu::isPositive(format, a)); output_prop(ID(isNegative), symfpu::isNegative(format, a)); output_prop(ID(isFinite), symfpu::isFinite(format, a)); + } else if (compare) { + auto b_bv = input_ubv(ID(b), eb+sb); + uf b = symfpu::unpack(format, b_bv); + output_prop(ID(smtlibEqual), symfpu::smtlibEqual(format, a, b)); + output_prop(ID(ieee754Equal), symfpu::ieee754Equal(format, a, b)); + output_prop(ID(lessThan), symfpu::lessThan(format, a, b)); + output_prop(ID(lessThanOrEqual), symfpu::lessThanOrEqual(format, a, b)); + output_prop(ID(sNV), a.getNaN() || b.getNaN()); + output_prop(ID(qNV), (a.getNaN() && is_sNaN(a_bv, sb)) || (b.getNaN() && is_sNaN(b_bv, sb))); } else { auto b_bv = input_ubv(ID(b), eb+sb); auto c_bv = input_ubv(ID(c), eb+sb); @@ -575,6 +612,11 @@ struct SymFpuPass : public Pass { return symfpu::falseDivide_flagged(format, rounding_mode, a, b, prop(false)); else if (op.compare("altsqrt") == 0) return symfpu::falseSqrt_flagged(format, rounding_mode, a); + else if (op.compare("min") == 0) + // setting zeroCase=a.getSign() makes +0 > -0, as per IEEE 754-2019 + return uf_flagged(symfpu::min(format, a, b, a.getSign())); + else if (op.compare("max") == 0) + return uf_flagged(symfpu::max(format, a, b, a.getSign())); else log_abort(); }; From 613d95b90959ac37fd5613c9fa6ece438b0e93fc Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:30 +1200 Subject: [PATCH 21/41] symfpu: Test comparisons --- tests/symfpu/edges.sv | 91 +++++++++++++++++++++++++++++++++------- tests/symfpu/run-test.sh | 11 +++++ 2 files changed, 87 insertions(+), 15 deletions(-) diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index fd2170991..adcfc9e19 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -202,6 +202,12 @@ module edges(input clk); assign rounded_000 = '0; `endif +`ifdef MAX + wire choose_max = 1; +`else + wire choose_max = 0; +`endif + wire rm_RNE = rm[0] == 1'b1; wire rm_RNA = rm[1:0] == 2'b10; wire rm_RTP = rm[2:0] == 3'b100; @@ -250,19 +256,21 @@ module edges(input clk); // all flags are possible cover (NV); -`ifdef DIVS -// only div can div/zero +`ifndef COMPARES + `ifdef DIVS + // only div can div/zero cover (DZ); -`endif -`ifndef SQRTS -// sqrt can't overflow or underflow - cover (OF); - `ifndef ADDSUB - // add/sub can't underflow - cover (UF); `endif -`endif + `ifndef SQRTS + // sqrt can't overflow or underflow + cover (OF); + `ifndef ADDSUB + // add/sub can't underflow + cover (UF); + `endif + `endif cover (NX); +`endif cover (!NV); cover (!DZ); cover (!OF); @@ -282,6 +290,7 @@ module edges(input clk); cover (o_ebmin); `endif +`ifndef COMPARES `ifndef SQRTS if (OF) begin cover (o_inf); @@ -324,7 +333,12 @@ module edges(input clk); assert (!NX); end - if (a_snan) + if (NV) + // output = qNaN + assert (o_qnan); +`endif // !COMPARES + + if (a_snan || b_snan) // signalling NaN raises invalid exception assert (NV); @@ -336,10 +350,6 @@ module edges(input clk); // output = +-inf assert (o_inf); - if (NV) - // output = qNaN - assert (o_qnan); - if (OF) // overflow is always inexact assert (NX); @@ -360,6 +370,57 @@ module edges(input clk); // a non-underflowing subnormal is exact assert (!NX); +`ifdef COMPARES + assume (c_zero); + assert (!OF); + assert (!UF); + assert (!NX); + assert (!DZ); + + if (!a_nan && b_nan) + assert (o == a); + else if (a_nan && !b_nan) + assert (o == b); + else if (a_nan && b_nan) + assert (o_nan); + else begin + assert (o == a || o == b); + + if (a_inf) begin + if (a_sign == choose_max) + assert (o == b); + else + assert (o == a); + end + + if (b_inf) begin + if (b_sign == choose_max) + assert (o == a); + else + assert (o == b); + end + end + + if (!a_special && !b_special) begin + if (a_sign != b_sign) + if (a_sign == choose_max) + assert (o == b); + else + assert (o == a); + // a_sign == b_sign + else if (a_exp != b_exp) + if ((a_exp > b_exp) ^ a_sign ^ choose_max) + assert (o == b); + else + assert (o == a); + // a_exp == b_exp + else if ((a_sig > b_sig) ^ a_sign ^ choose_max) + assert (o == b); + else + assert (o == a); + end +`endif + `ifdef DIVS assume (c_zero); // div/zero only when a is finite diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 42832da38..005f0cbc7 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -35,6 +35,14 @@ prove_op() { done } +prove_op_unrounded() { + # DYN is default rounding mode, so this is (currently) equivalent to no rounding mode + # but this does skip verifying the built in asserts + op=$1 + defs=$2 + prove_rm $op "DYN" "$defs" +} + prove_op sqrt "-DSQRT -DSQRTS" prove_op add "-DADD -DADDSUB -DADDS" prove_op sub "-DSUB -DADDSUB -DADDS" @@ -45,4 +53,7 @@ prove_op muladd "-DMULADD -DMULS -DADDS" prove_op altdiv "-DALTDIV -DDIVS" prove_op altsqrt "-DALTSQRT -DSQRTS" +prove_op_unrounded min "-DMIN -DCOMPARES" +prove_op_unrounded max "-DMAX -DCOMPARES" + generate_mk --yosys-scripts From dfec87e6a30559710a3f4d00f099c7b5c8b7715f Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:31 +1200 Subject: [PATCH 22/41] symfpu: Add symfpu_convert Convert one input to three outputs (int -> float, float -> int, float -> float). No rounding mode, no flags (yet). --- passes/cmds/symfpu.cc | 147 +++++++++++++++++++++++++++++++++++++----- 1 file changed, 131 insertions(+), 16 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index fa2860135..e51643aea 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -74,6 +74,23 @@ struct rtlil_traits { static void setflag(const string &name, const prop &p); }; +rm parse_rounding(std::string rounding) { + if (rounding.compare("RNE") == 0) + return rtlil_traits::RNE(); + else if (rounding.compare("RNA") == 0) + return rtlil_traits::RNA(); + else if (rounding.compare("RTP") == 0) + return rtlil_traits::RTP(); + else if (rounding.compare("RTN") == 0) + return rtlil_traits::RTN(); + else if (rounding.compare("RTZ") == 0) + return rtlil_traits::RTZ(); + else if (rounding.compare("DYN") == 0) + return {}; + else + log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding); +} + using bwt = rtlil_traits::bwt; using fpt = rtlil_traits::fpt; using ubv = rtlil_traits::ubv; @@ -529,22 +546,7 @@ struct SymFpuPass : public Pass { log_cmd_error("symfpu -classify does not support operator selection.\n"); } - rm rounding_mode; - if (rounding.compare("RNE") == 0) - rounding_mode = rtlil_traits::RNE(); - else if (rounding.compare("RNA") == 0) - rounding_mode = rtlil_traits::RNA(); - else if (rounding.compare("RTP") == 0) - rounding_mode = rtlil_traits::RTP(); - else if (rounding.compare("RTN") == 0) - rounding_mode = rtlil_traits::RTN(); - else if (rounding.compare("RTZ") == 0) - rounding_mode = rtlil_traits::RTZ(); - else if (rounding.compare("DYN") == 0) - rounding_mode = {}; - else - log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding); - + rm rounding_mode = parse_rounding(rounding); fpt format(eb, sb); auto mod = design->addModule(ID(symfpu)); @@ -655,4 +657,117 @@ struct SymFpuPass : public Pass { } } SymFpuPass; + +struct SymFpuConvertPass : public Pass { + SymFpuConvertPass() : Pass("symfpu_convert", "SymFPU based floating point conversion netlist generator") {} + bool formatted_help() override + { + auto *help = PrettyHelp::get_current(); + help->set_group("formal"); + + auto content_root = help->get_root(); + + content_root->usage("symfpu_convert [-rm ]"); + content_root->paragraph( + "Generates netlist for converting given input size to given output size. " + "Generated module has one input `i`, and three outputs, `o_if`, `o_fi`, and `o_ff`, " + "performing int -> float, float -> int, and float -> float conversions respectively. " + ); + + content_root->option("-isize ", "input port is bits wide; default=32"); + content_root->option("-osize ", "output ports are bits wide; default=32"); + content_root->option("-iexp ", "input port uses bits for exponent; default=8"); + content_root->option("-oexp ", "output ports use bits for exponent; default=8"); + + content_root->paragraph( + " bits of exponent implies bits of significand (including hidden bit), " + "e.g. the default is single precision float with N=32 and M=8 (and 24 bits of significand). " + ); + + auto rm_option = content_root->open_option("-rm "); + rm_option->paragraph("rounding mode to generate, must be one of the below; default=DYN"); + rm_option->codeblock( + " | rm | description\n" + "-----+--------+----------------------\n" + "RNE | 00001 | round ties to even\n" + "RNA | 00010 | round ties to away\n" + "RTP | 00100 | round toward positive\n" + "RTN | 01000 | round toward negative\n" + "RTZ | 10000 | round toward zero\n" + "DYN | xxxxx | round based on 'rm' input signal\n" + ); + rm_option->paragraph("Note: when not using DYN mode, the 'rm' input is ignored."); + + return true; + } + void execute(std::vector args, RTLIL::Design *design) override + { + //TODO: fix multiple calls to symfpu in single Yosys instance + //TODO: signed integers + int i_size = 32, o_size = 32, i_exp = 8, o_exp = 8; + string rounding = "DYN"; + log_header(design, "Executing SYMFPU_CONVERT pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) { + // all args take a value + if (argidx+1 >= args.size()) + break; + if (args[argidx] == "-isize") { + i_size = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-osize") { + o_size = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-iexp") { + i_exp = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-oexp") { + o_exp = atoi(args[++argidx].c_str()); + continue; + } + if (args[argidx] == "-rm") { + rounding = args[++argidx]; + continue; + } + break; + } + + extra_args(args, argidx, design); + + if (o_exp >= o_size || o_exp <= 0) + log_cmd_error("-oexp value (%d) must be in range: 0 < oM < oN (oN=%d)!\n", o_exp, o_size); + if (i_exp >= i_size || i_exp <= 0) + log_cmd_error("-iexp value (%d) must be in range: 0 < iM < iN (iN=%d)!\n", i_exp, i_size); + + if (rounding.compare("DYN") == 0) + log_cmd_error("rm must be set to a single rounding mode!\n"); + rm rounding_mode = parse_rounding(rounding); + + auto mod = design->addModule(ID(symfpu)); + symfpu_mod = mod; + + fpt i_format(i_exp, i_size-i_exp); + fpt o_format(o_exp, o_size-o_exp); + + auto i_bv = input_ubv(ID(i), i_size); + uf i_f = symfpu::unpack(i_format, i_bv); + + uf o_ff = symfpu::convertFloatToFloat(i_format, o_format, rounding_mode, i_f); + output_ubv(ID(o_ff), symfpu::pack(o_format, o_ff)); + + ubv o_default = symfpu::ITE(i_f.getSign(), ubv::zero(o_size), ubv::allOnes(o_size)); + ubv o_fi = symfpu::convertFloatToUBV(i_format, rounding_mode, i_f, o_size, o_default); + output_ubv(ID(o_fi), o_fi); + + uf o_if = symfpu::convertUBVToFloat(o_format, rounding_mode, i_bv); + output_ubv(ID(o_if), symfpu::pack(o_format, o_if)); + + symfpu_mod->fixup_ports(); + } +} SymFpuConvertPass; + PRIVATE_NAMESPACE_END From 675087937f66c92ab4f9b686d3aa52c490966db0 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:31 +1200 Subject: [PATCH 23/41] symfpu: Convert with flags --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 23 +++++++++++++++++------ 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 50cca8075..423911dc2 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 50cca80758d16bf72161d4d2eafb7b7c18ab44ba +Subproject commit 423911dc2022418d80a5aadd3ea3a876b352c9fc diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index e51643aea..33d91cc6a 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -99,6 +99,7 @@ using symfpu::ite; using uf = symfpu::unpackedFloat; using uf_flagged = symfpu::floatWithStatusFlags; using uf_flagged_ite = symfpu::ite; +using ubv_flagged = symfpu::ubvWithStatusFlags; PRIVATE_NAMESPACE_END @@ -756,15 +757,25 @@ struct SymFpuConvertPass : public Pass { auto i_bv = input_ubv(ID(i), i_size); uf i_f = symfpu::unpack(i_format, i_bv); - uf o_ff = symfpu::convertFloatToFloat(i_format, o_format, rounding_mode, i_f); - output_ubv(ID(o_ff), symfpu::pack(o_format, o_ff)); + uf_flagged o_ff = symfpu::convertFloatToFloat_flagged(i_format, o_format, rounding_mode, i_f); + output_ubv(ID(o_ff), symfpu::pack(o_format, o_ff.val)); + prop i_sNaN(i_f.getNaN() && is_sNaN(i_bv, i_size-i_exp)); + output_prop(ID(nv_ff), o_ff.nv || i_sNaN); + output_prop(ID(of_ff), o_ff.of); + output_prop(ID(uf_ff), o_ff.uf); + output_prop(ID(nx_ff), o_ff.nx); ubv o_default = symfpu::ITE(i_f.getSign(), ubv::zero(o_size), ubv::allOnes(o_size)); - ubv o_fi = symfpu::convertFloatToUBV(i_format, rounding_mode, i_f, o_size, o_default); - output_ubv(ID(o_fi), o_fi); + ubv_flagged o_fi = symfpu::convertFloatToUBV_flagged(i_format, rounding_mode, i_f, o_size, o_default); + output_ubv(ID(o_fi), o_fi.val); + output_prop(ID(nv_fi), o_fi.nv); + output_prop(ID(nx_fi), o_fi.nx); - uf o_if = symfpu::convertUBVToFloat(o_format, rounding_mode, i_bv); - output_ubv(ID(o_if), symfpu::pack(o_format, o_if)); + uf_flagged o_if = symfpu::convertUBVToFloat_flagged(o_format, rounding_mode, i_bv); + output_ubv(ID(o_if), symfpu::pack(o_format, o_if.val)); + output_prop(ID(nv_if), o_if.nv); + output_prop(ID(of_if), o_if.of); + output_prop(ID(nx_if), o_if.nx); symfpu_mod->fixup_ports(); } From 50c4a057b2234b0750856e465fd80cd03dbd42c9 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:31 +1200 Subject: [PATCH 24/41] symfpu: Use ubv for convert flags --- passes/cmds/symfpu.cc | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 33d91cc6a..90f2f3863 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -756,26 +756,24 @@ struct SymFpuConvertPass : public Pass { auto i_bv = input_ubv(ID(i), i_size); uf i_f = symfpu::unpack(i_format, i_bv); + prop i_sNaN(i_f.getNaN() && is_sNaN(i_bv, i_size-i_exp)); + + auto output_flags = [](IdString name, const prop &nv, const prop &nx, const prop &of = prop(false), const prop &uf = prop(false), const prop &dz = prop(false)) { + output_ubv(name, ubv{SigSpec({nv.bit, dz.bit, of.bit, uf.bit, nx.bit})}); + }; uf_flagged o_ff = symfpu::convertFloatToFloat_flagged(i_format, o_format, rounding_mode, i_f); output_ubv(ID(o_ff), symfpu::pack(o_format, o_ff.val)); - prop i_sNaN(i_f.getNaN() && is_sNaN(i_bv, i_size-i_exp)); - output_prop(ID(nv_ff), o_ff.nv || i_sNaN); - output_prop(ID(of_ff), o_ff.of); - output_prop(ID(uf_ff), o_ff.uf); - output_prop(ID(nx_ff), o_ff.nx); + output_flags(ID(flags_ff), o_ff.nv || i_sNaN, o_ff.nx, o_ff.of, o_ff.uf); ubv o_default = symfpu::ITE(i_f.getSign(), ubv::zero(o_size), ubv::allOnes(o_size)); ubv_flagged o_fi = symfpu::convertFloatToUBV_flagged(i_format, rounding_mode, i_f, o_size, o_default); output_ubv(ID(o_fi), o_fi.val); - output_prop(ID(nv_fi), o_fi.nv); - output_prop(ID(nx_fi), o_fi.nx); + output_flags(ID(flags_fi), o_fi.nv, o_fi.nx); uf_flagged o_if = symfpu::convertUBVToFloat_flagged(o_format, rounding_mode, i_bv); output_ubv(ID(o_if), symfpu::pack(o_format, o_if.val)); - output_prop(ID(nv_if), o_if.nv); - output_prop(ID(of_if), o_if.of); - output_prop(ID(nx_if), o_if.nx); + output_flags(ID(flags_if), o_if.nv, o_if.nx, o_if.of); symfpu_mod->fixup_ports(); } From 7b5d3346038d14d1bf36a8cb0fd8b2eaf9e24fa1 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:32 +1200 Subject: [PATCH 25/41] symfpu_convert: Handle signed ints Use input wire `is_signed` to select between signed and unsigned handling. --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 33 +++++++++++++++++++++++++-------- 2 files changed, 26 insertions(+), 9 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index 423911dc2..37cf1437b 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 423911dc2022418d80a5aadd3ea3a876b352c9fc +Subproject commit 37cf1437bd01176b3042b5644346f73df810ef37 diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 90f2f3863..acb33f37b 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -99,7 +99,8 @@ using symfpu::ite; using uf = symfpu::unpackedFloat; using uf_flagged = symfpu::floatWithStatusFlags; using uf_flagged_ite = symfpu::ite; -using ubv_flagged = symfpu::ubvWithStatusFlags; +using ubv_flagged = symfpu::bvWithStatusFlags; +using sbv_flagged = symfpu::bvWithStatusFlags; PRIVATE_NAMESPACE_END @@ -183,8 +184,8 @@ template struct bv { return bv{SigSpec(value)}; } - bv toSigned(void) const { return bv(*this); } - bv toUnsigned(void) const { return bv(*this); } + bv toSigned(void) const { return bv(*this); } + bv toUnsigned(void) const { return bv(*this); } bv extract(bwt upper, bwt lower) const { @@ -382,6 +383,13 @@ ubv input_ubv(IdString name, int width) return ubv(SigSpec(input)); } +prop input_prop(IdString name) +{ + auto input = symfpu_mod->addWire(name); + input->port_input = true; + return prop(SigBit(input)); +} + void output_ubv(IdString name, const ubv &value) { auto output = symfpu_mod->addWire(name, value.getWidth()); @@ -766,12 +774,21 @@ struct SymFpuConvertPass : public Pass { output_ubv(ID(o_ff), symfpu::pack(o_format, o_ff.val)); output_flags(ID(flags_ff), o_ff.nv || i_sNaN, o_ff.nx, o_ff.of, o_ff.uf); - ubv o_default = symfpu::ITE(i_f.getSign(), ubv::zero(o_size), ubv::allOnes(o_size)); - ubv_flagged o_fi = symfpu::convertFloatToUBV_flagged(i_format, rounding_mode, i_f, o_size, o_default); - output_ubv(ID(o_fi), o_fi.val); - output_flags(ID(flags_fi), o_fi.nv, o_fi.nx); + auto is_signed = input_prop(ID(is_signed)); - uf_flagged o_if = symfpu::convertUBVToFloat_flagged(o_format, rounding_mode, i_bv); + // use riscv behavior for invalid inputs + ubv o_signed_default = symfpu::ITE(i_f.getSign(), ubv::one(1).append(ubv::zero(o_size-1)), ubv::zero(1).append(ubv::allOnes(o_size-1))); + ubv o_unsigned_default = symfpu::ITE(i_f.getSign(), ubv::zero(o_size), ubv::allOnes(o_size)); + auto o_fi_signed = symfpu::convertFloatToSBV_flagged(i_format, rounding_mode, i_f, o_size, o_signed_default); + auto o_fi_unsigned = symfpu::convertFloatToUBV_flagged(i_format, rounding_mode, i_f, o_size, o_unsigned_default); + output_ubv(ID(o_fi), symfpu::ITE(is_signed, o_fi_signed.val.toUnsigned(), o_fi_unsigned.val)); + output_flags(ID(flags_fi), + symfpu::ITE(is_signed, o_fi_signed.nv, o_fi_unsigned.nv), + symfpu::ITE(is_signed, o_fi_signed.nx, o_fi_unsigned.nx)); + + uf_flagged o_if(uf_flagged_ite::iteOp(is_signed, + symfpu::convertSBVToFloat_flagged(o_format, rounding_mode, i_bv), + symfpu::convertUBVToFloat_flagged(o_format, rounding_mode, i_bv))); output_ubv(ID(o_if), symfpu::pack(o_format, o_if.val)); output_flags(ID(flags_if), o_if.nv, o_if.nx, o_if.of); From d5b6a38f65f7e0ff46ba4380f5f9f2c760042d79 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:32 +1200 Subject: [PATCH 26/41] symfpu: Missed a space --- passes/cmds/symfpu.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index acb33f37b..923b277b4 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -421,7 +421,7 @@ struct SymFpuPass : public Pass { content_root->usage("symfpu [size] [-op ] [-rm ]"); content_root->paragraph( - "Generates netlist for given floating point operation with floating point inputs" + "Generates netlist for given floating point operation with floating point inputs " "a, b, c, floating point output o, 5-bit input rm (rounding mode), and " "5 single-bit outputs NV (invalid operation), DZ (divide by zero), OF (overflow), " "UF (underflow), and NX (inexact)." From 952d01b821696104161c21a7ac3dd89998cddc22 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:32 +1200 Subject: [PATCH 27/41] libs/symfpu: tinyAfterRounding --- libs/symfpu | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/symfpu b/libs/symfpu index 37cf1437b..e68bf9d0b 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit 37cf1437bd01176b3042b5644346f73df810ef37 +Subproject commit e68bf9d0bb2e038e970ed11c7edcc19f29d84b12 From e6bd07a49aa370efd0db8e83ce306e9c90720756 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:33 +1200 Subject: [PATCH 28/41] tests/symfpu: Switch to generate_mk.py --- tests/symfpu/generate_mk.py | 50 +++++++++++++++++++++++++++++++ tests/symfpu/run-test.sh | 59 ------------------------------------- 2 files changed, 50 insertions(+), 59 deletions(-) create mode 100644 tests/symfpu/generate_mk.py delete mode 100755 tests/symfpu/run-test.sh diff --git a/tests/symfpu/generate_mk.py b/tests/symfpu/generate_mk.py new file mode 100644 index 000000000..aacbbf391 --- /dev/null +++ b/tests/symfpu/generate_mk.py @@ -0,0 +1,50 @@ +#!/usr/bin/env python3 + +import sys +sys.path.append("..") +import gen_tests_makefile + +from pathlib import Path +from textwrap import dedent + +cwd = Path.cwd() +for path in cwd.glob("*_edges.*"): + path.unlink() + +for op, defs in { + # standard ops + "sqrt": "-DSQRT -DSQRTS", + "add": "-DADD -DADDSUB -DADDS", + "sub": "-DSUB -DADDSUB -DADDS", + "mul": "-DMUL -DMULS", + "div": "-DDIV -DDIVS", + "muladd": "-DMULADD -DMULS -DADDS", + # altops + "altdiv": "-DALTDIV -DDIVS", + "altsqrt": "-DALTSQRT -DSQRTS", + # unrounded + "min": "-DMIN -DCOMPARES", + "max": "-DMAX -DCOMPARES", +}.items(): + rms = ["DYN"] + dyn_only = op in ["min", "max"] + if not dyn_only: + rms.extend(["RNE", "RNA", "RTP", "RTN", "RTZ"]) + for rm in rms: + with open(f"{op}_{rm}_edges.ys", "w") as ys: + print(f"symfpu -op {op} -rm {rm}", file=ys) + if rm != "DYN" or dyn_only: + print("sat -prove-asserts -verify", file=ys) + print( + dedent(f"""\ + chformal -remove + opt + + read_verilog -sv -formal {defs} -D{rm} edges.sv + chformal -remove -cover + chformal -lower + prep -top edges -flatten + sat -set-assumes -prove-asserts -verify""" + ), file=ys) + +gen_tests_makefile.generate(["--yosys-scripts"]) diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh deleted file mode 100755 index 005f0cbc7..000000000 --- a/tests/symfpu/run-test.sh +++ /dev/null @@ -1,59 +0,0 @@ -#!/usr/bin/env bash -set -eu - -source ../gen-tests-makefile.sh - -rm -f *_edges.* - -prove_rm() { - op=$1 - rm=$2 - defs=$3 - ys_file=${op}_${rm}_edges.ys - echo "symfpu -op $op -rm $rm" > $ys_file - if [[ $rm != "DYN" ]] then - echo "sat -prove-asserts -verify" >> $ys_file - fi - echo """\ -chformal -remove -opt - -read_verilog -sv -formal $defs -D${rm} edges.sv -chformal -remove -cover -chformal -lower -prep -top edges -flatten -sat -set-assumes -prove-asserts -verify -""" >> $ys_file -} - -prove_op() { - op=$1 - defs=$2 - rms="RNE RNA RTP RTN RTZ DYN" - for rm in $rms; do - prove_rm $op $rm "$defs" - done -} - -prove_op_unrounded() { - # DYN is default rounding mode, so this is (currently) equivalent to no rounding mode - # but this does skip verifying the built in asserts - op=$1 - defs=$2 - prove_rm $op "DYN" "$defs" -} - -prove_op sqrt "-DSQRT -DSQRTS" -prove_op add "-DADD -DADDSUB -DADDS" -prove_op sub "-DSUB -DADDSUB -DADDS" -prove_op mul "-DMUL -DMULS" -prove_op div "-DDIV -DDIVS" -prove_op muladd "-DMULADD -DMULS -DADDS" - -prove_op altdiv "-DALTDIV -DDIVS" -prove_op altsqrt "-DALTSQRT -DSQRTS" - -prove_op_unrounded min "-DMIN -DCOMPARES" -prove_op_unrounded max "-DMAX -DCOMPARES" - -generate_mk --yosys-scripts From c3043b1ce5f920f51ca21e94454bc8d66dd717f3 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:50:33 +1200 Subject: [PATCH 29/41] symfpu: whitespace --- passes/cmds/symfpu.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 923b277b4..45b05da07 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -279,10 +279,10 @@ template struct bv { bv operator>>(const bv &op) const { log_assert(getWidth() == op.getWidth()); - if (is_signed) - return bv{symfpu_mod->Sshr(NEW_ID, bits, op.bits, is_signed)}; - else - return bv{symfpu_mod->Shr(NEW_ID, bits, op.bits, is_signed)}; + if (is_signed) + return bv{symfpu_mod->Sshr(NEW_ID, bits, op.bits, is_signed)}; + else + return bv{symfpu_mod->Shr(NEW_ID, bits, op.bits, is_signed)}; } prop operator!=(const bv &op) const From 6730b3ec542d3656818fc01893308cd6305fa4e2 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:51:06 +1200 Subject: [PATCH 30/41] libs/symfpu: Fixup submodule --- .gitmodules | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.gitmodules b/.gitmodules index bbe58b111..d951c8d01 100644 --- a/.gitmodules +++ b/.gitmodules @@ -20,7 +20,7 @@ [submodule "sv-elab"] path = frontends/slang/lib url = https://github.com/povik/sv-elab -[submodule "libs/symfpu"] +[submodule "symfpu"] path = libs/symfpu - url = https://github.com/martin-cs/symfpu - branch = experimental + url = https://github.com/YosysHQ/symfpu + branch = floatWithStatusFlags From 9dd5c3a6a4a15aee10fea443f3c560618f03f413 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 15 Jul 2026 14:56:11 +1200 Subject: [PATCH 31/41] symfpu: Run pre-commit --- passes/cmds/symfpu.cc | 8 ++++---- tests/symfpu/edges.sv | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 45b05da07..f750214d4 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -643,7 +643,7 @@ struct SymFpuPass : public Pass { output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); }; - if (rounding.compare("DYN") != 0) + if (rounding.compare("DYN") != 0) output_fpu(make_op(rounding_mode)); else { auto out_RNE = make_op(rtlil_traits::RNE()); @@ -652,10 +652,10 @@ struct SymFpuPass : public Pass { auto out_RTN = make_op(rtlil_traits::RTN()); auto out_RTZ = make_op(rtlil_traits::RTZ()); output_fpu( - uf_flagged_ite::iteOp(rm_RNE, out_RNE, + uf_flagged_ite::iteOp(rm_RNE, out_RNE, uf_flagged_ite::iteOp(rm_RNA, out_RNA, uf_flagged_ite::iteOp(rm_RTP, out_RTP, - uf_flagged_ite::iteOp(rm_RTN, out_RTN, + uf_flagged_ite::iteOp(rm_RTN, out_RTN, uf_flagged_ite::iteOp(rm_RTZ, out_RTZ, uf_flagged::makeNaN(format, prop(true))))))) ); @@ -760,7 +760,7 @@ struct SymFpuConvertPass : public Pass { symfpu_mod = mod; fpt i_format(i_exp, i_size-i_exp); - fpt o_format(o_exp, o_size-o_exp); + fpt o_format(o_exp, o_size-o_exp); auto i_bv = input_ubv(ID(i), i_size); uf i_f = symfpu::unpack(i_format, i_bv); diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index adcfc9e19..5be02d3bd 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -119,7 +119,7 @@ module edges(input clk); wire lhs_norm = b_is_1 ? a_norm : b_norm; wire lhs_subnorm = b_is_1 ? a_subnorm : b_subnorm; wire lhs_finite = b_is_1 ? a_finite : b_finite; - + wire rhs_sign = c_sign; wire [30:0] rhs_unsigned = c_unsigned; wire [7:0] rhs_exp = c_exp; From fb0bb160ad429f24cab5dd45e0b96c9182353555 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 17 Jul 2026 12:02:43 +0200 Subject: [PATCH 32/41] autoname: rewrite --- passes/cmds/autoname.cc | 301 ++++++++++++++++++++++++++------------ tests/various/autoname.ys | 9 +- 2 files changed, 216 insertions(+), 94 deletions(-) diff --git a/passes/cmds/autoname.cc b/passes/cmds/autoname.cc index 6994fdefd..2a7043a2b 100644 --- a/passes/cmds/autoname.cc +++ b/passes/cmds/autoname.cc @@ -17,95 +17,233 @@ * */ + #include "kernel/yosys.h" +#include +#include +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -typedef struct name_proposal { - string name; +// An "object" is a cell or a wire. +// An object is "private" if its name starts with a '$'. +// +// The "autoname" pass renames private objects based on public object names, +// with suffixes added to show the relationship to the public objects. +// The pass chooses the "best" names based on minimizing their "cost". + +// The cost of a new name for a private object is the cost along a path +// to a publicly named object. +struct cost { + // score is a property of one "edge", not of the entire path. + // 0 if the neighbour drives the object, and the wire's fanout otherwise + unsigned int score = UINT_MAX; + // New name length + size_t length = SIZE_MAX; + // Earlier discovered connection wins + int edge_pos = 0; + + auto operator<=>(const cost &) const = default; +}; + +// Endpoints of an "edge" are always a cell index and a wire index. Goofy, I know. +// SigSig connections (module->connections()) don't count +// as neighbors. This means that the equivalent of `assign $w1 = \w2;` won't lead +// to $w1 being renamed. +struct Edge { + // Cell port name at which the wire connects to the cell + IdString port; + int cell; + int wire; + bool cell_is_output; unsigned int score; - name_proposal() : name(""), score(-1) { } - name_proposal(string name, unsigned int score) : name(name), score(score) { } - bool operator<(const name_proposal &other) const { - if (score != other.score) - return score < other.score; - else - return name.length() < other.name.length(); - } -} name_proposal; + // Edge's position in the edge list + int pos_in_cell; + int pos_in_wire; +}; -int autoname_worker(Module *module, const dict& wire_score) +// decide() finds shortest names for every object reachable from a public name, +// cheapest-first. It doesn't apply the renames to the objects yet. +// +// commit() then renames in decide() order, which is topological, so a source +// neighbour always already carries its final uniquify()d name. + +// A selected cell or wire +struct node { + // Exactly one of cell/wire is set + Cell *cell = nullptr; + Wire *wire = nullptr; + vector edges; + // Ignores module->connections() just as the rest of the code + unsigned int fanout = 0; + bool is_public = false; + bool renameable = false; + + size_t name_length = 0; + // Node index from which we want to construct the rename + int from_node = -1; + // Cost for the edge from that node + cost c; + // Suffix to append to the name of that node + string suffix; + // Is this name final? + bool decided = false; +}; + +// Decides the order of exploring neighbors +struct queue_item { + unsigned int score; + size_t length; + int index; + + auto operator<=>(const queue_item &) const = default; +}; + +struct ModuleAutonamer { - dict proposed_cell_names; - dict proposed_wire_names; - name_proposal best_name; + Module *module; - for (auto cell : module->selected_cells()) { - if (cell->name[0] == '$') { + // Cells in module order, then wires in the order that they're seen from cells. + // The index doubles as the tie-break between equally good + // proposals for different nodes. + vector nodes; + vector decided; + std::priority_queue, std::greater<>> queue; + int renamed = 0; + + ModuleAutonamer(Module *module) : module(module) { build_adjacency(); } + + void build_adjacency() + { + auto selected = module->selected_cells(); + // Arbitrary. Kinda just for passing tests without modifying them. + for (auto cell : selected | std::views::reverse) + nodes.emplace_back().cell = cell; + int ncells = GetSize(nodes); + + idict wire_ids; + + for (int ci = 0; ci < ncells; ci++) { + Cell *cell = nodes[ci].cell; for (auto &conn : cell->connections()) { - string suffix; - for (auto bit : conn.second) - if (bit.wire != nullptr && bit.wire->name[0] != '$') { - if (suffix.empty()) - suffix = stringf("_%s_%s", cell->type.unescape(), conn.first.unescape()); - name_proposal proposed_name( - bit.wire->name.str() + suffix, - cell->output(conn.first) ? 0 : wire_score.at(bit.wire) - ); - if (!proposed_cell_names.count(cell) || proposed_name < proposed_cell_names.at(cell)) { - if (proposed_name < best_name) - best_name = proposed_name; - proposed_cell_names[cell] = proposed_name; - } - } - } - } else { - for (auto &conn : cell->connections()) { - string suffix; - for (auto bit : conn.second) - if (bit.wire != nullptr && bit.wire->name[0] == '$' && !bit.wire->port_id) { - if (suffix.empty()) - suffix = stringf("_%s", conn.first.unescape()); - name_proposal proposed_name( - cell->name.str() + suffix, - cell->output(conn.first) ? 0 : wire_score.at(bit.wire) - ); - if (!proposed_wire_names.count(bit.wire) || proposed_name < proposed_wire_names.at(bit.wire)) { - if (proposed_name < best_name) - best_name = proposed_name; - proposed_wire_names[bit.wire] = proposed_name; - } - } + bool cell_is_output = cell->output(conn.first); + pool seen_in_this_port; + for (auto bit : conn.second) { + if (bit.wire == nullptr) + continue; + int wi = ncells + wire_ids(bit.wire); + if (wi == GetSize(nodes)) + nodes.emplace_back().wire = bit.wire; + nodes[wi].fanout++; + if (!seen_in_this_port.insert(bit.wire).second) + continue; + Edge edge{ + .port = conn.first, + .cell = ci, + .wire = wi, + .cell_is_output = cell_is_output, + .score = 0, // no fanouts are final yet + .pos_in_cell = GetSize(nodes[ci].edges), + .pos_in_wire = GetSize(nodes[wi].edges), + }; + nodes[ci].edges.push_back(edge); + nodes[wi].edges.push_back(edge); + } } } + + for (auto &nd : nodes) { + IdString name = nd.cell ? nd.cell->name : nd.wire->name; + nd.is_public = (name[0] != '$'); + nd.renameable = !nd.is_public && (nd.cell || nd.wire->port_id == 0); + if (nd.is_public) + nd.name_length = name.str().size(); + } + + // Only possible once every fanout is known. + for (auto &nd : nodes) + for (auto &edge : nd.edges) + edge.score = edge.cell_is_output ? 0 : nodes[edge.wire].fanout; + } + + void offer(int from, int n, const Edge &edge, int edge_pos) + { + node &nd = nodes[n]; + if (!nd.renameable || nd.decided) + return; + string suffix = nd.cell + ? stringf("_%s_%s", nd.cell->type.unescape(), edge.port.unescape()) + : stringf("_%s", edge.port.unescape()); + cost c{edge.score, nodes[from].name_length + suffix.length(), edge_pos}; + if (c >= nd.c) + return; + nd.c = c; + nd.from_node = from; + nd.name_length = c.length; + nd.suffix = std::move(suffix); + queue.push(queue_item{c.score, c.length, n}); + } + + // Expand a public (or newly decided) node. The name it lends + // is already settled and the neighbour can keep what offer() built + void expand(int n) + { + const node &nd = nodes[n]; + for (auto &edge : nd.edges) + if (nd.cell) + offer(n, edge.wire, edge, edge.pos_in_wire); + else + offer(n, edge.cell, edge, edge.pos_in_cell); + } + + void decide() + { + for (int n = 0; n < GetSize(nodes); n++) + if (nodes[n].is_public) + expand(n); + + while (!queue.empty()) { + int n = queue.top().index; + queue.pop(); + if (nodes[n].decided) + continue; + nodes[n].decided = true; + decided.push_back(n); + expand(n); + } } - int count = 0; - // compare against double best score for following comparisons so we don't - // pre-empt a future iteration - best_name.score *= 2; - - for (auto &it : proposed_cell_names) { - if (best_name < it.second) - continue; - IdString n = module->uniquify(IdString(it.second.name)); - log_debug("Rename cell %s in %s to %s.\n", it.first, module, n.unescape()); - module->rename(it.first, n); - count++; + // The source neighbour is decided before this node, so commit() reaches it + // first and its name is already final -- uniquify() suffix and all. + void commit(int n) + { + node &nd = nodes[n]; + const node &src = nodes[nd.from_node]; + string full; + full.reserve(nd.name_length); + (src.cell ? src.cell->name : src.wire->name).append_to(&full); + full += nd.suffix; + IdString name = module->uniquify(IdString(full)); + if (nd.cell) { + log_debug("Rename cell %s in %s to %s.\n", nd.cell, module, name.unescape()); + module->rename(nd.cell, name); + } else { + log_debug("Rename wire %s in %s to %s.\n", nd.wire, module, name.unescape()); + module->rename(nd.wire, name); + } + renamed++; } - for (auto &it : proposed_wire_names) { - if (best_name < it.second) - continue; - IdString n = module->uniquify(IdString(it.second.name)); - log_debug("Rename wire %s in %s to %s.\n", it.first, module, n.unescape()); - module->rename(it.first, n); - count++; + void run() + { + decide(); + for (int n : decided) + commit(n); + if (renamed > 0) + log("Renamed %d objects in module %s.\n", renamed, module); } - - return count; -} +}; struct AutonamePass : public Pass { AutonamePass() : Pass("autoname", "automatically assign names to objects") { } @@ -135,24 +273,7 @@ struct AutonamePass : public Pass { log_header(design, "Executing AUTONAME pass.\n"); for (auto module : design->selected_modules()) - { - dict wire_score; - for (auto cell : module->selected_cells()) - for (auto &conn : cell->connections()) - for (auto bit : conn.second) - if (bit.wire != nullptr) - wire_score[bit.wire]++; - - int count = 0, iter = 0; - while (1) { - iter++; - int n = autoname_worker(module, wire_score); - if (!n) break; - count += n; - } - if (count > 0) - log("Renamed %d objects in module %s (%d iterations).\n", count, module, iter); - } + ModuleAutonamer(module).run(); } } AutonamePass; diff --git a/tests/various/autoname.ys b/tests/various/autoname.ys index 7df1571b2..c5bd0ba3b 100644 --- a/tests/various/autoname.ys +++ b/tests/various/autoname.ys @@ -180,15 +180,16 @@ design -save order_test # wires are named for being cell outputs logger -expect log "Rename wire .d in top to or_Y" 1 logger -expect log "Rename cell .name2 in top to or_Y_.or_B" 1 -logger -expect log "Renamed 2 objects" 1 +logger -expect log "Rename wire .e in top to or_Y_.or_B_Y" 1 +logger -expect log "Rename wire .c in top to or_Y_.or_B_A" 1 +logger -expect log "Renamed 4 objects" 1 debug autoname t:$or logger -check-expected # $name gets shortest name (otherwise bcd_$__unknown_B) logger -expect log "Rename cell .name in top to a_.__unknown_A" 1 -# another output wire -logger -expect log "Rename wire .e in top to or_Y_.or_B_Y" 1 -logger -expect log "Renamed 4 objects" 1 +logger -expect log "Rename cell .name3 in top to or_Y_.or_B_Y_.and_B" 1 +logger -expect log "Renamed 2 objects" 1 debug autoname logger -check-expected From 8565451ef9399802b5fc037abe056251a3a8a93f Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 17 Jul 2026 22:48:46 +0200 Subject: [PATCH 33/41] autoname: selection determines what gets renamed, not the name it gets renamed to --- passes/cmds/autoname.cc | 39 ++++++++++++++++++++----------- tests/various/autoname.ys | 48 +++++++++++++++++++++++++++------------ 2 files changed, 60 insertions(+), 27 deletions(-) diff --git a/passes/cmds/autoname.cc b/passes/cmds/autoname.cc index 2a7043a2b..134d36ee6 100644 --- a/passes/cmds/autoname.cc +++ b/passes/cmds/autoname.cc @@ -79,6 +79,7 @@ struct node { unsigned int fanout = 0; bool is_public = false; bool renameable = false; + bool selected = false; size_t name_length = 0; // Node index from which we want to construct the rename @@ -89,6 +90,8 @@ struct node { string suffix; // Is this name final? bool decided = false; + + const IdString& name() const { return cell ? cell->name : wire->name; } }; // Decides the order of exploring neighbors @@ -106,7 +109,7 @@ struct ModuleAutonamer // Cells in module order, then wires in the order that they're seen from cells. // The index doubles as the tie-break between equally good - // proposals for different nodes. + // proposals for different nodes vector nodes; vector decided; std::priority_queue, std::greater<>> queue; @@ -116,9 +119,9 @@ struct ModuleAutonamer void build_adjacency() { - auto selected = module->selected_cells(); - // Arbitrary. Kinda just for passing tests without modifying them. - for (auto cell : selected | std::views::reverse) + vector cells(module->cells().begin(), module->cells().end()); + // Arbitrary. Kinda just for passing tests without modifying them + for (auto cell : cells | std::views::reverse) nodes.emplace_back().cell = cell; int ncells = GetSize(nodes); @@ -153,23 +156,25 @@ struct ModuleAutonamer } } + // Resolve selection before renaming for (auto &nd : nodes) { - IdString name = nd.cell ? nd.cell->name : nd.wire->name; + IdString name = nd.name(); + nd.selected = nd.cell ? module->selected(nd.cell) : module->selected(nd.wire); nd.is_public = (name[0] != '$'); nd.renameable = !nd.is_public && (nd.cell || nd.wire->port_id == 0); if (nd.is_public) nd.name_length = name.str().size(); } - // Only possible once every fanout is known. + // Only possible once every fanout is known for (auto &nd : nodes) for (auto &edge : nd.edges) edge.score = edge.cell_is_output ? 0 : nodes[edge.wire].fanout; } - void offer(int from, int n, const Edge &edge, int edge_pos) + void offer(int from, int to, const Edge &edge, int edge_pos) { - node &nd = nodes[n]; + node &nd = nodes[to]; if (!nd.renameable || nd.decided) return; string suffix = nd.cell @@ -182,7 +187,7 @@ struct ModuleAutonamer nd.from_node = from; nd.name_length = c.length; nd.suffix = std::move(suffix); - queue.push(queue_item{c.score, c.length, n}); + queue.push(queue_item{c.score, c.length, to}); } // Expand a public (or newly decided) node. The name it lends @@ -214,15 +219,23 @@ struct ModuleAutonamer } } - // The source neighbour is decided before this node, so commit() reaches it - // first and its name is already final -- uniquify() suffix and all. + void append_name(int n, string &out) + { + const node &nd = nodes[n]; + if (nd.is_public || nd.selected) + return nd.name().append_to(&out); + append_name(nd.from_node, out); + out += nd.suffix; + } + void commit(int n) { node &nd = nodes[n]; - const node &src = nodes[nd.from_node]; + if (!nd.selected) + return; string full; full.reserve(nd.name_length); - (src.cell ? src.cell->name : src.wire->name).append_to(&full); + append_name(nd.from_node, full); full += nd.suffix; IdString name = module->uniquify(IdString(full)); if (nd.cell) { diff --git a/tests/various/autoname.ys b/tests/various/autoname.ys index c5bd0ba3b..22b532f2c 100644 --- a/tests/various/autoname.ys +++ b/tests/various/autoname.ys @@ -78,12 +78,21 @@ module \top end end EOT +design -save fanout_test logger -expect log "Rename cell .name in top to bcd_.and_B" 1 logger -expect log "Rename cell .name2 in top to c_has_a_long_name_.or_B" 1 logger -expect log "Renamed 2 objects" 1 debug autoname logger -check-expected +# a selection only limits what gets renamed, never the name that gets picked: +# \a's fanout still counts $name2, even though it isn't selected +design -load fanout_test +logger -expect log "Rename cell .name in top to bcd_.and_B" 1 +logger -expect log "Renamed 1 objects" 1 +debug autoname c:$name +logger -check-expected + # names are unique design -reset read_rtlil < Date: Mon, 20 Jul 2026 09:58:04 +1200 Subject: [PATCH 34/41] symfpu: Drop libs/ from symfpu includes --- passes/cmds/symfpu.cc | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index f750214d4..789a84405 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -20,17 +20,17 @@ #include "kernel/log_help.h" #include "kernel/yosys.h" -#include "libs/symfpu/baseTypes/shared.h" -#include "libs/symfpu/core/add.h" -#include "libs/symfpu/core/divide.h" -#include "libs/symfpu/core/fma.h" -#include "libs/symfpu/core/ite.h" -#include "libs/symfpu/core/multiply.h" -#include "libs/symfpu/core/packing.h" -#include "libs/symfpu/core/sqrt.h" -#include "libs/symfpu/core/unpackedFloat.h" -#include "libs/symfpu/core/classify.h" -#include "libs/symfpu/core/compare.h" +#include "symfpu/baseTypes/shared.h" +#include "symfpu/core/add.h" +#include "symfpu/core/divide.h" +#include "symfpu/core/fma.h" +#include "symfpu/core/ite.h" +#include "symfpu/core/multiply.h" +#include "symfpu/core/packing.h" +#include "symfpu/core/sqrt.h" +#include "symfpu/core/unpackedFloat.h" +#include "symfpu/core/classify.h" +#include "symfpu/core/compare.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN From 60403f35cad61a8e49c63dbc539f15958f03bda7 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 20 Jul 2026 08:23:37 +0200 Subject: [PATCH 35/41] CI: back to using official action --- .github/workflows/extra-builds.yml | 2 +- .github/workflows/prepare-docs.yml | 2 +- .github/workflows/test-build.yml | 4 ++-- .github/workflows/test-compile.yml | 2 +- .github/workflows/test-sanitizers.yml | 2 +- .github/workflows/test-verific.yml | 2 +- 6 files changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/extra-builds.yml b/.github/workflows/extra-builds.yml index d041794d7..4601f1b12 100644 --- a/.github/workflows/extra-builds.yml +++ b/.github/workflows/extra-builds.yml @@ -15,7 +15,7 @@ jobs: steps: - id: skip_check if: ${{ github.event_name != 'merge_group' }} - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: # don't run on documentation changes paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' diff --git a/.github/workflows/prepare-docs.yml b/.github/workflows/prepare-docs.yml index 32f4619f7..db57acc1c 100644 --- a/.github/workflows/prepare-docs.yml +++ b/.github/workflows/prepare-docs.yml @@ -18,7 +18,7 @@ jobs: docs_export: ${{ github.ref == 'refs/heads/main' || startsWith(github.ref, 'refs/heads/docs-preview') || startsWith(github.ref, 'refs/tags/') }} steps: - id: skip_check - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: paths_ignore: '["**/README.md"]' # don't cancel in case we're updating docs diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index 566aad3c7..783210254 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -15,7 +15,7 @@ jobs: steps: - id: skip_check if: ${{ github.event_name != 'merge_group' }} - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: # don't run on documentation changes paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' @@ -38,7 +38,7 @@ jobs: steps: - id: skip_check if: ${{ github.event_name != 'merge_group' }} - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: # don't run on readme changes paths_ignore: '["**/README.md"]' diff --git a/.github/workflows/test-compile.yml b/.github/workflows/test-compile.yml index b57b0df53..b004959d3 100644 --- a/.github/workflows/test-compile.yml +++ b/.github/workflows/test-compile.yml @@ -15,7 +15,7 @@ jobs: steps: - id: skip_check if: ${{ github.event_name != 'merge_group' }} - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: # don't run on documentation changes paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' diff --git a/.github/workflows/test-sanitizers.yml b/.github/workflows/test-sanitizers.yml index d0509eb43..0029fdd8b 100644 --- a/.github/workflows/test-sanitizers.yml +++ b/.github/workflows/test-sanitizers.yml @@ -15,7 +15,7 @@ jobs: steps: - id: skip_check if: ${{ github.event_name != 'merge_group' }} - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: # don't run on documentation changes paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml index c73b9248b..54d582063 100644 --- a/.github/workflows/test-verific.yml +++ b/.github/workflows/test-verific.yml @@ -15,7 +15,7 @@ jobs: steps: - id: skip_check if: ${{ github.event_name != 'merge_group' && github.event_name != 'push' }} - uses: mmicko/skip-duplicate-actions@master + uses: fkirc/skip-duplicate-actions@v5.3.2 with: # don't run on documentation changes paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]' From a7cfabd40563b41f67432d2831e5178a8fbc64bd Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 20 Jul 2026 10:29:41 +0200 Subject: [PATCH 36/41] Fix gcc compile errors --- libs/symfpu | 2 +- passes/cmds/symfpu.cc | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/libs/symfpu b/libs/symfpu index e68bf9d0b..c0dd6eef9 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit e68bf9d0bb2e038e970ed11c7edcc19f29d84b12 +Subproject commit c0dd6eef9759381a67572c0098fbe118e23d2429 diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 789a84405..c227266a6 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -49,12 +49,12 @@ struct rm { thread_local Module *symfpu_mod = nullptr; struct rtlil_traits { - typedef uint64_t bwt; - typedef rm rm; - typedef symfpu::shared::floatingPointTypeInfo fpt; - typedef prop prop; - typedef bv sbv; - typedef bv ubv; + using bwt = uint64_t; + using rm = struct rm; + using fpt = symfpu::shared::floatingPointTypeInfo; + using prop = struct prop; + using sbv = bv; + using ubv = bv; // Return an instance of each rounding mode. static rm RNE(void) { return {rm::mode::RNE}; }; @@ -348,7 +348,7 @@ template bv symfpu::ite>::iteOp( return bv{symfpu_mod->Mux(NEW_ID, e.bits, t.bits, cond.bit)}; } -prop symfpu::ite::iteOp(bool cond, const prop &t, const prop &e) { return cond ? t : e; } +[[maybe_unused]] prop symfpu::ite::iteOp(bool cond, const prop &t, const prop &e) { return cond ? t : e; } template bv symfpu::ite>::iteOp(bool cond, const bv &t, const bv &e) { From cfd80cb48e114d730b8237e18150b4b018929c01 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 20 Jul 2026 11:53:55 +0200 Subject: [PATCH 37/41] Update constids to fix leaks --- kernel/constids.inc | 32 ++++++++++++++++++++++++++++++++ libs/symfpu | 2 +- 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/kernel/constids.inc b/kernel/constids.inc index cfd12e3fb..16cb80ce6 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -448,6 +448,7 @@ X(DST_EN) X(DST_PEN) X(DST_POL) X(DST_WIDTH) +X(DZ) X(D_ARST_N) X(D_BYPASS) X(D_EN) @@ -580,11 +581,14 @@ X(NMUX) X(NOR) X(NOT) X(NPRODUCTS) +X(NV) +X(NX) X(NX_CY) X(NX_CY_1BIT) X(O) X(OAI3) X(OAI4) +X(OF) X(OFFSET) X(OHOLDBOT) X(OHOLDTOP) @@ -779,6 +783,7 @@ X(T_RISE_MAX) X(T_RISE_MIN) X(T_RISE_TYP) X(U) +X(UF) X(UP) X(USE_DPORT) X(USE_MULT) @@ -882,6 +887,9 @@ X(f_mode) X(feedback) X(feedback_i) X(first) +X(flags_ff) +X(flags_fi) +X(flags_if) X(force_downto) X(force_upto) X(fsm_encoding) @@ -898,6 +906,7 @@ X(gold) X(hdlname) X(hierconn) X(i) +X(ieee754Equal) X(init) X(initial_top) X(interface_modport) @@ -905,11 +914,22 @@ X(interface_type) X(interfaces_replaced_in_module) X(invertible_pin) X(iopad_external_pin) +X(isFinite) +X(isInfinite) +X(isNaN) +X(isNegative) +X(isNormal) +X(isPositive) +X(isSubnormal) +X(isZero) X(is_inferred) X(is_interface) +X(is_signed) X(it) X(keep) X(keep_hierarchy) +X(lessThan) +X(lessThanOrEqual) X(lib_whitebox) X(library) X(load_acc) @@ -938,6 +958,9 @@ X(nomeminit) X(nosync) X(nowrshmsk) X(o) +X(o_ff) +X(o_fi) +X(o_if) X(offset) X(onehot) X(output_select) @@ -946,6 +969,7 @@ X(p_class) X(parallel_case) X(parameter) X(promoted_if) +X(qNV) X(raise_error) X(ram_block) X(ram_style) @@ -957,12 +981,14 @@ X(replaced_by_gclk) X(reprocess_after) X(reset) X(reset_i) +X(rm) X(rom_block) X(rom_style) X(romstyle) X(round) X(round_i) X(rtlil) +X(sNV) X(saturate_enable) X(saturate_enable_i) X(scopename) @@ -972,11 +998,16 @@ X(shift_right_i) X(single_bit_vector) X(smtlib2_comb_expr) X(smtlib2_module) +X(smtlibEqual) X(src) X(sta_arrival) X(submod) X(subtract) X(subtract_i) +X(symfpu) +X(symfpu_inv) +X(symfpu_post) +X(symfpu_pre) X(syn_ramstyle) X(syn_romstyle) X(techmap_autopurge) @@ -996,6 +1027,7 @@ X(unsigned_a) X(unsigned_a_i) X(unsigned_b) X(unsigned_b_i) +X(unsupported_sva) X(unused_bits) X(use_dsp) X(value) diff --git a/libs/symfpu b/libs/symfpu index c0dd6eef9..5d5e50867 160000 --- a/libs/symfpu +++ b/libs/symfpu @@ -1 +1 @@ -Subproject commit c0dd6eef9759381a67572c0098fbe118e23d2429 +Subproject commit 5d5e50867437fe5cabd6ab5aad3b3808ec86701f From 3006280d709c901ff108d94b423b4f7549422edc Mon Sep 17 00:00:00 2001 From: drewbabel <122849144+drewbabel@users.noreply.github.com> Date: Mon, 20 Jul 2026 23:59:40 -0700 Subject: [PATCH 38/41] xilinx_srl: keep the clock enable on FDRE shift registers run_fixed inferred a fixed length shift register from a chain of FDRE flops but assigned it ENPOL 2, which the cells_map template reads as no enable and ties the enable high. FDRE has an active high clock enable, so the shift register shifted every cycle and ignored stalls. Give FDRE and FDRE_1 chains ENPOL 1 so the active high enable is kept. Add tests/arch/xilinx/xilinx_srl_enable.ys covering the FDRE path. --- techlibs/xilinx/xilinx_srl.cc | 2 +- tests/arch/xilinx/xilinx_srl_enable.ys | 46 ++++++++++++++++++++++++++ 2 files changed, 47 insertions(+), 1 deletion(-) create mode 100644 tests/arch/xilinx/xilinx_srl_enable.ys diff --git a/techlibs/xilinx/xilinx_srl.cc b/techlibs/xilinx/xilinx_srl.cc index e23062eb7..10aa789e5 100644 --- a/techlibs/xilinx/xilinx_srl.cc +++ b/techlibs/xilinx/xilinx_srl.cc @@ -77,7 +77,7 @@ void run_fixed(xilinx_srl_pm &pm) } else log_abort(); - if (first_cell->type.in(ID($_DFFE_NP_), ID($_DFFE_PP_))) + if (first_cell->type.in(ID($_DFFE_NP_), ID($_DFFE_PP_), ID(FDRE), ID(FDRE_1))) c->setParam(ID(ENPOL), 1); else if (first_cell->type.in(ID($_DFFE_NN_), ID($_DFFE_PN_))) c->setParam(ID(ENPOL), 0); diff --git a/tests/arch/xilinx/xilinx_srl_enable.ys b/tests/arch/xilinx/xilinx_srl_enable.ys new file mode 100644 index 000000000..c95a849aa --- /dev/null +++ b/tests/arch/xilinx/xilinx_srl_enable.ys @@ -0,0 +1,46 @@ +# Regression test for a xilinx_srl bug where a fixed shift register inferred +# from FDRE cells dropped the clock enable. FDRE has an active high clock +# enable but run_fixed assigned it ENPOL 2 (no enable) instead of ENPOL 1, +# so the resulting shift register shifted every cycle and ignored stalls. +read_verilog < Date: Fri, 27 Mar 2026 09:58:37 +0000 Subject: [PATCH 39/41] abc: remove -fast (again) --- passes/techmap/abc.cc | 42 +++++------------------------------------- 1 file changed, 5 insertions(+), 37 deletions(-) diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 47ae49181..3c4341808 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -35,12 +35,6 @@ #define ABC_COMMAND_SOP "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; dch -f; cover {I} {P}" #define ABC_COMMAND_DFL "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" -#define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}" -#define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p" -#define ABC_FAST_COMMAND_LUT "strash; dretime; if" -#define ABC_FAST_COMMAND_SOP "strash; dretime; cover {I} {P}" -#define ABC_FAST_COMMAND_DFL "strash; dretime; map" - #include "kernel/register.h" #include "kernel/sigtools.h" #include "kernel/newcelltypes.h" @@ -139,7 +133,6 @@ struct AbcConfig std::vector dont_use_cells; bool cleanup = true; bool keepff = false; - bool fast_mode = false; bool show_tempdir = false; bool sop_mode = false; bool abc_dress = false; @@ -1077,16 +1070,15 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module for (int this_cost : config.lut_costs) if (this_cost != config.lut_costs.front()) all_luts_cost_same = false; - run_abc.abc_script += config.fast_mode ? ABC_FAST_COMMAND_LUT : ABC_COMMAND_LUT; - if (all_luts_cost_same && !config.fast_mode) + run_abc.abc_script += ABC_COMMAND_LUT; + if (all_luts_cost_same) run_abc.abc_script += "; lutpack -S 1"; } else if (!config.liberty_files.empty() || !config.genlib_files.empty()) - run_abc.abc_script += config.constr_file.empty() ? - (config.fast_mode ? ABC_FAST_COMMAND_LIB : ABC_COMMAND_LIB) : (config.fast_mode ? ABC_FAST_COMMAND_CTR : ABC_COMMAND_CTR); + run_abc.abc_script += config.constr_file.empty() ? ABC_COMMAND_LIB : ABC_COMMAND_CTR; else if (config.sop_mode) - run_abc.abc_script += config.fast_mode ? ABC_FAST_COMMAND_SOP : ABC_COMMAND_SOP; + run_abc.abc_script += ABC_COMMAND_SOP; else - run_abc.abc_script += config.fast_mode ? ABC_FAST_COMMAND_DFL : ABC_COMMAND_DFL; + run_abc.abc_script += ABC_COMMAND_DFL; if (config.script_file.empty() && !config.delay_target.empty()) for (size_t pos = run_abc.abc_script.find("dretime;"); pos != std::string::npos; pos = run_abc.abc_script.find("dretime;", pos+1)) @@ -1911,25 +1903,6 @@ struct AbcPass : public Pass { log(" otherwise:\n"); log("%s\n", fold_abc_cmd(ABC_COMMAND_DFL)); log("\n"); - log(" -fast\n"); - log(" use different default scripts that are slightly faster (at the cost\n"); - log(" of output quality):\n"); - log("\n"); - log(" for -liberty/-genlib without -constr:\n"); - log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_LIB)); - log("\n"); - log(" for -liberty/-genlib with -constr:\n"); - log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_CTR)); - log("\n"); - log(" for -lut/-luts:\n"); - log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_LUT)); - log("\n"); - log(" for -sop:\n"); - log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_SOP)); - log("\n"); - log(" otherwise:\n"); - log("%s\n", fold_abc_cmd(ABC_FAST_COMMAND_DFL)); - log("\n"); log(" -liberty \n"); log(" generate netlists for the specified cell library (using the liberty\n"); log(" file format).\n"); @@ -2093,7 +2066,6 @@ struct AbcPass : public Pass { config.abc_dress = design->scratchpad_get_bool("abc.dress", false); g_arg = design->scratchpad_get_string("abc.g", g_arg); - config.fast_mode = design->scratchpad_get_bool("abc.fast", false); bool dff_mode = design->scratchpad_get_bool("abc.dff", false); std::string clk_str; if (design->scratchpad.count("abc.clk")) { @@ -2202,10 +2174,6 @@ struct AbcPass : public Pass { g_arg_from_cmd = true; continue; } - if (arg == "-fast") { - config.fast_mode = true; - continue; - } if (arg == "-dff") { dff_mode = true; continue; From f0b5225134f6a7c3149b72952b4b196e5f1feb29 Mon Sep 17 00:00:00 2001 From: Lofty Date: Wed, 22 Jul 2026 13:38:40 +0100 Subject: [PATCH 40/41] flowmap: remove --- CODEOWNERS | 1 - .../macro_commands/synth_ice40.ys | 1 - passes/techmap/CMakeLists.txt | 3 - passes/techmap/flowmap.cc | 1617 ----------------- techlibs/common/CMakeLists.txt | 1 - techlibs/common/synth.cc | 17 +- techlibs/ice40/CMakeLists.txt | 1 - techlibs/ice40/synth_ice40.cc | 20 +- 8 files changed, 5 insertions(+), 1656 deletions(-) delete mode 100644 passes/techmap/flowmap.cc diff --git a/CODEOWNERS b/CODEOWNERS index 681854226..5693e90f3 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -15,7 +15,6 @@ passes/cmds/scratchpad.cc @nakengelhardt frontends/rpc/ @whitequark backends/cxxrtl/ @whitequark passes/cmds/bugpoint.cc @whitequark -passes/techmap/flowmap.cc @whitequark passes/opt/opt_lut.cc @whitequark passes/techmap/abc9*.cc @eddiehung @Ravenslofty backends/aiger/xaiger.cc @eddiehung diff --git a/docs/source/code_examples/macro_commands/synth_ice40.ys b/docs/source/code_examples/macro_commands/synth_ice40.ys index 2b06d5568..fba5b66b8 100644 --- a/docs/source/code_examples/macro_commands/synth_ice40.ys +++ b/docs/source/code_examples/macro_commands/synth_ice40.ys @@ -71,7 +71,6 @@ map_luts: techmap simplemap techmap - flowmap read_verilog abc9 ice40_wrapcarry -unwrap diff --git a/passes/techmap/CMakeLists.txt b/passes/techmap/CMakeLists.txt index 7306fd6e8..6c3d54477 100644 --- a/passes/techmap/CMakeLists.txt +++ b/passes/techmap/CMakeLists.txt @@ -198,9 +198,6 @@ yosys_pass(dfflegalize yosys_pass(dffunmap dffunmap.cc ) -yosys_pass(flowmap - flowmap.cc -) yosys_pass(extractinv extractinv.cc ) diff --git a/passes/techmap/flowmap.cc b/passes/techmap/flowmap.cc deleted file mode 100644 index a6d461209..000000000 --- a/passes/techmap/flowmap.cc +++ /dev/null @@ -1,1617 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2018 whitequark - * - * 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. - * - */ - -// [[CITE]] FlowMap algorithm -// Jason Cong; Yuzheng Ding, "An Optimal Technology Mapping Algorithm for Delay Optimization in Lookup-Table Based FPGA Designs," -// Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, Vol. 13, pp. 1-12, Jan. 1994. -// doi: 10.1109/43.273754 - -// [[CITE]] FlowMap-r algorithm -// Jason Cong; Yuzheng Ding, "On Area/Depth Tradeoff in LUT-Based FPGA Technology Mapping," -// Very Large Scale Integration Systems, IEEE Transactions on, Vol. 2, June 1994. -// doi: 10.1109/92.28574 - -// Required reading material: -// -// Min-cut max-flow theorem: -// https://www.coursera.org/lecture/algorithms-part2/maxflow-mincut-theorem-beb9G -// FlowMap paper: -// http://cadlab.cs.ucla.edu/~cong/papers/iccad92.pdf (short version) -// https://limsk.ece.gatech.edu/book/papers/flowmap.pdf (long version) -// FlowMap-r paper: -// http://cadlab.cs.ucla.edu/~cong/papers/dac93.pdf (short version) -// https://sci-hub.tw/10.1109/92.285741 (long version) - -// Notes on correspondence between paper and implementation: -// -// 1. In the FlowMap paper, the nodes are logic elements (analogous to Yosys cells) and edges are wires. However, in our implementation, -// we use an inverted approach: the nodes are Yosys wire bits, and the edges are derived from (but aren't represented by) Yosys cells. -// This may seem counterintuitive. Three observations may help understanding this. First, for a cell with a 1-bit Y output that is -// the sole driver of its output net (which is the typical case), these representations are equivalent, because there is an exact -// correspondence between cells and output wires. Second, in the paper, primary inputs (analogous to Yosys cell or module ports) are -// nodes, and in Yosys, inputs are wires; our approach allows a direct mapping from both primary inputs and 1-output logic elements to -// flow graph nodes. Third, Yosys cells may have multiple outputs or multi-bit outputs, and by using Yosys wire bits as flow graph nodes, -// such cells are supported without any additional effort; any Yosys cell with n output wire bits ends up being split into n flow graph -// nodes. -// -// 2. The FlowMap paper introduces three networks: Nt, Nt', and Nt''. The network Nt is directly represented by a subgraph of RTLIL graph, -// which is parsed into an equivalent but easier to traverse representation in FlowmapWorker. The network Nt' is built explicitly -// from a subgraph of Nt, and uses a similar representation in FlowGraph. The network Nt'' is implicit in FlowGraph, which is possible -// because of the following observation: each Nt' node corresponds to an Nt'' edge of capacity 1, and each Nt' edge corresponds to -// an Nt'' edge of capacity ∞. Therefore, we only need to explicitly record flow for Nt' edges and through Nt' nodes. -// -// 3. The FlowMap paper ambiguously states: "Moreover, we can find such a cut (X′′, X̅′′) by performing a depth first search starting at -// the source s, and including in X′′ all the nodes which are reachable from s." This actually refers to a specific kind of search, -// min-cut computation. Min-cut computation involves computing the set of nodes reachable from s by an undirected path with no full -// (i.e. zero capacity) forward edges or empty (i.e. no flow) backward edges. In addition, the depth first search is required to compute -// a max-volume max-flow min-cut specifically, because a max-flow min-cut is not, in general, unique. - -// Notes on implementation: -// -// 1. To compute depth optimal packing, an intermediate representation is used, where each cell with n output bits is split into n graph -// nodes. Each such graph node is represented directly with the wire bit (RTLIL::SigBit instance) that corresponds to the output bit -// it is created from. Fan-in and fan-out are represented explicitly by edge lists derived from the RTLIL graph. This IR never changes -// after it has been computed. -// -// In terms of data, this IR is comprised of `inputs`, `outputs`, `nodes`, `edges_fw` and `edges_bw` fields. -// -// We call this IR "gate IR". -// -// 2. To compute area optimal packing, another intermediate representation is used, which consists of some K-feasible cone for every node -// that exists in the gate IR. Immediately after depth optimal packing with FlowMap, each such cone occupies the lowest possible depth, -// but this is not true in general, and transformations of this IR may change the cones, although each transformation has to keep each -// cone K-feasible. In this IR, LUT fan-in and fan-out are represented explicitly by edge lists; if a K-feasible cone chosen for node A -// includes nodes B and C, there are edges between all predecessors of A, B and C in the gate IR and node A in this IR. Moreover, in -// this IR, cones may be *realized* or *derealized*. Only realized cones will end up mapped to actual LUTs in the output of this pass. -// -// Intuitively, this IR contains (some, ideally but not necessarily optimal) LUT representation for each input cell. By starting at outputs -// and traversing the graph of this IR backwards, each K-feasible cone is converted to an actual LUT at the end of the pass. This is -// the same as iterating through each realized LUT. -// -// The following are the invariants of this IR: -// a) Each gate IR node corresponds to a K-feasible cut. -// b) Each realized LUT is reachable through backward edges from some output. -// c) The LUT fan-in is exactly the fan-in of its constituent gates minus the fan-out of its constituent gates. -// The invariants are kept even for derealized LUTs, since the whole point of this IR is ease of packing, unpacking, and repacking LUTs. -// -// In terms of data, this IR is comprised of `lut_nodes` (the set of all realized LUTs), `lut_gates` (the map from a LUT to its -// constituent gates), `lut_edges_fw` and `lut_edges_bw` fields. The `inputs` and `outputs` fields are shared with the gate IR. -// -// We call this IR "LUT IR". - -#include "kernel/yosys.h" -#include "kernel/sigtools.h" -#include "kernel/modtools.h" -#include "kernel/consteval.h" - -USING_YOSYS_NAMESPACE -PRIVATE_NAMESPACE_BEGIN - -struct GraphStyle -{ - string label; - string color, fillcolor; - - GraphStyle(string label = "", string color = "black", string fillcolor = "") : - label(label), color(color), fillcolor(fillcolor) {} -}; - -static string dot_escape(string value) -{ - std::string escaped; - for (char c : value) { - if (c == '\n') - { - escaped += "\\n"; - continue; - } - if (c == '\\' || c == '"') - escaped += "\\"; - escaped += c; - } - return escaped; -} - -static void dump_dot_graph(string filename, - pool nodes, dict> edges, - pool inputs, pool outputs, - std::function node_style = - [](RTLIL::SigBit) { return GraphStyle{}; }, - std::function edge_style = - [](RTLIL::SigBit, RTLIL::SigBit) { return GraphStyle{}; }, - string name = "") -{ - FILE *f = fopen(filename.c_str(), "w"); - fprintf(f, "digraph \"%s\" {\n", name.c_str()); - fprintf(f, " rankdir=\"TB\";\n"); - - dict ids; - for (auto node : nodes) - { - ids[node] = ids.size(); - - string shape = "ellipse"; - if (inputs[node]) - shape = "box"; - if (outputs[node]) - shape = "octagon"; - auto prop = node_style(node); - string style = ""; - if (!prop.fillcolor.empty()) - style = "filled"; - fprintf(f, " n%d [ shape=%s, fontname=\"Monospace\", label=\"%s\", color=\"%s\", fillcolor=\"%s\", style=\"%s\" ];\n", - ids[node], shape.c_str(), dot_escape(prop.label.c_str()).c_str(), prop.color.c_str(), prop.fillcolor.c_str(), style.c_str()); - } - - fprintf(f, " { rank=\"source\"; "); - for (auto input : inputs) - if (nodes[input]) - fprintf(f, "n%d; ", ids[input]); - fprintf(f, "}\n"); - - fprintf(f, " { rank=\"sink\"; "); - for (auto output : outputs) - if (nodes[output]) - fprintf(f, "n%d; ", ids[output]); - fprintf(f, "}\n"); - - for (auto edge : edges) - { - auto source = edge.first; - for (auto sink : edge.second) { - if (nodes[source] && nodes[sink]) - { - auto prop = edge_style(source, sink); - fprintf(f, " n%d -> n%d [ label=\"%s\", color=\"%s\", fillcolor=\"%s\" ];\n", - ids[source], ids[sink], dot_escape(prop.label.c_str()).c_str(), prop.color.c_str(), prop.fillcolor.c_str()); - } - } - } - - fprintf(f, "}\n"); - fclose(f); -} - -struct FlowGraph -{ - const RTLIL::SigBit source; - RTLIL::SigBit sink; - pool nodes = {source}; - dict> edges_fw, edges_bw; - - const int MAX_NODE_FLOW = 1; - dict node_flow; - dict, int> edge_flow; - - dict> collapsed; - - void dump_dot_graph(string filename) - { - auto node_style = [&](RTLIL::SigBit node) { - string label = (node == source) ? "(source)" : log_signal(node); - for (auto collapsed_node : collapsed[node]) - label += stringf(" %s", log_signal(collapsed_node)); - int flow = node_flow[node]; - if (node != source && node != sink) - label += stringf("\n%d/%d", flow, MAX_NODE_FLOW); - else - label += stringf("\n%d/∞", flow); - return GraphStyle{label, flow < MAX_NODE_FLOW ? "green" : "black"}; - }; - auto edge_style = [&](RTLIL::SigBit source, RTLIL::SigBit sink) { - int flow = edge_flow[{source, sink}]; - return GraphStyle{stringf("%d/∞", flow), flow > 0 ? "blue" : "black"}; - }; - ::dump_dot_graph(filename, nodes, edges_fw, {source}, {sink}, node_style, edge_style); - } - - // Here, we are working on the Nt'' network, but our representation is the Nt' network. - // The difference between these is that where in Nt' we have a subgraph: - // - // v1 -> v2 -> v3 - // - // in Nt'' we have a corresponding subgraph: - // - // v'1b -∞-> v'2t -f-> v'2b -∞-> v'3t - // - // To address this, we split each node v into two nodes, v't and v'b. This representation is virtual, - // in the sense that nodes v't and v'b are overlaid on top of the original node v, and only exist - // in paths and worklists. - - struct NodePrime - { - RTLIL::SigBit node; - bool is_bottom; - - NodePrime(RTLIL::SigBit node, bool is_bottom) : - node(node), is_bottom(is_bottom) {} - - bool operator==(const NodePrime &other) const - { - return node == other.node && is_bottom == other.is_bottom; - } - bool operator!=(const NodePrime &other) const - { - return !(*this == other); - } - [[nodiscard]] Hasher hash_into(Hasher h) const - { - std::pair p = {node, is_bottom}; - h.eat(p); - return h; - } - - static NodePrime top(RTLIL::SigBit node) - { - return NodePrime(node, /*is_bottom=*/false); - } - - static NodePrime bottom(RTLIL::SigBit node) - { - return NodePrime(node, /*is_bottom=*/true); - } - - NodePrime as_top() const - { - log_assert(is_bottom); - return top(node); - } - - NodePrime as_bottom() const - { - log_assert(!is_bottom); - return bottom(node); - } - }; - - bool find_augmenting_path(bool commit) - { - NodePrime source_prime = {source, true}; - NodePrime sink_prime = {sink, false}; - vector path = {source_prime}; - pool visited = {}; - bool found; - do { - found = false; - - auto node_prime = path.back(); - visited.insert(node_prime); - - if (!node_prime.is_bottom) // vt - { - if (!visited[node_prime.as_bottom()] && node_flow[node_prime.node] < MAX_NODE_FLOW) - { - path.push_back(node_prime.as_bottom()); - found = true; - } - else - { - for (auto node_pred : edges_bw[node_prime.node]) - { - if (!visited[NodePrime::bottom(node_pred)] && edge_flow[{node_pred, node_prime.node}] > 0) - { - path.push_back(NodePrime::bottom(node_pred)); - found = true; - break; - } - } - } - } - else // vb - { - if (!visited[node_prime.as_top()] && node_flow[node_prime.node] > 0) - { - path.push_back(node_prime.as_top()); - found = true; - } - else - { - for (auto node_succ : edges_fw[node_prime.node]) - { - if (!visited[NodePrime::top(node_succ)] /* && edge_flow[...] < ∞ */) - { - path.push_back(NodePrime::top(node_succ)); - found = true; - break; - } - } - } - } - - if (!found && path.size() > 1) - { - path.pop_back(); - found = true; - } - } while(path.back() != sink_prime && found); - - if (commit && path.back() == sink_prime) - { - auto prev_prime = path.front(); - for (auto node_prime : path) - { - if (node_prime == source_prime) - continue; - - log_assert(prev_prime.is_bottom ^ node_prime.is_bottom); - if (prev_prime.node == node_prime.node) - { - auto node = node_prime.node; - if (!prev_prime.is_bottom && node_prime.is_bottom) - { - log_assert(node_flow[node] == 0); - node_flow[node]++; - } - else - { - log_assert(node_flow[node] != 0); - node_flow[node]--; - } - } - else - { - if (prev_prime.is_bottom && !node_prime.is_bottom) - { - log_assert(true /* edge_flow[...] < ∞ */); - edge_flow[{prev_prime.node, node_prime.node}]++; - } - else - { - log_assert((edge_flow[{node_prime.node, prev_prime.node}] > 0)); - edge_flow[{node_prime.node, prev_prime.node}]--; - } - } - prev_prime = node_prime; - } - - node_flow[source]++; - node_flow[sink]++; - } - return path.back() == sink_prime; - } - - int maximum_flow(int order) - { - int flow = 0; - while (flow < order && find_augmenting_path(/*commit=*/true)) - flow++; - return flow + find_augmenting_path(/*commit=*/false); - } - - pair, pool> edge_cut() - { - pool x = {source}, xi; // X and X̅ in the paper - - NodePrime source_prime = {source, true}; - pool visited; - vector worklist = {source_prime}; - while (!worklist.empty()) - { - auto node_prime = worklist.back(); - worklist.pop_back(); - if (visited[node_prime]) - continue; - visited.insert(node_prime); - - if (!node_prime.is_bottom) - x.insert(node_prime.node); - - // Mincut is constructed by traversing a graph in an undirected way along forward edges that aren't full, or backward edges - // that aren't empty. - if (!node_prime.is_bottom) // top - { - if (node_flow[node_prime.node] < MAX_NODE_FLOW) - worklist.push_back(node_prime.as_bottom()); - for (auto node_pred : edges_bw[node_prime.node]) - if (edge_flow[{node_pred, node_prime.node}] > 0) - worklist.push_back(NodePrime::bottom(node_pred)); - } - else // bottom - { - if (node_flow[node_prime.node] > 0) - worklist.push_back(node_prime.as_top()); - for (auto node_succ : edges_fw[node_prime.node]) - if (true /* edge_flow[...] < ∞ */) - worklist.push_back(NodePrime::top(node_succ)); - } - } - - for (auto node : nodes) - if (!x[node]) - xi.insert(node); - - for (auto collapsed_node : collapsed[sink]) - xi.insert(collapsed_node); - - log_assert(x[source] && !xi[source]); - log_assert(!x[sink] && xi[sink]); - return {x, xi}; - } -}; - -struct FlowmapWorker -{ - int order; - int r_alpha, r_beta, r_gamma; - bool debug, debug_relax; - - RTLIL::Module *module; - SigMap sigmap; - ModIndex index; - - dict node_origins; - - // Gate IR - pool nodes, inputs, outputs; - dict> edges_fw, edges_bw; - dict labels; - - // LUT IR - pool lut_nodes; - dict> lut_gates; - dict> lut_edges_fw, lut_edges_bw; - dict lut_depths, lut_altitudes, lut_slacks; - - int gate_count = 0, lut_count = 0, packed_count = 0; - int gate_area = 0, lut_area = 0; - - enum class GraphMode { - Label, - Cut, - Slack, - }; - - void dump_dot_graph(string filename, GraphMode mode, - pool subgraph_nodes = {}, dict> subgraph_edges = {}, - dict> collapsed = {}, - pair, pool> cut = {}) - { - if (subgraph_nodes.empty()) - subgraph_nodes = nodes; - if (subgraph_edges.empty()) - subgraph_edges = edges_fw; - - auto node_style = [&](RTLIL::SigBit node) { - string label = log_signal(node); - for (auto collapsed_node : collapsed[node]) - if (collapsed_node != node) - label += stringf(" %s", log_signal(collapsed_node)); - switch (mode) - { - case GraphMode::Label: - if (labels[node] == -1) - { - label += "\nl=?"; - return GraphStyle{label}; - } - else - { - label += stringf("\nl=%d", labels[node]); - string fillcolor = stringf("/set311/%d", 1 + labels[node] % 11); - return GraphStyle{label, "", fillcolor}; - } - - case GraphMode::Cut: - if (cut.first[node]) - return GraphStyle{label, "blue"}; - if (cut.second[node]) - return GraphStyle{label, "red"}; - return GraphStyle{label}; - - case GraphMode::Slack: - label += stringf("\nd=%d a=%d\ns=%d", lut_depths[node], lut_altitudes[node], lut_slacks[node]); - return GraphStyle{label, lut_slacks[node] == 0 ? "red" : "black"}; - } - return GraphStyle{label}; - }; - auto edge_style = [&](RTLIL::SigBit, RTLIL::SigBit) { - return GraphStyle{}; - }; - ::dump_dot_graph(filename, subgraph_nodes, subgraph_edges, inputs, outputs, node_style, edge_style, module->name.str()); - } - - void dump_dot_lut_graph(string filename, GraphMode mode) - { - pool lut_and_input_nodes; - lut_and_input_nodes.insert(lut_nodes.begin(), lut_nodes.end()); - lut_and_input_nodes.insert(inputs.begin(), inputs.end()); - dump_dot_graph(filename, mode, lut_and_input_nodes, lut_edges_fw, lut_gates); - } - - pool find_subgraph(RTLIL::SigBit sink) - { - pool subgraph; - pool worklist = {sink}; - while (!worklist.empty()) - { - auto node = worklist.pop(); - subgraph.insert(node); - for (auto source : edges_bw[node]) - { - if (!subgraph[source]) - worklist.insert(source); - } - } - return subgraph; - } - - FlowGraph build_flow_graph(RTLIL::SigBit sink, int p) - { - FlowGraph flow_graph; - flow_graph.sink = sink; - - pool worklist = {sink}, visited; - while (!worklist.empty()) - { - auto node = worklist.pop(); - visited.insert(node); - - auto collapsed_node = labels[node] == p ? sink : node; - if (node != collapsed_node) - flow_graph.collapsed[collapsed_node].insert(node); - flow_graph.nodes.insert(collapsed_node); - - for (auto node_pred : edges_bw[node]) - { - auto collapsed_node_pred = labels[node_pred] == p ? sink : node_pred; - if (node_pred != collapsed_node_pred) - flow_graph.collapsed[collapsed_node_pred].insert(node_pred); - if (collapsed_node != collapsed_node_pred) - { - flow_graph.edges_bw[collapsed_node].insert(collapsed_node_pred); - flow_graph.edges_fw[collapsed_node_pred].insert(collapsed_node); - } - if (inputs[node_pred]) - { - flow_graph.edges_bw[collapsed_node_pred].insert(flow_graph.source); - flow_graph.edges_fw[flow_graph.source].insert(collapsed_node_pred); - } - - if (!visited[node_pred]) - worklist.insert(node_pred); - } - } - return flow_graph; - } - - void discover_nodes(pool cell_types) - { - for (auto cell : module->selected_cells()) - { - if (!cell_types[cell->type]) - continue; - - if (!cell->known()) - log_error("Cell %s (%s.%s) is unknown.\n", cell->type, module, cell); - - pool fanout; - for (auto conn : cell->connections()) - { - if (!cell->output(conn.first)) continue; - int offset = -1; - for (auto bit : conn.second) - { - offset++; - if (!bit.wire) continue; - auto mapped_bit = sigmap(bit); - if (nodes[mapped_bit]) - log_error("Multiple drivers found for wire %s.\n", log_signal(mapped_bit)); - nodes.insert(mapped_bit); - node_origins[mapped_bit] = ModIndex::PortInfo(cell, conn.first, offset); - fanout.insert(mapped_bit); - } - } - - int fanin = 0; - for (auto conn : cell->connections()) - { - if (!cell->input(conn.first)) continue; - for (auto bit : sigmap(conn.second)) - { - if (!bit.wire) continue; - for (auto fanout_bit : fanout) - { - edges_fw[bit].insert(fanout_bit); - edges_bw[fanout_bit].insert(bit); - } - fanin++; - } - } - - if (fanin > order) - log_error("Cell %s (%s.%s) with fan-in %d cannot be mapped to a %d-LUT.\n", - cell->type.c_str(), module, cell, fanin, order); - - gate_count++; - gate_area += 1 << fanin; - } - - for (auto edge : edges_fw) - { - if (!nodes[edge.first]) - { - inputs.insert(edge.first); - nodes.insert(edge.first); - } - } - - for (auto node : nodes) - { - auto node_info = index.query(node); - if (node_info->is_output && !inputs[node]) - outputs.insert(node); - for (auto port : node_info->ports) - if (!cell_types[port.cell->type] && !inputs[node]) - outputs.insert(node); - } - - if (debug) - { - dump_dot_graph("flowmap-initial.dot", GraphMode::Label); - log("Dumped initial graph to `flowmap-initial.dot`.\n"); - } - } - - void label_nodes() - { - for (auto node : nodes) - labels[node] = -1; - for (auto input : inputs) - { - if (input.wire->attributes.count(ID($flowmap_level))) - labels[input] = input.wire->attributes[ID($flowmap_level)].as_int(); - else - labels[input] = 0; - } - - pool worklist = nodes; - int debug_num = 0; - while (!worklist.empty()) - { - auto sink = worklist.pop(); - if (labels[sink] != -1) - continue; - - bool inputs_have_labels = true; - for (auto sink_input : edges_bw[sink]) - { - if (labels[sink_input] == -1) - { - inputs_have_labels = false; - break; - } - } - if (!inputs_have_labels) - continue; - - if (debug) - { - debug_num++; - log("Examining subgraph %d rooted in %s.\n", debug_num, log_signal(sink)); - } - - pool subgraph = find_subgraph(sink); - - int p = 1; - for (auto subgraph_node : subgraph) - p = max(p, labels[subgraph_node]); - - FlowGraph flow_graph = build_flow_graph(sink, p); - int flow = flow_graph.maximum_flow(order); - pool x, xi; - if (flow <= order) - { - labels[sink] = p; - auto cut = flow_graph.edge_cut(); - x = cut.first; - xi = cut.second; - } - else - { - labels[sink] = p + 1; - x = subgraph; - x.erase(sink); - xi.insert(sink); - } - lut_gates[sink] = xi; - - pool k; - for (auto xi_node : xi) - { - for (auto xi_node_pred : edges_bw[xi_node]) - if (x[xi_node_pred]) - k.insert(xi_node_pred); - } - log_assert((int)k.size() <= order); - lut_edges_bw[sink] = k; - for (auto k_node : k) - lut_edges_fw[k_node].insert(sink); - - if (debug) - { - log(" Maximum flow: %d. Assigned label %d.\n", flow, labels[sink]); - dump_dot_graph(stringf("flowmap-%d-sub.dot", debug_num), GraphMode::Cut, subgraph, {}, {}, {x, xi}); - log(" Dumped subgraph to `flowmap-%d-sub.dot`.\n", debug_num); - flow_graph.dump_dot_graph(stringf("flowmap-%d-flow.dot", debug_num)); - log(" Dumped flow graph to `flowmap-%d-flow.dot`.\n", debug_num); - log(" LUT inputs:"); - for (auto k_node : k) - log(" %s", log_signal(k_node)); - log(".\n"); - log(" LUT packed gates:"); - for (auto xi_node : xi) - log(" %s", log_signal(xi_node)); - log(".\n"); - } - - for (auto sink_succ : edges_fw[sink]) - worklist.insert(sink_succ); - } - - if (debug) - { - dump_dot_graph("flowmap-labeled.dot", GraphMode::Label); - log("Dumped labeled graph to `flowmap-labeled.dot`.\n"); - } - } - - int map_luts() - { - pool worklist = outputs; - while (!worklist.empty()) - { - auto lut_node = worklist.pop(); - lut_nodes.insert(lut_node); - for (auto input_node : lut_edges_bw[lut_node]) - if (!lut_nodes[input_node] && !inputs[input_node]) - worklist.insert(input_node); - } - - int depth = 0; - for (auto label : labels) - depth = max(depth, label.second); - log("Mapped to %d LUTs with maximum depth %d.\n", GetSize(lut_nodes), depth); - - if (debug) - { - dump_dot_lut_graph("flowmap-mapped.dot", GraphMode::Label); - log("Dumped mapped graph to `flowmap-mapped.dot`.\n"); - } - - return depth; - } - - void realize_derealize_lut(RTLIL::SigBit lut, pool *changed = nullptr) - { - pool worklist = {lut}; - while (!worklist.empty()) - { - auto lut = worklist.pop(); - if (inputs[lut]) - continue; - - bool realized_successors = false; - for (auto lut_succ : lut_edges_fw[lut]) - if (lut_nodes[lut_succ]) - realized_successors = true; - - if (realized_successors && !lut_nodes[lut]) - lut_nodes.insert(lut); - else if (!realized_successors && lut_nodes[lut]) - lut_nodes.erase(lut); - else - continue; - - for (auto lut_pred : lut_edges_bw[lut]) - worklist.insert(lut_pred); - - if (changed) - changed->insert(lut); - } - } - - void add_lut_edge(RTLIL::SigBit pred, RTLIL::SigBit succ, pool *changed = nullptr) - { - log_assert(!lut_edges_fw[pred][succ] && !lut_edges_bw[succ][pred]); - log_assert((int)lut_edges_bw[succ].size() < order); - - lut_edges_fw[pred].insert(succ); - lut_edges_bw[succ].insert(pred); - realize_derealize_lut(pred, changed); - - if (changed) - { - changed->insert(pred); - changed->insert(succ); - } - } - - void remove_lut_edge(RTLIL::SigBit pred, RTLIL::SigBit succ, pool *changed = nullptr) - { - log_assert(lut_edges_fw[pred][succ] && lut_edges_bw[succ][pred]); - - lut_edges_fw[pred].erase(succ); - lut_edges_bw[succ].erase(pred); - realize_derealize_lut(pred, changed); - - if (changed) - { - if (lut_nodes[pred]) - changed->insert(pred); - changed->insert(succ); - } - } - - pair, pool> cut_lut_at_gate(RTLIL::SigBit lut, RTLIL::SigBit lut_gate) - { - pool gate_inputs = lut_edges_bw[lut]; - pool other_inputs; - pool worklist = {lut}; - while (!worklist.empty()) - { - auto node = worklist.pop(); - for (auto node_pred : edges_bw[node]) - { - if (node_pred == lut_gate) - continue; - if (lut_gates[lut][node_pred]) - worklist.insert(node_pred); - else - { - gate_inputs.erase(node_pred); - other_inputs.insert(node_pred); - } - } - } - return {gate_inputs, other_inputs}; - } - - void compute_lut_distances(dict &lut_distances, bool forward, - pool initial = {}, pool *changed = nullptr) - { - pool terminals = forward ? inputs : outputs; - auto &lut_edges_next = forward ? lut_edges_fw : lut_edges_bw; - auto &lut_edges_prev = forward ? lut_edges_bw : lut_edges_fw; - - if (initial.empty()) - initial = terminals; - for (auto node : initial) - lut_distances.erase(node); - - pool worklist = initial; - while (!worklist.empty()) - { - auto lut = worklist.pop(); - int lut_distance = 0; - if (forward && inputs[lut]) - lut_distance = labels[lut]; // to support (* $flowmap_level=n *) - for (auto lut_prev : lut_edges_prev[lut]) - if ((lut_nodes[lut_prev] || inputs[lut_prev]) && lut_distances.count(lut_prev)) - lut_distance = max(lut_distance, lut_distances[lut_prev] + 1); - if (!lut_distances.count(lut) || lut_distances[lut] != lut_distance) - { - lut_distances[lut] = lut_distance; - if (changed != nullptr && !inputs[lut]) - changed->insert(lut); - for (auto lut_next : lut_edges_next[lut]) - if (lut_nodes[lut_next] || inputs[lut_next]) - worklist.insert(lut_next); - } - } - } - - void check_lut_distances(const dict &lut_distances, bool forward) - { - dict gold_lut_distances; - compute_lut_distances(gold_lut_distances, forward); - for (auto lut_distance : lut_distances) - if (lut_nodes[lut_distance.first]) - log_assert(lut_distance.second == gold_lut_distances[lut_distance.first]); - } - - // LUT depth is the length of the longest path from any input in LUT fan-in to LUT. - // LUT altitude (for lack of a better term) is the length of the longest path from LUT to any output in LUT fan-out. - void update_lut_depths_altitudes(pool worklist = {}, pool *changed = nullptr) - { - compute_lut_distances(lut_depths, /*forward=*/true, worklist, changed); - compute_lut_distances(lut_altitudes, /*forward=*/false, worklist, changed); - if (debug_relax && !worklist.empty()) { - check_lut_distances(lut_depths, /*forward=*/true); - check_lut_distances(lut_altitudes, /*forward=*/false); - } - } - - // LUT critical output set is the set of outputs whose depth will increase (equivalently, slack will decrease) if the depth of - // the LUT increases. (This is referred to as RPOv for LUTv in the paper.) - void compute_lut_critical_outputs(dict> &lut_critical_outputs, - pool worklist = {}) - { - if (worklist.empty()) - worklist = lut_nodes; - - while (!worklist.empty()) - { - bool updated_some = false; - for (auto lut : worklist) - { - if (outputs[lut]) - lut_critical_outputs[lut] = {lut}; - else - { - bool all_succ_computed = true; - lut_critical_outputs[lut] = {}; - for (auto lut_succ : lut_edges_fw[lut]) - { - if (lut_nodes[lut_succ] && lut_depths[lut_succ] == lut_depths[lut] + 1) - { - if (lut_critical_outputs.count(lut_succ)) - lut_critical_outputs[lut].insert(lut_critical_outputs[lut_succ].begin(), lut_critical_outputs[lut_succ].end()); - else - { - all_succ_computed = false; - break; - } - } - } - if (!all_succ_computed) - { - lut_critical_outputs.erase(lut); - continue; - } - } - worklist.erase(lut); - updated_some = true; - } - log_assert(updated_some); - } - } - - // Invalidating LUT critical output sets is tricky, because increasing the depth of a LUT may take other, adjacent LUTs off the critical - // path to the output. Conservatively, if we increase depth of some LUT, every LUT in its input cone needs to have its critical output - // set invalidated, too. - pool invalidate_lut_critical_outputs(dict> &lut_critical_outputs, - pool worklist) - { - pool changed; - while (!worklist.empty()) - { - auto lut = worklist.pop(); - changed.insert(lut); - lut_critical_outputs.erase(lut); - for (auto lut_pred : lut_edges_bw[lut]) - { - if (lut_nodes[lut_pred] && !changed[lut_pred]) - { - changed.insert(lut_pred); - worklist.insert(lut_pred); - } - } - } - return changed; - } - - void check_lut_critical_outputs(const dict> &lut_critical_outputs) - { - dict> gold_lut_critical_outputs; - compute_lut_critical_outputs(gold_lut_critical_outputs); - for (auto lut_critical_output : lut_critical_outputs) - if (lut_nodes[lut_critical_output.first]) - log_assert(lut_critical_output.second == gold_lut_critical_outputs[lut_critical_output.first]); - } - - void update_lut_critical_outputs(dict> &lut_critical_outputs, - pool worklist = {}) - { - if (!worklist.empty()) - { - pool invalidated = invalidate_lut_critical_outputs(lut_critical_outputs, worklist); - compute_lut_critical_outputs(lut_critical_outputs, invalidated); - check_lut_critical_outputs(lut_critical_outputs); - } - else - compute_lut_critical_outputs(lut_critical_outputs); - } - - void update_breaking_node_potentials(dict> &potentials, - const dict> &lut_critical_outputs) - { - for (auto lut : lut_nodes) - { - if (potentials.count(lut)) - continue; - if (lut_gates[lut].size() == 1 || lut_slacks[lut] == 0) - continue; - - if (debug_relax) - log(" Computing potentials for LUT %s.\n", log_signal(lut)); - - for (auto lut_gate : lut_gates[lut]) - { - if (lut == lut_gate) - continue; - - if (debug_relax) - log(" Considering breaking node %s.\n", log_signal(lut_gate)); - - int r_ex, r_im, r_slk; - - auto cut_inputs = cut_lut_at_gate(lut, lut_gate); - pool gate_inputs = cut_inputs.first, other_inputs = cut_inputs.second; - if (gate_inputs.empty() && (int)other_inputs.size() >= order) - { - if (debug_relax) - log(" Breaking would result in a (k+1)-LUT.\n"); - continue; - } - - pool elim_fanin_luts; - for (auto gate_input : gate_inputs) - { - if (lut_edges_fw[gate_input].size() == 1) - { - log_assert(lut_edges_fw[gate_input][lut]); - elim_fanin_luts.insert(gate_input); - } - } - if (debug_relax) - { - if (!lut_nodes[lut_gate]) - log(" Breaking requires a new LUT.\n"); - if (!gate_inputs.empty()) - { - log(" Breaking eliminates LUT inputs"); - for (auto gate_input : gate_inputs) - log(" %s", log_signal(gate_input)); - log(".\n"); - } - if (!elim_fanin_luts.empty()) - { - log(" Breaking eliminates fan-in LUTs"); - for (auto elim_fanin_lut : elim_fanin_luts) - log(" %s", log_signal(elim_fanin_lut)); - log(".\n"); - } - } - r_ex = (lut_nodes[lut_gate] ? 0 : -1) + elim_fanin_luts.size(); - - pool> maybe_mergeable_luts; - - // Try to merge LUTv with one of its successors. - RTLIL::SigBit last_lut_succ; - int fanout = 0; - for (auto lut_succ : lut_edges_fw[lut]) - { - if (lut_nodes[lut_succ]) - { - fanout++; - last_lut_succ = lut_succ; - } - } - if (fanout == 1) - maybe_mergeable_luts.insert({lut, last_lut_succ}); - - // Try to merge LUTv with one of its predecessors. - for (auto lut_pred : other_inputs) - { - int fanout = 0; - for (auto lut_pred_succ : lut_edges_fw[lut_pred]) - if (lut_nodes[lut_pred_succ] || lut_pred_succ == lut_gate) - fanout++; - if (fanout == 1) - maybe_mergeable_luts.insert({lut_pred, lut}); - } - - // Try to merge LUTw with one of its predecessors. - for (auto lut_gate_pred : lut_edges_bw[lut_gate]) - { - int fanout = 0; - for (auto lut_gate_pred_succ : lut_edges_fw[lut_gate_pred]) - if (lut_nodes[lut_gate_pred_succ] || lut_gate_pred_succ == lut_gate) - fanout++; - if (fanout == 1) - maybe_mergeable_luts.insert({lut_gate_pred, lut_gate}); - } - - r_im = 0; - for (auto maybe_mergeable_pair : maybe_mergeable_luts) - { - log_assert(lut_edges_fw[maybe_mergeable_pair.first][maybe_mergeable_pair.second]); - pool unique_inputs; - for (auto fst_lut_pred : lut_edges_bw[maybe_mergeable_pair.first]) - if (lut_nodes[fst_lut_pred]) - unique_inputs.insert(fst_lut_pred); - for (auto snd_lut_pred : lut_edges_bw[maybe_mergeable_pair.second]) - if (lut_nodes[snd_lut_pred]) - unique_inputs.insert(snd_lut_pred); - unique_inputs.erase(maybe_mergeable_pair.first); - if ((int)unique_inputs.size() <= order) - { - if (debug_relax) - log(" Breaking may allow merging %s and %s.\n", - log_signal(maybe_mergeable_pair.first), log_signal(maybe_mergeable_pair.second)); - r_im++; - } - } - - int lut_gate_depth; - if (lut_nodes[lut_gate]) - lut_gate_depth = lut_depths[lut_gate]; - else - { - lut_gate_depth = 0; - for (auto lut_gate_pred : lut_edges_bw[lut_gate]) - lut_gate_depth = max(lut_gate_depth, lut_depths[lut_gate_pred] + 1); - } - if (lut_depths[lut] >= lut_gate_depth + 1) - r_slk = 0; - else - { - int depth_delta = lut_gate_depth + 1 - lut_depths[lut]; - if (depth_delta > lut_slacks[lut]) - { - if (debug_relax) - log(" Breaking would increase depth by %d, which is more than available slack.\n", depth_delta); - continue; - } - - if (debug_relax) - { - log(" Breaking increases depth of LUT by %d.\n", depth_delta); - if (lut_critical_outputs.at(lut).size()) - { - log(" Breaking decreases slack of outputs"); - for (auto lut_critical_output : lut_critical_outputs.at(lut)) - { - log(" %s", log_signal(lut_critical_output)); - log_assert(lut_slacks[lut_critical_output] > 0); - } - log(".\n"); - } - } - r_slk = lut_critical_outputs.at(lut).size() * depth_delta; - } - - int p = 100 * (r_alpha * r_ex + r_beta * r_im + r_gamma) / (r_slk + 1); - if (debug_relax) - log(" Potential for breaking node %s: %d (Rex=%d, Rim=%d, Rslk=%d).\n", - log_signal(lut_gate), p, r_ex, r_im, r_slk); - potentials[lut][lut_gate] = p; - } - } - } - - bool relax_depth_for_bound(bool first, int depth_bound, dict> &lut_critical_outputs) - { - int initial_count = GetSize(lut_nodes); - - for (auto node : lut_nodes) - { - lut_slacks[node] = depth_bound - (lut_depths[node] + lut_altitudes[node]); - log_assert(lut_slacks[node] >= 0); - } - if (debug) - { - dump_dot_lut_graph(stringf("flowmap-relax-%d-initial.dot", depth_bound), GraphMode::Slack); - log(" Dumped initial slack graph to `flowmap-relax-%d-initial.dot`.\n", depth_bound); - } - - dict> potentials; - for (int break_num = 1; ; break_num++) - { - update_breaking_node_potentials(potentials, lut_critical_outputs); - - if (potentials.empty()) - { - log(" Relaxed to %d (+%d) LUTs.\n", GetSize(lut_nodes), GetSize(lut_nodes) - initial_count); - if (!first && break_num == 1) - { - log(" Design fully relaxed.\n"); - return true; - } - else - { - log(" Slack exhausted.\n"); - break; - } - } - - RTLIL::SigBit breaking_lut, breaking_gate; - int best_potential = INT_MIN; - for (auto lut_gate_potentials : potentials) - { - for (auto gate_potential : lut_gate_potentials.second) - { - if (gate_potential.second > best_potential) - { - breaking_lut = lut_gate_potentials.first; - breaking_gate = gate_potential.first; - best_potential = gate_potential.second; - } - } - } - log(" Breaking LUT %s to %s LUT %s (potential %d).\n", - log_signal(breaking_lut), lut_nodes[breaking_gate] ? "reuse" : "extract", log_signal(breaking_gate), best_potential); - - if (debug_relax) - log(" Removing breaking gate %s from LUT.\n", log_signal(breaking_gate)); - lut_gates[breaking_lut].erase(breaking_gate); - - auto cut_inputs = cut_lut_at_gate(breaking_lut, breaking_gate); - pool gate_inputs = cut_inputs.first; - - pool worklist = lut_gates[breaking_lut]; - pool elim_gates = gate_inputs; - while (!worklist.empty()) - { - auto lut_gate = worklist.pop(); - bool all_gate_preds_elim = true; - for (auto lut_gate_pred : edges_bw[lut_gate]) - if (!elim_gates[lut_gate_pred]) - all_gate_preds_elim = false; - if (all_gate_preds_elim) - { - if (debug_relax) - log(" Removing gate %s from LUT.\n", log_signal(lut_gate)); - lut_gates[breaking_lut].erase(lut_gate); - for (auto lut_gate_succ : edges_fw[lut_gate]) - worklist.insert(lut_gate_succ); - } - } - log_assert(!lut_gates[breaking_lut].empty()); - - pool directly_affected_nodes = {breaking_lut}; - for (auto gate_input : gate_inputs) - { - if (debug_relax) - log(" Removing LUT edge %s -> %s.\n", log_signal(gate_input), log_signal(breaking_lut)); - remove_lut_edge(gate_input, breaking_lut, &directly_affected_nodes); - } - if (debug_relax) - log(" Adding LUT edge %s -> %s.\n", log_signal(breaking_gate), log_signal(breaking_lut)); - add_lut_edge(breaking_gate, breaking_lut, &directly_affected_nodes); - - if (debug_relax) - log(" Updating slack and potentials.\n"); - - pool indirectly_affected_nodes = {}; - update_lut_depths_altitudes(directly_affected_nodes, &indirectly_affected_nodes); - update_lut_critical_outputs(lut_critical_outputs, indirectly_affected_nodes); - for (auto node : indirectly_affected_nodes) - { - lut_slacks[node] = depth_bound - (lut_depths[node] + lut_altitudes[node]); - log_assert(lut_slacks[node] >= 0); - if (debug_relax) - log(" LUT %s now has depth %d and slack %d.\n", log_signal(node), lut_depths[node], lut_slacks[node]); - } - - worklist = indirectly_affected_nodes; - pool visited; - while (!worklist.empty()) - { - auto node = worklist.pop(); - visited.insert(node); - potentials.erase(node); - // We are invalidating the entire output cone of the gate IR node, not just of the LUT IR node. This is done to also invalidate - // all LUTs that could contain one of the indirectly affected nodes as a *part* of them, as they may not be in the output cone - // of any of the LUT IR nodes, e.g. if we have a LUT IR node A and node B as predecessors of node C, where node B includes all - // gates from node A. - for (auto node_succ : edges_fw[node]) - if (!visited[node_succ]) - worklist.insert(node_succ); - } - - if (debug) - { - dump_dot_lut_graph(stringf("flowmap-relax-%d-break-%d.dot", depth_bound, break_num), GraphMode::Slack); - log(" Dumped slack graph after break %d to `flowmap-relax-%d-break-%d.dot`.\n", break_num, depth_bound, break_num); - } - } - - return false; - } - - void optimize_area(int depth, int optarea) - { - dict> lut_critical_outputs; - update_lut_depths_altitudes(); - update_lut_critical_outputs(lut_critical_outputs); - - for (int depth_bound = depth; depth_bound <= depth + optarea; depth_bound++) - { - log("Relaxing with depth bound %d.\n", depth_bound); - bool fully_relaxed = relax_depth_for_bound(depth_bound == depth, depth_bound, lut_critical_outputs); - - if (fully_relaxed) - break; - } - } - - void pack_cells(int minlut) - { - ConstEval ce(module); - for (auto input_node : inputs) - ce.stop(input_node); - - pool mapped_nodes; - for (auto node : lut_nodes) - { - if (node_origins.count(node)) - { - auto origin = node_origins[node]; - if (origin.cell->getPort(origin.port).size() == 1) - log("Packing %s.%s.%s (%s).\n", - module, origin.cell, origin.port.c_str(), log_signal(node)); - else - log("Packing %s.%s.%s [%d] (%s).\n", - module, origin.cell, origin.port.c_str(), origin.offset, log_signal(node)); - } - else - { - log("Packing %s.%s.\n", module, log_signal(node)); - } - - for (auto gate_node : lut_gates[node]) - { - log_assert(node_origins.count(gate_node)); - - if (gate_node == node) - continue; - - auto gate_origin = node_origins[gate_node]; - if (gate_origin.cell->getPort(gate_origin.port).size() == 1) - log(" Packing %s.%s.%s (%s).\n", - module, gate_origin.cell, gate_origin.port.c_str(), log_signal(gate_node)); - else - log(" Packing %s.%s.%s [%d] (%s).\n", - module, gate_origin.cell, gate_origin.port.c_str(), gate_origin.offset, log_signal(gate_node)); - } - - vector input_nodes(lut_edges_bw[node].begin(), lut_edges_bw[node].end()); - RTLIL::Const lut_table(State::Sx, max(1 << input_nodes.size(), 1 << minlut)); - unsigned const mask = 1 << input_nodes.size(); - for (unsigned i = 0; i < mask; i++) - { - ce.push(); - for (size_t n = 0; n < input_nodes.size(); n++) - ce.set(input_nodes[n], ((i >> n) & 1) ? State::S1 : State::S0); - - RTLIL::SigSpec value = node, undef; - if (!ce.eval(value, undef)) - { - string env; - for (auto input_node : input_nodes) - env += stringf(" %s = %s\n", log_signal(input_node), log_signal(ce.values_map(input_node))); - log_error("Cannot evaluate %s because %s is not defined.\nEvaluation environment:\n%s", - log_signal(node), log_signal(undef), env.c_str()); - } - - lut_table.set(i, value.as_bool() ? State::S1 : State::S0); - ce.pop(); - } - - RTLIL::SigSpec lut_a, lut_y = node; - for (auto input_node : input_nodes) - lut_a.append(input_node); - if ((int)input_nodes.size() < minlut) - lut_a.append(RTLIL::Const(State::Sx, minlut - input_nodes.size())); - - RTLIL::Cell *lut = module->addLut(NEW_ID, lut_a, lut_y, lut_table); - mapped_nodes.insert(node); - for (auto gate_node : lut_gates[node]) - { - auto gate_origin = node_origins[gate_node]; - lut->add_strpool_attribute(ID::src, gate_origin.cell->get_strpool_attribute(ID::src)); - packed_count++; - } - lut_count++; - lut_area += lut_table.size(); - - if ((int)input_nodes.size() >= minlut) - log(" Packed into a %d-LUT %s.%s.\n", GetSize(input_nodes), module, lut); - else - log(" Packed into a %d-LUT %s.%s (implemented as %d-LUT).\n", GetSize(input_nodes), module, lut, minlut); - } - - for (auto node : mapped_nodes) - { - auto origin = node_origins[node]; - RTLIL::SigSpec driver = origin.cell->getPort(origin.port); - driver[origin.offset] = module->addWire(NEW_ID); - origin.cell->setPort(origin.port, driver); - } - } - - FlowmapWorker(int order, int minlut, pool cell_types, int r_alpha, int r_beta, int r_gamma, - bool relax, int optarea, bool debug, bool debug_relax, - RTLIL::Module *module) : - order(order), r_alpha(r_alpha), r_beta(r_beta), r_gamma(r_gamma), debug(debug), debug_relax(debug_relax), - module(module), sigmap(module), index(module) - { - log("Labeling cells.\n"); - discover_nodes(cell_types); - label_nodes(); - int depth = map_luts(); - - if (relax) - { - log("\n"); - log("Optimizing area.\n"); - optimize_area(depth, optarea); - } - - log("\n"); - log("Packing cells.\n"); - pack_cells(minlut); - } -}; - -static void split(std::vector &tokens, const std::string &text, char sep) -{ - size_t start = 0, end = 0; - while ((end = text.find(sep, start)) != std::string::npos) { - tokens.push_back(text.substr(start, end - start)); - start = end + 1; - } - tokens.push_back(text.substr(start)); -} - -struct FlowmapPass : public Pass { - FlowmapPass() : Pass("flowmap", "pack LUTs with FlowMap") { } - void help() override - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" flowmap [options] [selection]\n"); - log("\n"); - log("This pass uses the FlowMap technology mapping algorithm to pack logic gates\n"); - log("into k-LUTs with optimal depth. It allows mapping any circuit elements that can\n"); - log("be evaluated with the `eval` pass, including cells with multiple output ports\n"); - log("and multi-bit input and output ports.\n"); - log("\n"); - log(" -maxlut k\n"); - log(" perform technology mapping for a k-LUT architecture. if not specified,\n"); - log(" defaults to 3.\n"); - log("\n"); - log(" -minlut n\n"); - log(" only produce n-input or larger LUTs. if not specified, defaults to 1.\n"); - log("\n"); - log(" -cells [,,...]\n"); - log(" map specified cells. if not specified, maps $_NOT_, $_AND_, $_OR_,\n"); - log(" $_XOR_ and $_MUX_, which are the outputs of the `simplemap` pass.\n"); - log("\n"); - log(" -relax\n"); - log(" perform depth relaxation and area minimization.\n"); - log("\n"); - log(" -r-alpha n, -r-beta n, -r-gamma n\n"); - log(" parameters of depth relaxation heuristic potential function.\n"); - log(" if not specified, alpha=8, beta=2, gamma=1.\n"); - log("\n"); - log(" -optarea n\n"); - log(" optimize for area by trading off at most n logic levels for fewer LUTs.\n"); - log(" n may be zero, to optimize for area without increasing depth.\n"); - log(" implies -relax.\n"); - log("\n"); - log(" -debug\n"); - log(" dump intermediate graphs.\n"); - log("\n"); - log(" -debug-relax\n"); - log(" explain decisions performed during depth relaxation.\n"); - log("\n"); - } - void execute(std::vector args, RTLIL::Design *design) override - { - int order = 3; - int minlut = 1; - vector cells; - bool relax = false; - int r_alpha = 8, r_beta = 2, r_gamma = 1; - int optarea = 0; - bool debug = false, debug_relax = false; - - size_t argidx; - for (argidx = 1; argidx < args.size(); argidx++) - { - if (args[argidx] == "-maxlut" && argidx + 1 < args.size()) - { - order = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-minlut" && argidx + 1 < args.size()) - { - minlut = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-cells" && argidx + 1 < args.size()) - { - split(cells, args[++argidx], ','); - continue; - } - if (args[argidx] == "-relax") - { - relax = true; - continue; - } - if (args[argidx] == "-r-alpha" && argidx + 1 < args.size()) - { - r_alpha = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-r-beta" && argidx + 1 < args.size()) - { - r_beta = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-r-gamma" && argidx + 1 < args.size()) - { - r_gamma = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-optarea" && argidx + 1 < args.size()) - { - relax = true; - optarea = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-debug") - { - debug = true; - continue; - } - if (args[argidx] == "-debug-relax") - { - debug = debug_relax = true; - continue; - } - break; - } - extra_args(args, argidx, design); - - pool cell_types; - if (!cells.empty()) - { - for (auto &cell : cells) - cell_types.insert(cell); - } - else - { - cell_types = {ID($_NOT_), ID($_AND_), ID($_OR_), ID($_XOR_), ID($_MUX_)}; - } - - const char *algo_r = relax ? "-r" : ""; - log_header(design, "Executing FLOWMAP pass (pack LUTs with FlowMap%s).\n", algo_r); - - int gate_count = 0, lut_count = 0, packed_count = 0; - int gate_area = 0, lut_area = 0; - for (auto module : design->selected_modules()) - { - FlowmapWorker worker(order, minlut, cell_types, r_alpha, r_beta, r_gamma, relax, optarea, debug, debug_relax, module); - gate_count += worker.gate_count; - lut_count += worker.lut_count; - packed_count += worker.packed_count; - gate_area += worker.gate_area; - lut_area += worker.lut_area; - } - - log("\n"); - log("Packed %d cells (%d of them duplicated) into %d LUTs.\n", packed_count, packed_count - gate_count, lut_count); - log("Solution takes %.1f%% of original gate area.\n", lut_area * 100.0 / gate_area); - } -} FlowmapPass; - -PRIVATE_NAMESPACE_END diff --git a/techlibs/common/CMakeLists.txt b/techlibs/common/CMakeLists.txt index 48999e711..89da53883 100644 --- a/techlibs/common/CMakeLists.txt +++ b/techlibs/common/CMakeLists.txt @@ -13,7 +13,6 @@ yosys_pass(synth check clean flatten - flowmap fsm hierarchy memory diff --git a/techlibs/common/synth.cc b/techlibs/common/synth.cc index 3656218c5..31986f25b 100644 --- a/techlibs/common/synth.cc +++ b/techlibs/common/synth.cc @@ -92,9 +92,6 @@ struct SynthPass : public ScriptPass { log(" -abc9\n"); log(" use new ABC9 flow (EXPERIMENTAL)\n"); log("\n"); - log(" -flowmap\n"); - log(" use FlowMap LUT techmapping instead of ABC\n"); - log("\n"); log(" -no-rw-check\n"); log(" marks all recognized read ports as \"return don't-care value on\n"); log(" read/write collision\" (same result as setting the no_rw_check\n"); @@ -115,7 +112,7 @@ struct SynthPass : public ScriptPass { } string top_module, fsm_opts, memory_opts, abc, latches_opt; - bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth, arith_tree, hieropt, relative_share; + bool autotop, flatten, noalumacc, nofsm, noabc, noshare, booth, arith_tree, hieropt, relative_share; int lut; std::vector techmap_maps; @@ -133,7 +130,6 @@ struct SynthPass : public ScriptPass { nofsm = false; noabc = false; noshare = false; - flowmap = false; booth = false; arith_tree = false; hieropt = false; @@ -216,10 +212,6 @@ struct SynthPass : public ScriptPass { abc = "abc9"; continue; } - if (args[argidx] == "-flowmap") { - flowmap = true; - continue; - } if (args[argidx] == "-no-rw-check") { memory_opts += " -no-rw-check"; continue; @@ -246,8 +238,6 @@ struct SynthPass : public ScriptPass { if (abc == "abc9" && !lut) log_cmd_error("ABC9 flow only supported for FPGA synthesis (using '-lut' option)\n"); - if (flowmap && !lut) - log_cmd_error("FlowMap is only supported for FPGA synthesis (using '-lut' option)\n"); log_header(design, "Executing SYNTH pass.\n"); log_push(); @@ -334,16 +324,13 @@ struct SynthPass : public ScriptPass { if (help_mode) { run(techmap_cmd + " -map +/gate2lut.v", "(if -noabc and -lut)"); run("clean; opt_lut", " (if -noabc and -lut)"); - run("flowmap -maxlut K", " (if -flowmap and -lut)"); } else if (noabc && lut) { run(stringf("%s -map +/gate2lut.v -D LUT_WIDTH=%d", techmap_cmd, lut)); run("clean; opt_lut"); - } else if (flowmap) { - run(stringf("flowmap -maxlut %d", lut)); } run("opt -fast" + hieropt_flag); - if ((!noabc && !flowmap) || help_mode) { + if (!noabc || help_mode) { #ifdef YOSYS_ENABLE_ABC if (help_mode) { run(abc, " (unless -noabc, unless -lut)"); diff --git a/techlibs/ice40/CMakeLists.txt b/techlibs/ice40/CMakeLists.txt index f925e6956..86b2e59a2 100644 --- a/techlibs/ice40/CMakeLists.txt +++ b/techlibs/ice40/CMakeLists.txt @@ -38,7 +38,6 @@ yosys_pass(synth_ice40 deminout dfflegalize flatten - flowmap fsm hierarchy ice40_braminit diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc index 07911350e..68db38c51 100644 --- a/techlibs/ice40/synth_ice40.cc +++ b/techlibs/ice40/synth_ice40.cc @@ -109,9 +109,6 @@ struct SynthIce40Pass : public ScriptPass log(" -noabc9\n"); log(" disable use of new ABC9 flow\n"); log("\n"); - log(" -flowmap\n"); - log(" use FlowMap LUT techmapping instead of abc (EXPERIMENTAL)\n"); - log("\n"); log(" -no-rw-check\n"); log(" marks all recognized read ports as \"return don't-care value on\n"); log(" read/write collision\" (same result as setting the no_rw_check\n"); @@ -130,7 +127,7 @@ struct SynthIce40Pass : public ScriptPass } string top_opt, blif_file, edif_file, json_file, device_opt, latches; - bool nocarry, nodffe, nobram, spram, dsp, flatten, retime, noabc, abc2, vpr, abc9, dff, flowmap, no_rw_check; + bool nocarry, nodffe, nobram, spram, dsp, flatten, retime, noabc, abc2, vpr, abc9, dff, no_rw_check; int min_ce_use; void clear_flags() override @@ -151,7 +148,6 @@ struct SynthIce40Pass : public ScriptPass abc2 = false; vpr = false; abc9 = true; - flowmap = false; device_opt = "hx"; no_rw_check = false; latches = "error"; @@ -257,10 +253,6 @@ struct SynthIce40Pass : public ScriptPass device_opt = args[++argidx]; continue; } - if (args[argidx] == "-flowmap") { - flowmap = true; - continue; - } if (args[argidx] == "-no-rw-check") { no_rw_check = true; continue; @@ -284,10 +276,6 @@ struct SynthIce40Pass : public ScriptPass log_cmd_error("-retime option not currently compatible with -abc9!\n"); if (abc9 && noabc) log_cmd_error("-abc9 is incompatible with -noabc!\n"); - if (abc9 && flowmap) - log_cmd_error("-abc9 is incompatible with -flowmap!\n"); - if (flowmap && noabc) - log_cmd_error("-flowmap is incompatible with -noabc!\n"); log_header(design, "Executing SYNTH_ICE40 pass.\n"); log_push(); @@ -422,12 +410,10 @@ struct SynthIce40Pass : public ScriptPass if (latches == "error" || help_mode) run("check -latchonly -assert", "(only if -latches error, the default)"); run("techmap -map +/ice40/latches_map.v"); - if (noabc || flowmap || help_mode) { - run("simplemap", " (if -noabc or -flowmap)"); + if (noabc || help_mode) { + run("simplemap", " (if -noabc)"); if (noabc || help_mode) run("techmap -map +/gate2lut.v -D LUT_WIDTH=4", "(only if -noabc)"); - if (flowmap || help_mode) - run("flowmap -maxlut 4", "(only if -flowmap)"); } if (!noabc) { if (abc9) { From 5574994453f930dec7e9a07f7424c88c34b8162e Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 22 Jul 2026 15:03:12 +0200 Subject: [PATCH 41/41] Add dependencies to gtests --- CMakeLists.txt | 1 + tests/unit/CMakeLists.txt | 3 +++ 2 files changed, 4 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3745ea0fe..bccf29049 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -535,6 +535,7 @@ if (NOT YOSYS_BUILD_PYTHON_ONLY) add_custom_target(test-unit COMMAND ${CMAKE_CTEST_COMMAND} --test-dir tests/unit --output-on-failure WORKING_DIRECTORY ${CMAKE_BINARY_DIR} + DEPENDS $<$:yosys-gtest-all> ) add_custom_target(test-vanilla diff --git a/tests/unit/CMakeLists.txt b/tests/unit/CMakeLists.txt index cc326d2d3..8534964a6 100644 --- a/tests/unit/CMakeLists.txt +++ b/tests/unit/CMakeLists.txt @@ -14,6 +14,7 @@ function(yosys_gtest arg_TARGET) ) yosys_expand_components(test_components essentials ${arg_COMPONENTS}) yosys_link_components(${target} PRIVATE ${test_components}) + add_dependencies(yosys-gtest-all ${target}) if(NOT CMAKE_CROSSCOMPILING) gtest_discover_tests(${target}) @@ -21,6 +22,8 @@ function(yosys_gtest arg_TARGET) endfunction() if (GTest_FOUND) + add_custom_target(yosys-gtest-all) + add_subdirectory(kernel) add_subdirectory(opt) add_subdirectory(techmap)