mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-03-23 12:59:15 +00:00
Code Activity

symfpu: Configurable rounding modes

Browse source 
Including tests, but currently only testing rounding modes on multiply.
Also missing the ...01 case.
This commit is contained in:
Krystine Sherwin 2026-03-11 12:58:54 +13:00
parent ae5ac17e3f
commit cd28709b81
No known key found for this signature in database
3 changed files with 132 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

66
tests/symfpu/edges.sv
View file

@ -4,6 +4,11 @@ module edges();
reg NV, DZ, OF, UF, NX;
symfpu mod (.*);
wire [31:0] pos_max = 32'h7f7fffff;
wire [31:0] pos_inf = 32'h7f800000;
wire [31:0] neg_max = 32'hff7fffff;
wire [31:0] neg_inf = 32'hff800000;
wire a_sign = a[31];
wire [30:0] a_unsigned = a[30:0];
wire [7:0] a_exp = a[30:23];
@ -128,6 +133,15 @@ module edges();
wire lhs_dominates = lhs_exp > rhs_exp;
wire [7:0] exp_diff = lhs_dominates ? lhs_exp - rhs_exp : rhs_exp - lhs_exp;
wire round_p_001 = 0;
wire round_p_011 = a == 32'h40400000 && b == 32'h40000001;
wire round_n_011 = 0;
wire round_n_011 = a == 32'hc0400000 && b == 32'h40000001;
wire [30:0] rounded_100 = 31'h40C00002;
wire [30:0] rounded_010 = 31'h40C00001;
wire [30:0] rounded_000 = 31'h40C00000;
always @* begin
if (a_nan)
// input NaN = output NaN
@ -157,10 +171,29 @@ module edges();
// underflow is always inexact
assert (NX);
if (OF) begin
// for RNE, output = +=inf
`ifdef RNE
if (OF) // output = +-inf
assert (o_inf);
end
`elsif RNA
if (OF) // output = +-inf
assert (o_inf);
`elsif RTP
if (OF) // output = +inf or -max
// RTP add is raising inexact overflow for NaN input
assert (o == pos_inf || o == neg_max);
if (o == neg_inf)
assert (!OF);
`elsif RTN
if (OF) // output = +max or -inf
assert (o == pos_max || o == neg_inf);
if (o == pos_inf)
assert (!OF);
`elsif RTZ
if (OF) // output = +-max
assert (o == pos_max || o == neg_max);
if (o_inf) // cannot overflow to infinity
assert (!OF);
`endif
if (UF)
// output = subnormal
@ -223,6 +256,33 @@ module edges();
assert (!UF);
`endif
`ifdef RNE
if (round_p_001) assert (o_unsigned == rounded_000);
if (round_p_011) assert (o_unsigned == rounded_100);
if (round_n_011) assert (o_unsigned == rounded_000);
if (round_n_011) assert (o_unsigned == rounded_100);
`elsif RNA
if (round_p_001) assert (o_unsigned == rounded_010);
if (round_p_011) assert (o_unsigned == rounded_100);
if (round_n_011) assert (o_unsigned == rounded_010);
if (round_n_011) assert (o_unsigned == rounded_100);
`elsif RTP
if (round_p_001) assert (o_unsigned == rounded_010);
if (round_p_011) assert (o_unsigned == rounded_100);
if (round_n_011) assert (o_unsigned == rounded_000);
if (round_n_011) assert (o_unsigned == rounded_010);
`elsif RTN
if (round_p_001) assert (o_unsigned == rounded_000);
if (round_p_011) assert (o_unsigned == rounded_010);
if (round_n_011) assert (o_unsigned == rounded_010);
if (round_n_011) assert (o_unsigned == rounded_100);
`elsif RTZ
if (round_p_001) assert (o_unsigned == rounded_000);
if (round_p_011) assert (o_unsigned == rounded_010);
if (round_n_011) assert (o_unsigned == rounded_000);
if (round_n_011) assert (o_unsigned == rounded_010);
`endif
`ifdef ADDS
if (use_lhs) begin
// inf - inf

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

@ -3,6 +3,7 @@ set -eu
source ../gen-tests-makefile.sh
# operators
ops="sqrt add sub mul div muladd"
for op in $ops; do
rm -f ${op}_edges.*
@ -32,4 +33,33 @@ prove_op mul "-DMUL -DMULS"
prove_op div "-DDIV"
prove_op muladd "-DMULADD -DMULS -DADDS"
# rounding modes
rms="RNE RNA RTP RTN RTZ"
for rm in $rms; do
rm -f ${rm}_edges.*
done
prove_rm() {
rm=$1
defs=$2
ys_file=${rm}_edges.ys
echo """\
symfpu -rm $rm
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_rm RNE "-DRNE"
prove_rm RNA "-DRNA"
prove_rm RTP "-DRTP"
prove_rm RTN "-DRTN"
prove_rm RTZ "-DRTZ"
generate_mk --yosys-scripts