diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index 7d58146e3..1cfd34b66 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -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_option->paragraph("rounding mode to generate, must be one of the below; default=RNE"); + rm_option->codeblock( + " | 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 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::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(format, rtlil_traits::RNE(), a, b, prop(true)); + o = symfpu::add(format, rounding_mode, a, b, prop(true)); else if (op.compare("sub") == 0) - o = symfpu::add(format, rtlil_traits::RNE(), a, b, prop(false)); + o = symfpu::add(format, rounding_mode, a, b, prop(false)); else if (op.compare("mul") == 0) - o = symfpu::multiply(format, rtlil_traits::RNE(), a, b); + o = symfpu::multiply(format, rounding_mode, a, b); else if (op.compare("div") == 0) - o = symfpu::divide(format, rtlil_traits::RNE(), a, b); + o = symfpu::divide(format, rounding_mode, a, b); else if (op.compare("muladd") == 0) - o = symfpu::fma(format, rtlil_traits::RNE(), a, b, c); + o = symfpu::fma(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 diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index 943858b9f..37a7adf26 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -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 diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index 32692b78b..70d08ede2 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -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