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

tests/symfpu: UF to ebmin is valid

Browse source
This commit is contained in:
Krystine Sherwin 2026-03-11 12:58:55 +13:00
parent b4186e2295
commit f0bfc87e27
No known key found for this signature in database
1 changed files with 17 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

29
tests/symfpu/edges.sv
View file

@ -66,6 +66,7 @@ module edges();
wire o_subnorm = o_exp == 8'h00 && o_sig != '0; wire o_subnorm = o_exp == 8'h00 && o_sig != '0;
wire o_finite = o_norm || o_subnorm; wire o_finite = o_norm || o_subnorm;
wire o_unclamped = o_finite && o_unsigned != 31'h7f7fffff; wire o_unclamped = o_finite && o_unsigned != 31'h7f7fffff;
wire o_ebmin = o_exp == 8'h01 && o_sig == '0;
`ifdef MULADD `ifdef MULADD
wire muladd_zero = c_zero; wire muladd_zero = c_zero;
@ -215,8 +216,8 @@ module edges();
assert (NX); assert (NX);
if (UF) if (UF)
// output = subnormal or zero // output = subnormal or zero or +-e^bmin
assert (o_subnorm || o_zero); assert (o_subnorm || o_zero || o_ebmin);
if (o_inf && !OF) if (o_inf && !OF)
// a non-overflowing infinity is exact // a non-overflowing infinity is exact
@ -228,8 +229,8 @@ module edges();
`ifdef DIV `ifdef DIV
assume (c_zero); assume (c_zero);
// div/zero when a = finite, b = 0 // div/zero only when a is finite
assert (!DZ || ((a_norm || a_subnorm) && b_unsigned == '0)); assert (DZ ^~ (a_finite && b_zero));
// 0/0 or inf/inf // 0/0 or inf/inf
if ((a_zero && b_zero) || (a_inf && b_inf)) if ((a_zero && b_zero) || (a_inf && b_inf))
assert (NV); assert (NV);
@ -305,15 +306,19 @@ module edges();
5'b10000 /* RTZ */: assert (o == pos_max || o == neg_max); 5'b10000 /* RTZ */: assert (o == pos_max || o == neg_max);
endcase endcase
// RTx modes cannot overflow to the far infinity // RTx modes cannot underflow to the opposite ebmin (or either for RTZ)
if (rm_RTP && o == neg_inf) if (UF && o_ebmin)
assert (!OF); if (o_sign)
if (rm_RTN && o == pos_inf) assert (rm_RNE || rm_RNA || rm_RTN);
assert (!OF); else
assert (rm_RNE || rm_RNA || rm_RTP);
// RTZ cannot overflow to either // and the same for overflowing to infinities
if (rm_RTZ && o_inf) if (OF && o_inf)
assert (!OF); if (o_sign)
assert (rm_RNE || rm_RNA || rm_RTN);
else
assert (rm_RNE || rm_RNA || rm_RTP);
// test rounding // test rounding
if (round_p_001) if (round_p_001)