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 5aee853. ± 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.

[Timmmm]

@jrtc27 is the ok now? I'll merge in a week if nobody objects...