Deduplicate some floating point code

[Timmmm]

This is an initial effort to deduplicate the floating point code (see #432). Currently all the floating point code is copy/pasted for every size of float (f16, f32, f64). That's very verbose and error prone and is going to get worse if people want f128!

It's also unnecessary because Sail has an amazing type system so it can easily deal with functions that are generic over the size of the float.

Note, this PR is composed of 6 commits which all build and work, so I would recommend a rebase merge rather than a squash merge to preserve the history.

Normally I would make the PRs in series, but 6 PRs is going to take like a year to get through our review system so I'm doing it all in one! I recommend reviewing the individual commits though.

Also note some of the changes look like they are kind of pointless, e.g. F_or_X_H(rs1) to F_or_X(16, rs1), but that's just because this is only part of the solution.

[Timmmm]

@Incarnation-p-lee you might be interested in some of this code, especially these functions - took me a little while to get the types figured out!

// Split a floating point bitvec up into its sign, exponent, mantissa parts.
val fsplit : forall 'n, 'n in {16, 32, 64}.
  bits('n) -> (
    bits(1),
    bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
    bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
  )
function fsplit(x) = {
  if      'n == 16 then (x[15..15], x[14..10], x[9..0])
  else if 'n == 32 then (x[31..31], x[30..23], x[22..0])
  else                  (x[63..63], x[62..52], x[51..0])
}

// Join sign, exponent, mantissa parts back into a single bit vector.
val fmake : forall 'e, 'e in {5, 8, 11}.
  (
    bits(1),
    bits('e),
    bits(if 'e == 5 then 10 else (if 'e == 8 then 23 else 52)),
  ) -> bits(if 'e == 5 then 16 else (if 'e == 8 then 32 else 64))
function fmake(sign, exp, mant) = sign @ exp @ mant

But with those you can do generic functions like

// Bit vector type for floating points - restricted to f16, f32, f64.
type fbits = { 'n, 'n in {16, 32, 64}. bits('n) }

function f_is_neg_inf(x : fbits) -> bool = {
  let (sign, exp, mant) = fsplit(x);
  (  (sign == 0b1)
   & (exp  == ones())
   & (mant == zeros()))
}

and it all type checks nicely.

[github-actions]

Test Results

712 tests  ±0     0 ✅  - 712   0s ⏱️ ±0s
  6 suites ±0     0 💤 ±  0 
  1 files   ±0   712 ❌ +712 

For more details on these failures, see this check.

Results for commit cf7553b. ± Comparison against base commit a2ffa85.

[Incarnation-p-lee]

Thanks @Timmmm . That is very cool, I suppose this is what I need shortly. Just complete the API design draft doc, and will work out a POC on the sail side. I bet that will be very helpful.

[Timmmm]

I think this probably failed to using an old version of Sail. I will make a PR to update it.

[Timmmm]

Oh actually it turns out type level if-then-else was only added to Sail three weeks ago! Very timely. But it means we'll need to wait for the next Sail release for this to compile.

[Incarnation-p-lee]

Oh actually it turns out type level if-then-else was only added to Sail three weeks ago! Very timely. But it means we'll need to wait for the next Sail release for this to compile.

Got it, I suppose I can leverage SAIL_DIR to the new built one from the sail repo. Let me have a try later(in the middle of fixing ICE for GCC ...) and keep you posted.

[Incarnation-p-lee]

Not sure if below parts can transform to

  bits('n) -> (
    bits(1),
    bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
    bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
  )

=>

  bits('n) -> (
    bits(1),
    bits(match 'n {
       16 => 5,
       32 => 8,
       64 => 11,
    }),
    bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
  )

That would be more friendly for reading, specially when we add fp128 support.

[Incarnation-p-lee]

Not sure if below parts can transform to

  bits('n) -> (
    bits(1),
    bits(if 'n == 16 then 5 else (if 'n == 32 then 8 else 11)),
    bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
  )

=>

  bits('n) -> (
    bits(1),
    bits(match 'n {
       16 => 5,
       32 => 8,
       64 => 11,
    }),
    bits(if 'n == 16 then 10 else (if 'n == 32 then 23 else 52)),
  )

That would be more friendly for reading, specially when we add fp128 support.

Unfortunately not work for matches in bits now.
Another interest found for types, looks we can leverage tuple for arg nums > 1.

val feq_quiet : forall 'n, 'n in {16, 32, 64}. (bits('n), bits('n)) -> (bool, bits_fflags)
function feq_quiet(v1, v2) = { }

=>

type fp_bits_x2 = { 'n, 'n in {16, 32, 64}. (bits('n), bits('n)) }
val      feq_quiet : (fp_bits_x2) -> (bool, bits_fflags)
function feq_quiet (tuple) = {
  let (v1, v2) = tuple;
}

[aamartin0000]

Hello, switching on width alone may not be adequate for future-proofing. For example, there is already BF16 format along with "standard" FP16, for 16-bit width floats (see Zfbf). AI/ML will also be adding a variety of 8-, and possibly even 6- or 4-bit floats. (These may only be supported in the vector or matrix instruction sets, and may not even be IEEE754 compliant.) The formats we will support, which differ in the allocation of exponent vs. significand bits, has not yet been nailed down.

The point is, if you're changing this code, it may as well be done in a more generic fashion that will work with these future formats.

[Timmmm]

Hmm that is a good point. Unfortunately I don't think Sail supports type level enums so supporting multiple 16-bit float formats in this way is going to be a bit tricky.

Perhaps the best solution is to make all the functions generic over the split sizes, instead of the total size. Like instead of

function f_is_pos_zero(x : fbits) -> bool = {
  let (sign, exp, mant) = fsplit(x);
  (  (sign == zeros())
   & (exp  == zeros())
   & (mant == zeros()))
}

have

function f_is_pos_zero(sign : fsign, exp : fexp, mant : fmant) -> bool = {
  (  (sign == zeros())
   & (exp  == zeros())
   & (mant == zeros()))
}

Quite a bit more tedious to use though. Perhaps we should cross that bridge when we come to it. At the very worst those weird formats can copy & paste the implementations as they would have to now.

[aamartin0000]

Whatever you feel is best. I just wanted to make sure you were aware of the situation, so that any change you make now won't make it really hard to change later on when these new formats come into use.

You still need to figure out how to deal with FP16 vs BF16, and that could provide a template for all the other formats to be added. Rather than the width, maybe you could key off of opcode bits? Hardware decode logic has to do it this way.

[Incarnation-p-lee]

Hi @Timmmm, Just FYI, the sail side accept the float bits representation in structure, more details can be located here.

[Timmmm]

Closing this since we can use the code included in Sail instead.