Fix RV64F compilation, simplify fmv implementation, and make nan boxing functions generic

[Timmmm]

Simplify the implementations with fewer intermediate variables, and fix compilation of RV64F.

I also added relevant quote from the spec because the spec for these instructions is very confusing. This is a prime candidate for getting Sail code into the spec.

Fixes #556

[github-actions]

Test Results

396 tests  ±0   396 ✅ ±0   0s ⏱️ ±0s
  4 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit e204f5e. ± Comparison against base commit b8d1fa5.

♻️ This comment has been updated with latest results.

[arichardson]

Minor nit: The title of the commit sounds like there is an implementation bug. Maybe Fix RV64F compilation and simplify fmv implementation?

Change LGTM.

[jordancarlin]

Looks good with the latest changes. A nice cleanup + fixes a clear problem with building the model.

[Timmmm]

Btw canonical_NaN() can actually be completely generic with some of the new Sail library code:

$include <float/common.sail>

val canonical_NaN : forall 'n, 'n in {16, 32, 64, 128} . (implicit('n)) -> bits('n)
function canonical_NaN(n) = float_compose(struct {
    sign = 0b0,
    exp = ones(),
    mantissa = 0b1 @ zeros(),
  })

Ok actually that's not quite true. <float/common.sail> is missing float_compose, but it's very simple (I'll make a PR):

val      float_compose : forall 'n, 'n in { 16, 32, 64, 128 }. float_bits('n) -> bits('n)
function float_compose(op) = op.sign @ op.exp @ op.mantissa

And also 0b1 @ zeros() doesn't quite work, so you currently need this full code:

$include <float/common.sail>

val      float_compose : forall 'n, 'n in { 16, 32, 64, 128 }. float_bits('n) -> bits('n)
function float_compose(op) = op.sign @ op.exp @ op.mantissa

val leading_one : forall 'n, 'n >= 1. (implicit('n)) -> bits('n)
function leading_one(n) = 0b1 @ zeros('n - 1)

val canonical_NaN : forall 'n, 'n in {16, 32, 64, 128} . (implicit('n)) -> bits('n)
function canonical_NaN(n) = float_compose(struct {
    sign = 0b0,
    exp = ones(),
    mantissa = leading_one(),
  })

Very cool though right? IMO we should do this in future and switch the _D suffixed versions to pass integers in.

[arichardson]

Btw canonical_NaN() can actually be completely generic with some of the new Sail library code:

$include <float/common.sail>

val canonical_NaN : forall 'n, 'n in {16, 32, 64, 128} . (implicit('n)) -> bits('n)
function canonical_NaN(n) = float_compose(struct {
    sign = 0b0,
    exp = ones(),
    mantissa = 0b1 @ zeros(),
  })

Ok actually that's not quite true. <float/common.sail> is missing float_compose, but it's very simple (I'll make a PR):

val      float_compose : forall 'n, 'n in { 16, 32, 64, 128 }. float_bits('n) -> bits('n)
function float_compose(op) = op.sign @ op.exp @ op.mantissa

And also 0b1 @ zeros() doesn't quite work, so you currently need this full code:

$include <float/common.sail>

val      float_compose : forall 'n, 'n in { 16, 32, 64, 128 }. float_bits('n) -> bits('n)
function float_compose(op) = op.sign @ op.exp @ op.mantissa

val leading_one : forall 'n, 'n >= 1. (implicit('n)) -> bits('n)
function leading_one(n) = 0b1 @ zeros('n - 1)

val canonical_NaN : forall 'n, 'n in {16, 32, 64, 128} . (implicit('n)) -> bits('n)
function canonical_NaN(n) = float_compose(struct {
    sign = 0b0,
    exp = ones(),
    mantissa = leading_one(),
  })

Very cool though right? IMO we should do this in future and switch the _D suffixed versions to pass integers in.

Yes this looks much nicer!

[jordancarlin]

Very cool though right? IMO we should do this in future and switch the _D suffixed versions to pass integers in.

Definitely nicer that way. For now you could put the logic for the matching in the canonical_NaN function (more similar to what you had initially) and have the _D suffixed versions pass the integer in now. That way there is less changing and it would just be the internals of that one function that get modified later.

[jrtc27]

Very cool though right? IMO we should do this in future and switch the _D suffixed versions to pass integers in.

Definitely nicer that way. For now you could put the logic for the matching in the canonical_NaN function (more similar to what you had initially) and have the _D suffixed versions pass the integer in now. That way there is less changing and it would just be the internals of that one function that get modified later.

Yeah, having the suffixed versions be wrappers around the integer-taking version was what I was imagining.

[Timmmm]

Yeah, having the suffixed versions be wrappers around the integer-taking version was what I was imagining.

Ok I updated it to this.

[jrtc27]

Not just stored, using as an input to some computation sees the same thing, right? As in this is just a property of any read of a non-NaN-boxed value?

[jrtc27]

And in particular transfer instructions (FLn/FSn/FMV.n.X/FMV.X.n) don't do this, despite storing in a smaller register.

[Timmmm]

Ah yeah you're right I didn't really describe it correctly (and I think the spec is not especially readable). How about this:

// Except for floating-point transfer instructions (FSn and FMV.n.X),
// n-bit reads of a >n-bit floating point register "unboxes" the value stored
// in the register. If the register does not contain a valid boxed value
// then a canonical NaN value is returned instead.

and

// n-bit writes to a >n-bit floating point register "boxes" the value
// by prepending 1s, which turn it into a qNaN.

[jrtc27]

(un)boxes should be (un)box as you have plural reads/writes, but yes that looks ok to me otherwise