mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-02 15:18:07 +00:00
Code Activity

symfpu: floatWithStatusFlags

Browse source 
Now with verified muladd exceptions.
This commit is contained in:
Krystine Sherwin 2026-03-11 12:58:54 +13:00
parent a0a0b2ce84
commit cc4e9e52a8
No known key found for this signature in database
4 changed files with 37 additions and 65 deletions
Download patch file Download diff file Expand all files Collapse all files

2
libs/symfpu

@ -1 +1 @@
Subproject commit 7ef44ec4a91de1635b3c837dc00ea5b570b3e871 Subproject commit 3be4ad0421f67483795d2d8f789a38d4cc303c3a

73
passes/cmds/symfpu.cc
View file

@ -78,6 +78,7 @@ using ubv = rtlil_traits::ubv;
using sbv = rtlil_traits::sbv; using sbv = rtlil_traits::sbv;
using symfpu::ite; using symfpu::ite;
using uf = symfpu::unpackedFloat<rtlil_traits>; using uf = symfpu::unpackedFloat<rtlil_traits>;
using uf_flagged = symfpu::floatWithStatusFlags<rtlil_traits>;
PRIVATE_NAMESPACE_END PRIVATE_NAMESPACE_END
@ -500,74 +501,36 @@ struct SymFpuPass : public Pass {
uf a = symfpu::unpack<rtlil_traits>(format, a_bv); uf a = symfpu::unpack<rtlil_traits>(format, a_bv);
uf b = symfpu::unpack<rtlil_traits>(format, b_bv); uf b = symfpu::unpack<rtlil_traits>(format, b_bv);
uf c = symfpu::unpack<rtlil_traits>(format, c_bv); uf c = symfpu::unpack<rtlil_traits>(format, c_bv);
uf o = symfpu::unpackedFloat<rtlil_traits>::makeNaN(format); uf_flagged o_flagged(symfpu::unpackedFloat<rtlil_traits>::makeNaN(format));
if (op.compare("sqrt") == 0) if (op.compare("add") == 0)
o = symfpu::sqrt(format, rounding_mode, a); o_flagged = uf_flagged(symfpu::add_flagged<rtlil_traits>(format, rounding_mode, a, b, prop(true)));
else if (op.compare("add") == 0)
o = symfpu::add<rtlil_traits>(format, rounding_mode, a, b, prop(true));
else if (op.compare("sub") == 0) else if (op.compare("sub") == 0)
o = symfpu::add<rtlil_traits>(format, rounding_mode, a, b, prop(false)); o_flagged = uf_flagged(symfpu::add_flagged<rtlil_traits>(format, rounding_mode, a, b, prop(false)));
else if (op.compare("mul") == 0) else if (op.compare("mul") == 0)
o = symfpu::multiply<rtlil_traits>(format, rounding_mode, a, b); o_flagged = uf_flagged(symfpu::multiply_flagged<rtlil_traits>(format, rounding_mode, a, b));
else if (op.compare("div") == 0) else if (op.compare("div") == 0)
o = symfpu::divide<rtlil_traits>(format, rounding_mode, a, b); o_flagged = uf_flagged(symfpu::divide_flagged<rtlil_traits>(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) else if (op.compare("muladd") == 0)
o = symfpu::fma<rtlil_traits>(format, rounding_mode, a, b, c); o_flagged = symfpu::fma_flagged<rtlil_traits>(format, rounding_mode, a, b, c);
else else
log_abort(); log_abort();
// signaling NaN inputs raise NV // 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) || (b.getNaN() && is_sNaN(b_bv, sb) && inputs >= 2)
|| (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3) || (c.getNaN() && is_sNaN(c_bv, sb) && inputs >= 3)
); );
// invalid operation sets output to NaN output_prop(ID(NV), o_flagged.nv || signals_invalid);
prop invalid_operation(symfpu_mod->ReduceOr(NEW_ID, flag_map["NV"])); output_prop(ID(DZ), o_flagged.dz);
rtlil_traits::invariant(!invalid_operation || o.getNaN()); output_prop(ID(OF), o_flagged.of);
output_prop(ID(NV), invalid_operation); output_prop(ID(UF), o_flagged.uf);
output_prop(ID(NX), o_flagged.nx);
// div/0 is a (correctly-signed) infinity output_ubv(ID(o), symfpu::pack<rtlil_traits>(format, o_flagged.val));
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<rtlil_traits>(format, o));
symfpu_mod->fixup_ports(); symfpu_mod->fixup_ports();
} }
} SymFpuPass; } SymFpuPass;

25
tests/symfpu/edges.sv
View file

@ -166,16 +166,26 @@ module edges();
assign rounded_000 = '0; assign rounded_000 = '0;
`endif `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 always @* begin
if (a_nan || b_nan || c_nan) begin if (a_nan || b_nan || c_nan) begin
// input NaN = output NaN // input NaN = output NaN
assert (o_nan); assert (o_nan);
// NaN inputs give NaN outputs, do not raise exceptions (unless signaling NV) // NaN inputs give NaN outputs, do not raise exceptions (unless signaling NV)
// assert (!DZ); assert (!DZ);
// assert (!OF); assert (!OF);
// assert (!UF); assert (!UF);
// assert (!NX); assert (!NX);
end end
if (a_snan) if (a_snan)
@ -226,8 +236,8 @@ module edges();
`endif `endif
if (UF) if (UF)
// output = subnormal // output = subnormal or zero
assert (o_subnorm); assert (o_subnorm || o_zero);
if (o_inf && !OF) if (o_inf && !OF)
// a non-overflowing infinity is exact // a non-overflowing infinity is exact
@ -354,7 +364,6 @@ module edges();
// normal multiplication, overflow addition // normal multiplication, overflow addition
if (a == 31'h5f400000 && b == a && c == 32'h7f400000) begin if (a == 31'h5f400000 && b == a && c == 32'h7f400000) begin
assert (OF); assert (OF);
assert (o_inf); // assuming RNE
end end
// if multiplication overflows, addition can bring it back in range // if multiplication overflows, addition can bring it back in range
if (a == 32'hc3800001 && b == 32'h7b800000 && !c_special) begin if (a == 32'hc3800001 && b == 32'h7b800000 && !c_special) begin
@ -364,7 +373,7 @@ module edges();
else if (c_exp <= 8'he7) else if (c_exp <= 8'he7)
// addend can't be too small // addend can't be too small
assert (OF); 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 // this is just the turning point for this particular value
assert (OF); assert (OF);
else else

2
tests/symfpu/run-test.sh
View file

@ -37,6 +37,6 @@ prove_op add "-DADD -DADDSUB -DADDS"
prove_op sub "-DSUB -DADDSUB -DADDS" prove_op sub "-DSUB -DADDSUB -DADDS"
prove_op mul "-DMUL -DMULS" prove_op mul "-DMUL -DMULS"
prove_op div "-DDIV" prove_op div "-DDIV"
# prove_op muladd "-DMULADD -DMULS -DADDS" prove_op muladd "-DMULADD -DMULS -DADDS"
generate_mk --yosys-scripts generate_mk --yosys-scripts