From d26aa0e31de6ece605cbe407bd4e0ca4ac430dad Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 17 Jan 2026 17:32:43 +1300 Subject: [PATCH] symfpu: Add flags Use symfpu fork. Add tests for symfpu properties and extra edge case checking for flags. --- Makefile | 1 + libs/symfpu | 2 +- passes/cmds/symfpu.cc | 81 ++++++++++- 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/Makefile b/Makefile index 5c7128f5a..3355e8e61 100644 --- a/Makefile +++ b/Makefile @@ -890,6 +890,7 @@ MK_TEST_DIRS += tests/opt MK_TEST_DIRS += tests/sat MK_TEST_DIRS += tests/sim MK_TEST_DIRS += tests/svtypes +MK_TEST_DIRS += tests/symfpu MK_TEST_DIRS += tests/techmap MK_TEST_DIRS += tests/various MK_TEST_DIRS += tests/rtlil 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/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