mirror of
https://github.com/YosysHQ/yosys
synced 2026-01-17 16:06:27 +00:00
symfpu: Add flags
Use symfpu fork. Add tests for symfpu properties and extra edge case checking for flags.
This commit is contained in:
Krystine Sherwin
parent
2a76d8f7a9
commit
d26aa0e31d
6 changed files with 403 additions and 4 deletions
1
Makefile
1
Makefile
|
|
@ -890,6 +890,7 @@ MK_TEST_DIRS += tests/opt
|
|||
MK_TEST_DIRS += tests/sat
|
||||
MK_TEST_DIRS += tests/sim
|
||||
MK_TEST_DIRS += tests/svtypes
|
||||
MK_TEST_DIRS += tests/symfpu
|
||||
MK_TEST_DIRS += tests/techmap
|
||||
MK_TEST_DIRS += tests/various
|
||||
MK_TEST_DIRS += tests/rtlil
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
Subproject commit aeaa3fa62730148c855f5a9e0a9b7040d48e0b7e
|
||||
Subproject commit ac38165068f507d2b46ad16b870272f0ca5a6c0a
|
||||
|
|
@ -69,6 +69,7 @@ struct rtlil_traits {
|
|||
static void precondition(const prop &p);
|
||||
static void postcondition(const prop &p);
|
||||
static void invariant(const prop &p);
|
||||
static void setflag(const string &name, const prop &p);
|
||||
};
|
||||
|
||||
using bwt = rtlil_traits::bwt;
|
||||
|
|
@ -261,6 +262,12 @@ template <bool is_signed> struct bv {
|
|||
return bv{symfpu_mod->Shr(NEW_ID, bits, op.bits, is_signed)};
|
||||
}
|
||||
|
||||
prop operator!=(const bv<is_signed> &op) const
|
||||
{
|
||||
log_assert(getWidth() == op.getWidth());
|
||||
return prop{symfpu_mod->Ne(NEW_ID, bits, op.bits, is_signed)};
|
||||
}
|
||||
|
||||
prop operator==(const bv<is_signed> &op) const
|
||||
{
|
||||
log_assert(getWidth() == op.getWidth());
|
||||
|
|
@ -367,6 +374,19 @@ void output_prop(IdString name, const prop &value)
|
|||
output->port_output = true;
|
||||
}
|
||||
|
||||
// unpacked floats don't track NaN signalling, so we need to check the
|
||||
// raw bitvector
|
||||
template <bool is_signed> prop is_sNaN(bv<is_signed> bitvector, int sb) {
|
||||
return bitvector.extract(sb-2, sb-2).isAllZeros();
|
||||
}
|
||||
|
||||
std::map<std::string, SigSpec> flag_map;
|
||||
|
||||
void rtlil_traits::setflag(const string &name, const prop &cond)
|
||||
{
|
||||
flag_map[name].append(cond.bit);
|
||||
}
|
||||
|
||||
struct SymFpuPass : public Pass {
|
||||
SymFpuPass() : Pass("symfpu", "SymFPU based floating point netlist generator") {}
|
||||
bool formatted_help() override
|
||||
|
|
@ -382,6 +402,7 @@ struct SymFpuPass : public Pass {
|
|||
content_root->option("-eb <N>", "use <N> bits for exponent; default=8");
|
||||
content_root->option("-sb <N>", "use <N> bits for significand, including hidden bit; default=24");
|
||||
|
||||
// conversions could be useful, but for targeting Sail we don't need them
|
||||
auto op_option = content_root->open_option("-op <OP>");
|
||||
op_option->paragraph("floating point operation to generate, must be one of the below; default=mul");
|
||||
op_option->codeblock(
|
||||
|
|
@ -399,6 +420,7 @@ struct SymFpuPass : public Pass {
|
|||
}
|
||||
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";
|
||||
int inputs = 2;
|
||||
|
|
@ -441,9 +463,13 @@ struct SymFpuPass : public Pass {
|
|||
|
||||
symfpu_mod = mod;
|
||||
|
||||
uf a = symfpu::unpack<rtlil_traits>(format, input_ubv(ID(a), eb+sb));
|
||||
uf b = symfpu::unpack<rtlil_traits>(format, input_ubv(ID(b), eb+sb));
|
||||
uf c = symfpu::unpack<rtlil_traits>(format, input_ubv(ID(c), eb+sb));
|
||||
auto a_bv = input_ubv(ID(a), eb+sb);
|
||||
auto b_bv = input_ubv(ID(b), eb+sb);
|
||||
auto c_bv = input_ubv(ID(c), eb+sb);
|
||||
|
||||
uf a = symfpu::unpack<rtlil_traits>(format, a_bv);
|
||||
uf b = symfpu::unpack<rtlil_traits>(format, b_bv);
|
||||
uf c = symfpu::unpack<rtlil_traits>(format, c_bv);
|
||||
uf o = symfpu::unpackedFloat<rtlil_traits>::makeNaN(format);
|
||||
|
||||
if (op.compare("sqrt") == 0)
|
||||
|
|
@ -461,6 +487,55 @@ struct SymFpuPass : public Pass {
|
|||
else
|
||||
log_abort();
|
||||
|
||||
// signaling NaN inputs raise NV
|
||||
rtlil_traits::setflag("NV", (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)
|
||||
);
|
||||
|
||||
// invalid operation sets output to NaN
|
||||
prop invalid_operation(symfpu_mod->ReduceOr(NEW_ID, flag_map["NV"]));
|
||||
rtlil_traits::invariant(!invalid_operation || o.getNaN());
|
||||
output_prop(ID(NV), invalid_operation);
|
||||
|
||||
// div/0 is a (correctly-signed) infinity
|
||||
prop divide_by_zero(symfpu_mod->ReduceOr(NEW_ID, flag_map["DZ"]));
|
||||
rtlil_traits::invariant(!divide_by_zero || o.getInf());
|
||||
output_prop(ID(DZ), divide_by_zero);
|
||||
|
||||
prop maybe_overflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["maybe_OF"]));
|
||||
if (op.compare("div") == 0)
|
||||
// this feels like the division should be skipped but isn't handling
|
||||
// special cases until the end, so we need to manually check if the
|
||||
// overflow is valid
|
||||
rtlil_traits::setflag("OF", maybe_overflow && !(a.getInf() || a.getNaN() || a.getZero()));
|
||||
else if (op.compare("muladd") == 0) {
|
||||
// *grumbles*
|
||||
prop anyInf(a.getInf() || b.getInf() || c.getInf());
|
||||
// *grumbling intensifies*
|
||||
rtlil_traits::setflag("OF", maybe_overflow && !(anyInf || !o.getInf()));
|
||||
} else
|
||||
rtlil_traits::setflag("OF", maybe_overflow);
|
||||
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());
|
||||
output_prop(ID(OF), overflow);
|
||||
|
||||
// inexactness doesn't have an output value test, but OF and UF imply NX
|
||||
prop inexact(symfpu_mod->ReduceOr(NEW_ID, flag_map["NX"]));
|
||||
output_prop(ID(NX), inexact);
|
||||
|
||||
// underflow is non-zero tininess
|
||||
rtlil_traits::setflag("UF", inexact && o.inSubnormalRange(format, prop(true)));
|
||||
prop underflow(symfpu_mod->ReduceOr(NEW_ID, flag_map["UF"]));
|
||||
rtlil_traits::invariant(!underflow || o.inSubnormalRange(format, prop(true)));
|
||||
output_prop(ID(UF), underflow);
|
||||
|
||||
// over/underflow is definitionally inexact
|
||||
rtlil_traits::invariant(!overflow || inexact);
|
||||
rtlil_traits::invariant(!underflow || inexact);
|
||||
|
||||
output_ubv(ID(o), symfpu::pack<rtlil_traits>(format, o));
|
||||
symfpu_mod->fixup_ports();
|
||||
}
|
||||
|
|
|
|||
1
tests/symfpu/.gitignore
vendored
Normal file
1
tests/symfpu/.gitignore
vendored
Normal file
|
|
@ -0,0 +1 @@
|
|||
*_edges.ys
|
||||
287
tests/symfpu/edges.sv
Normal file
287
tests/symfpu/edges.sv
Normal file
|
|
@ -0,0 +1,287 @@
|
|||
module edges();
|
||||
(* anyseq *) reg [31:0] a, b, c;
|
||||
reg [31:0] o;
|
||||
reg NV, DZ, OF, UF, NX;
|
||||
symfpu mod (.*);
|
||||
|
||||
wire a_sign = a[31];
|
||||
wire [30:0] a_unsigned = a[30:0];
|
||||
wire [7:0] a_exp = a[30:23];
|
||||
wire [22:0] a_sig = a[22:0];
|
||||
wire a_zero = a_unsigned == '0;
|
||||
wire a_special = a_exp == 8'hff;
|
||||
wire a_inf = a_special && a_sig == '0;
|
||||
wire a_nan = a_special && a_sig != '0;
|
||||
wire a_qnan = a_nan && a_sig[22] && a_sig[21:0] == '0;
|
||||
wire a_snan = a_nan && !a_sig[22];
|
||||
wire a_norm = a_exp > 8'h00 && !a_special;
|
||||
wire a_subnorm = a_exp == 8'h00 && a_sig != '0;
|
||||
wire a_finite = a_norm || a_subnorm;
|
||||
|
||||
wire b_sign = b[31];
|
||||
wire [30:0] b_unsigned = b[30:0];
|
||||
wire [7:0] b_exp = b[30:23];
|
||||
wire [22:0] b_sig = b[22:0];
|
||||
wire b_zero = b_unsigned == '0;
|
||||
wire b_special = b_exp == 8'hff;
|
||||
wire b_inf = b_special && b_sig == '0;
|
||||
wire b_nan = b_special && b_sig != '0;
|
||||
wire b_qnan = b_nan && b_sig[22];
|
||||
wire b_snan = b_nan && !b_sig[22];
|
||||
wire b_norm = b_exp > 8'h00 && !b_special;
|
||||
wire b_subnorm = b_exp == 8'h00 && b_sig != '0;
|
||||
wire b_finite = b_norm || b_subnorm;
|
||||
|
||||
wire c_sign = c[31];
|
||||
wire [30:0] c_unsigned = c[30:0];
|
||||
wire [7:0] c_exp = c[30:23];
|
||||
wire [22:0] c_sig = c[22:0];
|
||||
wire c_zero = c_unsigned == '0;
|
||||
wire c_special = c_exp == 8'hff;
|
||||
wire c_inf = c_special && c_sig == '0;
|
||||
wire c_nan = c_special && c_sig != '0;
|
||||
wire c_qnan = c_nan && c_sig[22];
|
||||
wire c_snan = c_nan && !c_sig[22];
|
||||
wire c_norm = c_exp > 8'h00 && !c_special;
|
||||
wire c_subnorm = c_exp == 8'h00 && c_sig != '0;
|
||||
wire c_finite = c_norm || c_subnorm;
|
||||
|
||||
wire o_sign = o[31];
|
||||
wire [30:0] o_unsigned = o[30:0];
|
||||
wire [7:0] o_exp = o[30:23];
|
||||
wire [22:0] o_sig = o[22:0];
|
||||
wire o_zero = o_unsigned == '0;
|
||||
wire o_special = o_exp == 8'hff;
|
||||
wire o_inf = o_special && o_sig == '0;
|
||||
wire o_nan = o_special && o_sig != '0;
|
||||
wire o_qnan = o_nan && o_sig[22];
|
||||
wire o_snan = o_nan && !o_sig[22];
|
||||
wire o_norm = o_exp > 8'h00 && !o_special;
|
||||
wire o_subnorm = o_exp == 8'h00 && o_sig != '0;
|
||||
wire o_finite = o_norm || o_subnorm;
|
||||
|
||||
`ifdef MULADD
|
||||
wire muladd_zero = c_zero;
|
||||
wire a_is_1 = a == 32'h3f800000;
|
||||
wire b_is_1 = b == 32'h3f800000;
|
||||
wire use_lhs = a_is_1 || b_is_1;
|
||||
wire lhs_sign = b_is_1 ? a_sign : b_sign;
|
||||
wire [30:0] lhs_unsigned = b_is_1 ? a_unsigned : b_unsigned;
|
||||
wire [7:0] lhs_exp = b_is_1 ? a_exp : b_exp;
|
||||
wire [22:0] lhs_sig = b_is_1 ? a_sig : b_sig;
|
||||
wire lhs_zero = b_is_1 ? a_zero : b_zero;
|
||||
wire lhs_inf = b_is_1 ? a_inf : b_inf;
|
||||
wire lhs_nan = b_is_1 ? a_nan : b_nan;
|
||||
wire lhs_qnan = b_is_1 ? a_qnan : b_qnan;
|
||||
wire lhs_snan = b_is_1 ? a_snan : b_snan;
|
||||
wire lhs_norm = b_is_1 ? a_norm : b_norm;
|
||||
wire lhs_subnorm = b_is_1 ? a_subnorm : b_subnorm;
|
||||
wire lhs_finite = b_is_1 ? a_finite : b_finite;
|
||||
|
||||
wire rhs_sign = c_sign;
|
||||
wire [30:0] rhs_unsigned = c_unsigned;
|
||||
wire [7:0] rhs_exp = c_exp;
|
||||
wire [22:0] rhs_sig = c_sig;
|
||||
wire rhs_zero = c_zero;
|
||||
wire rhs_inf = c_inf;
|
||||
wire rhs_nan = c_nan;
|
||||
wire rhs_qnan = c_qnan;
|
||||
wire rhs_snan = c_snan;
|
||||
wire rhs_norm = c_norm;
|
||||
wire rhs_subnorm = c_subnorm;
|
||||
wire rhs_finite = c_finite;
|
||||
`else
|
||||
wire muladd_zero = 1;
|
||||
wire use_lhs = 1;
|
||||
wire lhs_sign = a_sign;
|
||||
wire [30:0] lhs_unsigned = a_unsigned;
|
||||
wire [7:0] lhs_exp = a_exp;
|
||||
wire [22:0] lhs_sig = a_sig;
|
||||
wire lhs_zero = a_zero;
|
||||
wire lhs_inf = a_inf;
|
||||
wire lhs_nan = a_nan;
|
||||
wire lhs_qnan = a_qnan;
|
||||
wire lhs_snan = a_snan;
|
||||
wire lhs_norm = a_norm;
|
||||
wire lhs_subnorm = a_subnorm;
|
||||
wire lhs_finite = a_finite;
|
||||
|
||||
wire rhs_sign = b_sign;
|
||||
wire [30:0] rhs_unsigned = b_unsigned;
|
||||
wire [7:0] rhs_exp = b_exp;
|
||||
wire [22:0] rhs_sig = b_sig;
|
||||
wire rhs_zero = b_zero;
|
||||
wire rhs_inf = b_inf;
|
||||
wire rhs_nan = b_nan;
|
||||
wire rhs_qnan = b_qnan;
|
||||
wire rhs_snan = b_snan;
|
||||
wire rhs_norm = b_norm;
|
||||
wire rhs_subnorm = b_subnorm;
|
||||
wire rhs_finite = b_finite;
|
||||
`endif
|
||||
|
||||
`ifdef SUB
|
||||
wire is_sub = lhs_sign == rhs_sign;
|
||||
`else
|
||||
wire is_sub = lhs_sign != rhs_sign;
|
||||
`endif
|
||||
wire lhs_dominates = lhs_exp > rhs_exp;
|
||||
wire [7:0] exp_diff = lhs_dominates ? lhs_exp - rhs_exp : rhs_exp - lhs_exp;
|
||||
|
||||
always @* begin
|
||||
if (a_nan)
|
||||
// input NaN = output NaN
|
||||
assert (o_nan);
|
||||
|
||||
if (a_snan)
|
||||
// signalling NaN raises invalid exception
|
||||
assert (NV);
|
||||
|
||||
if (a_qnan && b_qnan && c_qnan)
|
||||
// quiet NaN inputs do not raise invalid exception
|
||||
assert (!NV);
|
||||
|
||||
if (DZ)
|
||||
// output = +-inf
|
||||
assert (o_inf);
|
||||
|
||||
if (NV)
|
||||
// output = qNaN
|
||||
assert (o_qnan);
|
||||
|
||||
if (OF)
|
||||
// overflow is always inexact
|
||||
assert (NX);
|
||||
|
||||
if (UF)
|
||||
// underflow is always inexact
|
||||
assert (NX);
|
||||
|
||||
if (OF) begin
|
||||
// for RNE, output = +=inf
|
||||
assert (o_inf);
|
||||
end
|
||||
|
||||
if (UF)
|
||||
// output = subnormal
|
||||
assert (o_subnorm);
|
||||
|
||||
if (o_inf && !OF)
|
||||
// a non-overflowing infinity is exact
|
||||
assert (!NX);
|
||||
|
||||
if (o_subnorm && !UF)
|
||||
// a non-underflowing subnormal is exact
|
||||
assert (!NX);
|
||||
|
||||
`ifdef DIV
|
||||
// a = finite, b = 0
|
||||
if ((a_norm || a_subnorm) && b_unsigned == '0)
|
||||
assert (DZ);
|
||||
// 0/0 or inf/inf
|
||||
if ((a_zero && b_zero) || (a_inf && b_inf))
|
||||
assert (NV);
|
||||
// dividing by a very small number will overflow
|
||||
if (a_norm && a_exp > 8'h80 && b == 32'h00000001)
|
||||
assert (OF);
|
||||
// dividing by a much smaller number will overflow
|
||||
if (a_norm && b_finite && lhs_dominates && exp_diff > 8'h80)
|
||||
assert (OF);
|
||||
// dividing by a much larger number will hit 0 bias
|
||||
if (a_finite && b_norm && !lhs_dominates && exp_diff > 8'h7f) begin
|
||||
assert (o_exp == '0);
|
||||
// if the divisor is large enough, underflow (or zero) is guaranteed
|
||||
if (exp_diff > 8'h95) begin
|
||||
assert (NX);
|
||||
assert (UF || o_zero);
|
||||
end
|
||||
end
|
||||
`endif
|
||||
|
||||
`ifdef MULS
|
||||
// 0/inf or inf/0
|
||||
if ((a_inf && b_zero) || (a_zero && b_inf))
|
||||
assert (NV);
|
||||
// very large multiplications overflow
|
||||
if (a_unsigned == 31'h7f400000 && b_unsigned == a_unsigned && !c_special)
|
||||
assert (OF);
|
||||
// multiplying a small number by an even smaller number will underflow
|
||||
if (a_norm && a_exp < 8'h60 && b_subnorm && !c_special) begin
|
||||
assert (NX);
|
||||
`ifdef MULADD
|
||||
assert (UF || (c_zero ? o_zero : o == c));
|
||||
`else
|
||||
assert (UF || o_zero);
|
||||
`endif
|
||||
if (o_zero)
|
||||
assert (o_sign == a_sign ^ b_sign);
|
||||
end
|
||||
`endif
|
||||
|
||||
`ifdef ADDSUB
|
||||
// adder can't underflow, subnormals are always exact
|
||||
assert (!UF);
|
||||
`endif
|
||||
|
||||
`ifdef ADDS
|
||||
if (use_lhs) begin
|
||||
// inf - inf
|
||||
if (lhs_inf && rhs_inf && is_sub)
|
||||
assert (NV);
|
||||
// very large additions overflow
|
||||
if (lhs_unsigned == 31'h7f400000 && rhs_unsigned == lhs_unsigned && !is_sub)
|
||||
assert (OF);
|
||||
// if the difference in exponent is more than the width of the mantissa,
|
||||
// the result cannot be exact
|
||||
if (lhs_finite && rhs_finite && exp_diff > 8'd24)
|
||||
assert (NX || OF);
|
||||
if (!UF) begin
|
||||
// for a small difference in exponent with zero LSB, the result must be
|
||||
// exact
|
||||
if (o_finite && lhs_dominates && exp_diff < 8'd08 && rhs_sig[7:0] == 0 && lhs_sig[7:0] == 0)
|
||||
assert (!NX);
|
||||
if (exp_diff == 0 && !OF && lhs_sig[7:0] == 0 && rhs_sig[7:0] == 0)
|
||||
assert (!NX);
|
||||
end
|
||||
// there's probably a better general case for this, but a moderate
|
||||
// difference in exponent with non zero LSB must be inexact
|
||||
if (o_finite && lhs_dominates && exp_diff > 8'd09 && rhs_sig[7:0] != 0 && lhs_sig[7:0] == 0)
|
||||
assert (NX);
|
||||
end
|
||||
`endif
|
||||
|
||||
`ifdef MULADD
|
||||
// not sure how to check this in the generic case since we don't have the partial mul
|
||||
if ((a_inf || b_inf) && !(a_nan || b_nan) && c_inf && (a_sign ^ b_sign ^ c_sign))
|
||||
assert (NV);
|
||||
// normal multiplication, overflow addition
|
||||
if (a == 31'h5f400000 && b == a && c == 32'h7f400000) begin
|
||||
assert (OF);
|
||||
assert (o_inf); // assuming RNE
|
||||
end
|
||||
// if multiplication overflows, addition can bring it back in range
|
||||
if (a == 32'hc3800001 && b == 32'h7b800000 && !c_special) begin
|
||||
if (c_sign)
|
||||
// result is negative, so a negative addend can't
|
||||
assert (OF);
|
||||
else if (c_exp <= 8'he7)
|
||||
// addend can't be too small
|
||||
assert (OF);
|
||||
else if (c_exp == 8'he8 && c_sig <= 22'h200000)
|
||||
// this is just the turning point for this particular value
|
||||
assert (OF);
|
||||
else
|
||||
// a large enough positive addend will never overflow (but is
|
||||
// still likely to be inexact)
|
||||
assert (!OF);
|
||||
end
|
||||
`endif
|
||||
|
||||
`ifdef SQRT
|
||||
// complex roots are invalid
|
||||
if (a_sign && (a_norm || a_subnorm))
|
||||
assert (NV);
|
||||
`endif
|
||||
|
||||
end
|
||||
endmodule
|
||||
35
tests/symfpu/run-test.sh
Executable file
35
tests/symfpu/run-test.sh
Executable file
|
|
@ -0,0 +1,35 @@
|
|||
#!/usr/bin/env bash
|
||||
set -eu
|
||||
|
||||
source ../gen-tests-makefile.sh
|
||||
|
||||
ops="sqrt add sub mul div muladd"
|
||||
for op in $ops; do
|
||||
rm -f ${op}_edges.*
|
||||
done
|
||||
|
||||
prove_op() {
|
||||
op=$1
|
||||
defs=$2
|
||||
ys_file=${op}_edges.ys
|
||||
echo """\
|
||||
symfpu -op $op
|
||||
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_op sqrt "-DSQRT"
|
||||
prove_op add "-DADD -DADDSUB -DADDS"
|
||||
prove_op sub "-DSUB -DADDSUB -DADDS"
|
||||
prove_op mul "-DMUL -DMULS"
|
||||
prove_op div "-DDIV"
|
||||
prove_op muladd "-DMULADD -DMULS -DADDS"
|
||||
|
||||
generate_mk --yosys-scripts
|
||||
Loading…
Add table
Add a link
Reference in a new issue