diff --git a/.gitmodules b/.gitmodules index ab798fb71..d951c8d01 100644 --- a/.gitmodules +++ b/.gitmodules @@ -20,3 +20,7 @@ [submodule "sv-elab"] path = frontends/slang/lib url = https://github.com/povik/sv-elab +[submodule "symfpu"] + path = libs/symfpu + url = https://github.com/YosysHQ/symfpu + branch = floatWithStatusFlags 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/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..5d5e50867 --- /dev/null +++ b/libs/symfpu @@ -0,0 +1 @@ +Subproject commit 5d5e50867437fe5cabd6ab5aad3b3808ec86701f 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..c227266a6 --- /dev/null +++ b/passes/cmds/symfpu.cc @@ -0,0 +1,799 @@ +/* + * 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 "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 + +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 { + 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}; }; + 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); + 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; +using sbv = rtlil_traits::sbv; +using symfpu::ite; +using uf = symfpu::unpackedFloat; +using uf_flagged = symfpu::floatWithStatusFlags; +using uf_flagged_ite = symfpu::ite; +using ubv_flagged = symfpu::bvWithStatusFlags; +using sbv_flagged = symfpu::bvWithStatusFlags; + +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->Ne(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)}; +} + +[[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) +{ + 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)); +} + +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()); + symfpu_mod->connect(output, value.bits); + 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; +} + +// 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(); +} + +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"); + + auto content_root = help->get_root(); + + 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"); + + // 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( + " | 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" + "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" + ); + + 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."); + + 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." + ); + + 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 + { + //TODO: fix multiple calls to symfpu in single Yosys instance + int eb = 8, sb = 24; + string op = "mul", rounding = "DYN"; + int inputs = 2; + bool classify = false, compare = false; + 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; + } + if (args[argidx] == "-op" && argidx+1 < args.size()) { + op = args[++argidx]; + if (op.compare("sqrt") == 0 + || op.compare("altsqrt") == 0) // currently undocumented + inputs = 1; + else if (op.compare("add") == 0 + || op.compare("sub") == 0 + || 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) + inputs = 3; + else + log_cmd_error("Unknown operation '%s'. Call help symfpu for available operations.\n", op); + log("Generating '%s'\n", op); + continue; + } + if (args[argidx] == "-rm" && argidx+1 < args.size()) { + rounding = args[++argidx]; + continue; + } + if (args[argidx] == "-classify") { + classify = true; + continue; + } + if (args[argidx] == "-compare") { + compare = true; + continue; + } + break; + } + + extra_args(args, argidx, design); + + 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("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"); + } + + rm rounding_mode = parse_rounding(rounding); + fpt format(eb, sb); + + auto mod = design->addModule(ID(symfpu)); + + symfpu_mod = mod; + + auto a_bv = input_ubv(ID(a), eb+sb); + uf a = symfpu::unpack(format, a_bv); + + 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 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); + 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 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 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(); + }; + + // 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(); + } +} 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); + 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)); + output_flags(ID(flags_ff), o_ff.nv || i_sNaN, o_ff.nx, o_ff.of, o_ff.uf); + + auto is_signed = input_prop(ID(is_signed)); + + // 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); + + symfpu_mod->fixup_ports(); + } +} SymFpuConvertPass; + +PRIVATE_NAMESPACE_END 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..5be02d3bd --- /dev/null +++ b/tests/symfpu/edges.sv @@ -0,0 +1,784 @@ +module edges(input clk); + +`ifdef MASK + (* 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 + (* 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]; + 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 + (* anyseq *) reg [31:0] a, b, c; +`endif + + (* anyseq *) reg [4:0] rm; + reg [31:0] o; + 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]; + 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 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]; + 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; + wire o_clamped = o_unsigned == 31'h7f7fffff; + 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); + +`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; + + wire round_p_001, round_p_011, round_n_001, round_n_011; + wire [30:0] rounded_100, rounded_010, rounded_000; + +`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 + +`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; + 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 + // 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); + +`ifndef SQRTS +// sqrt has no b input + cover (b_sign); + cover (!b_sign); + cover (b_zero); + cover (b_norm); + cover (b_subnorm); + 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); + cover (c_norm); + cover (c_subnorm); + cover (c_inf); + cover (c_qnan); + cover (c_snan); +`endif + + // all flags are possible + cover (NV); +`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 + cover (NX); +`endif + 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_inf); + cover (o_nan); +`ifndef SQRTS +// subnormal outputs not possible for 8/24 sqrt + cover (o_subnorm); + cover (o_ebmin); +`endif + +`ifndef COMPARES +`ifndef SQRTS + 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 +`endif + + 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 (NV) + // output = qNaN + assert (o_qnan); +`endif // !COMPARES + + if (a_snan || b_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 (OF) + // overflow is always inexact + assert (NX); + + if (UF) + // underflow is always inexact + assert (NX); + + if (UF) + // output = subnormal or zero or +-e^bmin + assert (o_subnorm || o_zero || o_ebmin); + + 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 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 + assert (DZ ^~ (a_finite && b_zero)); + // 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 + // 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 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])); + `endif +`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); + // 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'h68 && b_subnorm && !c_special) begin + assert (NX); + `ifdef MULADD + // within rounding + assert (UF || (c_zero ? o_zero : (o == c || o == c+1 || o == c-1))); + `else + assert (UF || o_zero); + 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 + +`ifdef RNE + assume (rm_RNE); +`elsif RNA + assume (rm_RNA); +`elsif RTP + assume (rm_RTP); +`elsif RTN + assume (rm_RTN); +`elsif RTZ + 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 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); + + // 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) + 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 + 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_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); + 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); + 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_muladd_turning) + // 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 SQRTS + assume (b_zero); + assume (c_zero); + assert (!UF); + assert (!OF); + // complex roots are invalid + 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 + +`ifdef EDGE_EVENTS + 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 + // 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 + 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 +`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 +`endif +endmodule 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"])