mirror of
https://github.com/YosysHQ/yosys
synced 2026-01-21 17:44:45 +00:00
symfpu: floatWithStatusFlags
Now with verified muladd exceptions.
This commit is contained in:
Krystine Sherwin
parent
5c99ff204b
commit
88e6305849
4 changed files with 37 additions and 65 deletions
|
|
@ -1 +1 @@
|
|||
Subproject commit 7ef44ec4a91de1635b3c837dc00ea5b570b3e871
|
||||
Subproject commit 3be4ad0421f67483795d2d8f789a38d4cc303c3a
|
||||
|
|
@ -78,6 +78,7 @@ using ubv = rtlil_traits::ubv;
|
|||
using sbv = rtlil_traits::sbv;
|
||||
using symfpu::ite;
|
||||
using uf = symfpu::unpackedFloat<rtlil_traits>;
|
||||
using uf_flagged = symfpu::floatWithStatusFlags<rtlil_traits>;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
|
||||
|
|
@ -500,74 +501,36 @@ struct SymFpuPass : public Pass {
|
|||
uf a = symfpu::unpack<rtlil_traits>(format, a_bv);
|
||||
uf b = symfpu::unpack<rtlil_traits>(format, b_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)
|
||||
o = symfpu::sqrt(format, rounding_mode, a);
|
||||
else if (op.compare("add") == 0)
|
||||
o = symfpu::add<rtlil_traits>(format, rounding_mode, a, b, prop(true));
|
||||
if (op.compare("add") == 0)
|
||||
o_flagged = uf_flagged(symfpu::add_flagged<rtlil_traits>(format, rounding_mode, a, b, prop(true)));
|
||||
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)
|
||||
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)
|
||||
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)
|
||||
o = symfpu::fma<rtlil_traits>(format, rounding_mode, a, b, c);
|
||||
else
|
||||
o_flagged = symfpu::fma_flagged<rtlil_traits>(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<rtlil_traits>(format, o));
|
||||
output_ubv(ID(o), symfpu::pack<rtlil_traits>(format, o_flagged.val));
|
||||
symfpu_mod->fixup_ports();
|
||||
}
|
||||
} SymFpuPass;
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue