From 288f805da4d87f0085cff7fa3e6499e005398aa2 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 9 Dec 2025 15:16:59 +0100 Subject: [PATCH] wip: symfpu pass --- .gitmodules | 4 + Makefile | 2 + libs/symfpu | 1 + passes/cmds/Makefile.inc | 1 + passes/cmds/symfpu.cc | 411 +++++++++++++++++++++++++++++++++++++++ 5 files changed, 419 insertions(+) create mode 160000 libs/symfpu create mode 100644 passes/cmds/symfpu.cc diff --git a/.gitmodules b/.gitmodules index 9f18be11e..e9dd59e09 100644 --- a/.gitmodules +++ b/.gitmodules @@ -5,3 +5,7 @@ [submodule "cxxopts"] path = libs/cxxopts url = https://github.com/jarro2783/cxxopts +[submodule "libs/symfpu"] + path = libs/symfpu + url = https://github.com/martin-cs/symfpu + branch = experimental diff --git a/Makefile b/Makefile index b744763c8..5c7128f5a 100644 --- a/Makefile +++ b/Makefile @@ -684,6 +684,8 @@ OBJS += libs/minisat/SimpSolver.o OBJS += libs/minisat/Solver.o OBJS += libs/minisat/System.o +passes/cmds/symfpu.o: CXXFLAGS += -Ilibs + ifeq ($(ENABLE_ZLIB),1) OBJS += libs/fst/fstapi.o OBJS += libs/fst/fastlz.o 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/Makefile.inc b/passes/cmds/Makefile.inc index 9bf615a7e..dd34caec3 100644 --- a/passes/cmds/Makefile.inc +++ b/passes/cmds/Makefile.inc @@ -57,3 +57,4 @@ OBJS += passes/cmds/abstract.o OBJS += passes/cmds/test_select.o OBJS += passes/cmds/timeest.o OBJS += passes/cmds/linecoverage.o +OBJS += passes/cmds/symfpu.o 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