From 88e6305849fbccad349b7b75ea2c09d7a447c030 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Wed, 21 Jan 2026 18:32:07 +1300 Subject: [PATCH] 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