diff --git a/passes/cmds/symfpu.cc b/passes/cmds/symfpu.cc index fb7a09377..05ee59f2a 100644 --- a/passes/cmds/symfpu.cc +++ b/passes/cmds/symfpu.cc @@ -79,6 +79,7 @@ using sbv = rtlil_traits::sbv; using symfpu::ite; using uf = symfpu::unpackedFloat; using uf_flagged = symfpu::floatWithStatusFlags; +using uf_flagged_ite = symfpu::ite; PRIVATE_NAMESPACE_END @@ -411,16 +412,18 @@ struct SymFpuPass : public Pass { ); 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->paragraph("rounding mode to generate, must be one of the below; default=DYN"); 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" + " | rm | description\n" + "-----+--------+----------------------\n" + "RNE | 00001 | round ties to even\n" + "RNA | 00010 | round ties to away\n" + "RTP | 00100 | round toward positive\n" + "RTN | 01000 | round toward negative\n" + "RTZ | 10000 | round toward zero\n" + "DYN | xxxxx | round based on 'rm' input signal\n" ); + rm_option->paragraph("Note: when not using DYN mode, the 'rm' input is ignored."); return true; } @@ -428,7 +431,7 @@ struct SymFpuPass : public Pass { { //TODO: fix multiple calls to symfpu in single Yosys instance int eb = 8, sb = 24; - string op = "mul", rounding = "RNE"; + string op = "mul", rounding = "DYN"; int inputs = 2; log_header(design, "Executing SYMFPU pass.\n"); @@ -470,14 +473,16 @@ struct SymFpuPass : public Pass { rm rounding_mode; if (rounding.compare("RNE") == 0) rounding_mode = rtlil_traits::RNE(); - else if (rounding.compare("RNA") == 0) + else if (rounding.compare("RNA") == 0) rounding_mode = rtlil_traits::RNA(); - else if (rounding.compare("RTP") == 0) + else if (rounding.compare("RTP") == 0) rounding_mode = rtlil_traits::RTP(); - else if (rounding.compare("RTN") == 0) + else if (rounding.compare("RTN") == 0) rounding_mode = rtlil_traits::RTN(); - else if (rounding.compare("RTZ") == 0) + else if (rounding.compare("RTZ") == 0) rounding_mode = rtlil_traits::RTZ(); + else if (rounding.compare("DYN") == 0) + rounding_mode = {}; else log_cmd_error("Unknown rounding mode '%s'. Call help sympfpu for available rounding modes.\n", rounding); @@ -495,12 +500,38 @@ struct SymFpuPass : public Pass { uf b = symfpu::unpack(format, b_bv); uf c = symfpu::unpack(format, c_bv); + auto rm_wire = symfpu_mod->addWire(ID(rm), 5); + rm_wire->port_input = true; + SigSpec rm_sig(rm_wire); + prop rm_RNE(rm_sig[0]); + prop rm_RNA(rm_sig[1]); + prop rm_RTP(rm_sig[2]); + prop rm_RTN(rm_sig[3]); + prop rm_RTZ(rm_sig[4]); + // signaling NaN inputs raise NV 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) ); + auto make_op = [&op, &format, &a, &b, &c](rm rounding_mode) { + if (op.compare("add") == 0) + return symfpu::add_flagged(format, rounding_mode, a, b, prop(true)); + else if (op.compare("sub") == 0) + return symfpu::add_flagged(format, rounding_mode, a, b, prop(false)); + else if (op.compare("mul") == 0) + return symfpu::multiply_flagged(format, rounding_mode, a, b); + else if (op.compare("div") == 0) + return symfpu::divide_flagged(format, rounding_mode, a, b); + else if (op.compare("sqrt") == 0) + return symfpu::sqrt_flagged(format, rounding_mode, a); + else if (op.compare("muladd") == 0) + return symfpu::fma_flagged(format, rounding_mode, a, b, c); + else + log_abort(); + }; + // calling this more than once will fail auto output_fpu = [&signals_invalid, &format](const uf_flagged &o_flagged) { output_prop(ID(NV), o_flagged.nv || signals_invalid); @@ -512,20 +543,24 @@ struct SymFpuPass : public Pass { output_ubv(ID(o), symfpu::pack(format, o_flagged.val)); }; - if (op.compare("add") == 0) - output_fpu(symfpu::add_flagged(format, rounding_mode, a, b, prop(true))); - else if (op.compare("sub") == 0) - output_fpu(symfpu::add_flagged(format, rounding_mode, a, b, prop(false))); - else if (op.compare("mul") == 0) - output_fpu(symfpu::multiply_flagged(format, rounding_mode, a, b)); - else if (op.compare("div") == 0) - output_fpu(symfpu::divide_flagged(format, rounding_mode, a, b)); - else if (op.compare("sqrt") == 0) - output_fpu(symfpu::sqrt_flagged(format, rounding_mode, a)); - else if (op.compare("muladd") == 0) - output_fpu(symfpu::fma_flagged(format, rounding_mode, a, b, c)); - else - log_abort(); + if (rounding.compare("DYN") != 0) + output_fpu(make_op(rounding_mode)); + else { + auto out_RNE = make_op(rtlil_traits::RNE()); + auto out_RNA = make_op(rtlil_traits::RNA()); + auto out_RTP = make_op(rtlil_traits::RTP()); + auto out_RTN = make_op(rtlil_traits::RTN()); + auto out_RTZ = make_op(rtlil_traits::RTZ()); + output_fpu( + uf_flagged_ite::iteOp(rm_RNE, out_RNE, + uf_flagged_ite::iteOp(rm_RNA, out_RNA, + uf_flagged_ite::iteOp(rm_RTP, out_RTP, + uf_flagged_ite::iteOp(rm_RTN, out_RTN, + uf_flagged_ite::iteOp(rm_RTZ, out_RTZ, + uf_flagged::makeNaN(format, prop(true))))))) + ); + } + symfpu_mod->fixup_ports(); } diff --git a/tests/symfpu/edges.sv b/tests/symfpu/edges.sv index ba40140b4..eecb60bad 100644 --- a/tests/symfpu/edges.sv +++ b/tests/symfpu/edges.sv @@ -1,5 +1,6 @@ module edges(); (* anyseq *) reg [31:0] a, b, c; + (* anyseq *) reg [4:0] rm; reg [31:0] o; reg NV, DZ, OF, UF, NX; symfpu mod (.*); @@ -166,15 +167,16 @@ 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 + wire rm_RNE = rm[0] == 1'b1; + wire rm_RNA = rm[1:0] == 2'b10; + wire rm_RTP = rm[2:0] == 3'b100; + wire rm_RTN = rm[3:0] == 4'b1000; + wire rm_RTZ = rm[4:0] == 5'b10000; + + wire c_muladd_turning = rm_RNE || rm_RNA ? c_sig <= 23'h200000 : + rm_RTP ? c_sig == '0 : + rm_RTN ? c_sig < 23'h400000 : + c_sig == '0; always @* begin if (a_nan || b_nan || c_nan) begin @@ -212,29 +214,6 @@ module edges(); // underflow is always inexact assert (NX); -`ifdef RNE - if (OF) // output = +-inf - assert (o_inf); -`elsif RNA - if (OF) // output = +-inf - assert (o_inf); -`elsif RTP - if (OF) // output = +inf or -max - 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 or zero assert (o_subnorm || o_zero); @@ -304,32 +283,73 @@ module edges(); `endif `ifdef RNE - if (round_p_001) assert (o_unsigned == rounded_000); - if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_001) assert (o_unsigned == rounded_000); - if (round_n_011) assert (o_unsigned == rounded_100); + assume (rm_RNE); `elsif RNA - if (round_p_001) assert (o_unsigned == rounded_010); - if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_001) assert (o_unsigned == rounded_010); - if (round_n_011) assert (o_unsigned == rounded_100); + assume (rm_RNA); `elsif RTP - if (round_p_001) assert (o_unsigned == rounded_010); - if (round_p_011) assert (o_unsigned == rounded_100); - if (round_n_001) assert (o_unsigned == rounded_000); - if (round_n_011) assert (o_unsigned == rounded_010); + assume (rm_RTP); `elsif RTN - if (round_p_001) assert (o_unsigned == rounded_000); - if (round_p_011) assert (o_unsigned == rounded_010); - if (round_n_001) assert (o_unsigned == rounded_010); - if (round_n_011) assert (o_unsigned == rounded_100); + assume (rm_RTN); `elsif RTZ - if (round_p_001) assert (o_unsigned == rounded_000); - if (round_p_011) assert (o_unsigned == rounded_010); - if (round_n_001) assert (o_unsigned == rounded_000); - if (round_n_011) assert (o_unsigned == rounded_010); + assume (rm_RTZ); +`else + assume ($onehot(rm)); `endif + if (OF) + // rounding mode determines if overflow value is inf or max + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_inf); + 5'bzzz10 /* RNA */: assert (o_inf); + 5'bzz100 /* RTP */: assert (o == pos_inf || o == neg_max); + 5'bz1000 /* RTN */: assert (o == pos_max || o == neg_inf); + 5'b10000 /* RTZ */: assert (o == pos_max || o == neg_max); + endcase + + // RTx modes cannot overflow to the far infinity + if (rm_RTP && o == neg_inf) + assert (!OF); + if (rm_RTN && o == pos_inf) + assert (!OF); + + // RTZ cannot overflow to either + if (rm_RTZ && o_inf) + assert (!OF); + + // test rounding + if (round_p_001) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_000); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_010); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_010); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_000); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_000); + endcase + if (round_p_011) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_100); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_100); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_100); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_010); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_010); + endcase + if (round_n_001) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_000); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_010); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_000); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_010); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_000); + endcase + if (round_n_011) + casez (rm) + 5'bzzzz1 /* RNE */: assert (o_unsigned == rounded_100); + 5'bzzz10 /* RNA */: assert (o_unsigned == rounded_100); + 5'bzz100 /* RTP */: assert (o_unsigned == rounded_010); + 5'bz1000 /* RTN */: assert (o_unsigned == rounded_100); + 5'b10000 /* RTZ */: assert (o_unsigned == rounded_010); + endcase + `ifdef ADDS if (use_lhs) begin // inf - inf diff --git a/tests/symfpu/run-test.sh b/tests/symfpu/run-test.sh index e0346aecf..36db8f395 100755 --- a/tests/symfpu/run-test.sh +++ b/tests/symfpu/run-test.sh @@ -10,9 +10,11 @@ prove_rm() { rm=$2 defs=$3 ys_file=${op}_${rm}_edges.ys + echo "symfpu -op $op -rm $rm" > $ys_file + if [[ $rm != "DYN" ]] then + echo "sat -prove-asserts -verify" >> $ys_file + fi echo """\ -symfpu -op $op -rm $rm -sat -prove-asserts -verify chformal -remove opt @@ -20,13 +22,13 @@ read_verilog -sv -formal $defs -D${rm} edges.sv chformal -lower prep -top edges -flatten sat -set-assumes -prove-asserts -verify -""" > $ys_file +""" >> $ys_file } prove_op() { op=$1 defs=$2 - rms="RNE RNA RTP RTN RTZ" + rms="RNE RNA RTP RTN RTZ DYN" for rm in $rms; do prove_rm $op $rm "$defs" done