From 0ef11ee048be25b0c4a89d1865d13030b15f173c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 15 Jul 2026 14:50:06 +1200 Subject: [PATCH 01/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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/34] 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 c2237447bf64f8430b076732c86c2b6c486c57ba Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 20 Jul 2026 09:58:04 +1200 Subject: [PATCH 32/34] 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 a7cfabd40563b41f67432d2831e5178a8fbc64bd Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 20 Jul 2026 10:29:41 +0200 Subject: [PATCH 33/34] 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 34/34] 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