mirror of
https://github.com/YosysHQ/yosys
synced 2026-01-22 18:14:01 +00:00
symfpu: Configurable rounding modes
Including tests, but currently only testing rounding modes on multiply. Also missing the ...01 case.
This commit is contained in:
Krystine Sherwin
parent
aa43a32551
commit
9db187469d
3 changed files with 132 additions and 11 deletions
|
|
@ -416,13 +416,25 @@ struct SymFpuPass : public Pass {
|
|||
"muladd | three input fused multiple-add | o = (a*b)+c\n"
|
||||
);
|
||||
|
||||
auto rm_option = content_root->open_option("-rm <RM>");
|
||||
rm_option->paragraph("rounding mode to generate, must be one of the below; default=RNE");
|
||||
rm_option->codeblock(
|
||||
"<RM> | description\n"
|
||||
"-----+----------------------\n"
|
||||
"RNE | round ties to even\n"
|
||||
"RNA | round ties to away\n"
|
||||
"RTP | round toward positive\n"
|
||||
"RTN | round toward negative\n"
|
||||
"RTZ | round toward zero\n"
|
||||
);
|
||||
|
||||
return true;
|
||||
}
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
//TODO: fix multiple calls to symfpu in single Yosys instance
|
||||
int eb = 8, sb = 24;
|
||||
string op = "mul";
|
||||
string op = "mul", rounding = "RNE";
|
||||
int inputs = 2;
|
||||
log_header(design, "Executing SYMFPU pass.\n");
|
||||
|
||||
|
|
@ -452,11 +464,29 @@ struct SymFpuPass : public Pass {
|
|||
log("Generating '%s'\n", op);
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-rm" && argidx+1 < args.size()) {
|
||||
rounding = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
extra_args(args, argidx, design);
|
||||
|
||||
rm rounding_mode;
|
||||
if (rounding.compare("RNE") == 0)
|
||||
rounding_mode = rtlil_traits::RNE();
|
||||
else if (rounding.compare("RNA") == 0)
|
||||
rounding_mode = rtlil_traits::RNA();
|
||||
else if (rounding.compare("RTP") == 0)
|
||||
rounding_mode = rtlil_traits::RTP();
|
||||
else if (rounding.compare("RTN") == 0)
|
||||
rounding_mode = rtlil_traits::RTN();
|
||||
else if (rounding.compare("RTZ") == 0)
|
||||
rounding_mode = rtlil_traits::RTZ();
|
||||
else
|
||||
log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding);
|
||||
|
||||
fpt format(eb, sb);
|
||||
|
||||
auto mod = design->addModule(ID(symfpu));
|
||||
|
|
@ -473,17 +503,17 @@ struct SymFpuPass : public Pass {
|
|||
uf o = symfpu::unpackedFloat<rtlil_traits>::makeNaN(format);
|
||||
|
||||
if (op.compare("sqrt") == 0)
|
||||
o = symfpu::sqrt(format, rtlil_traits::RNE(), a);
|
||||
o = symfpu::sqrt(format, rounding_mode, a);
|
||||
else if (op.compare("add") == 0)
|
||||
o = symfpu::add<rtlil_traits>(format, rtlil_traits::RNE(), a, b, prop(true));
|
||||
o = symfpu::add<rtlil_traits>(format, rounding_mode, a, b, prop(true));
|
||||
else if (op.compare("sub") == 0)
|
||||
o = symfpu::add<rtlil_traits>(format, rtlil_traits::RNE(), a, b, prop(false));
|
||||
o = symfpu::add<rtlil_traits>(format, rounding_mode, a, b, prop(false));
|
||||
else if (op.compare("mul") == 0)
|
||||
o = symfpu::multiply<rtlil_traits>(format, rtlil_traits::RNE(), a, b);
|
||||
o = symfpu::multiply<rtlil_traits>(format, rounding_mode, a, b);
|
||||
else if (op.compare("div") == 0)
|
||||
o = symfpu::divide<rtlil_traits>(format, rtlil_traits::RNE(), a, b);
|
||||
o = symfpu::divide<rtlil_traits>(format, rounding_mode, a, b);
|
||||
else if (op.compare("muladd") == 0)
|
||||
o = symfpu::fma<rtlil_traits>(format, rtlil_traits::RNE(), a, b, c);
|
||||
o = symfpu::fma<rtlil_traits>(format, rounding_mode, a, b, c);
|
||||
else
|
||||
log_abort();
|
||||
|
||||
|
|
@ -519,7 +549,8 @@ struct SymFpuPass : public Pass {
|
|||
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());
|
||||
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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue