From abf0427f7365184e8869ac22d4958fe5aced2086 Mon Sep 17 00:00:00 2001
From: Tim Hutt <timothy.hutt@codasip.com>
Date: Fri, 21 Jul 2023 12:25:10 +0100
Subject: [PATCH] Remove dependence of C softfloat code on Sail model.

The flags and result for a softfloat operation are currently pushed to the Sail code from C like this:

    // C
    zfloat_result = res.v;
    zfloat_fflags = (mach_bits)softfloat_exceptionFlags

    // Sail
    register float_result : bits(64)
    register float_fflags : bits(64)

This changes it to pull the flags from the Sail side with a callback:

    // C
    mach_bits softfloat_float_flags(unit u)
    {
      return (mach_bits)softfloat_exceptionFlags;
    }
    // Sail
    val extern_float_flags = {c: "softfloat_float_flags", ocaml: "Softfloat.float_flags", lem: "softfloat_float_flags"} : (unit) -> bits_LU

The `float_result` is changed to just be the return value of all of the functions.

The benefits are:

1. It uses the official FFI system instead of hackily reaching into the generated C code.
2. It removes the two-way dependence between the C softfloat code and the Sail model. The C softfloat code no longer has any references to the Sail model.

Tested with `run_fp_tests.sh` - all 82 tests pass.
---
 c_emulator/riscv_softfloat.c         | 406 +++++++++-----------------
 c_emulator/riscv_softfloat.h         | 168 +++++------
 model/riscv_softfloat_interface.sail | 411 ++++++++++++++-------------
 3 files changed, 430 insertions(+), 555 deletions(-)

diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c
index 2c2d0d2b2..2ba5e176f 100644
--- a/c_emulator/riscv_softfloat.c
+++ b/c_emulator/riscv_softfloat.c
@@ -14,11 +14,12 @@ static uint_fast8_t uint8_of_rm(mach_bits rm)
   softfloat_exceptionFlags = 0;                                                \
   softfloat_roundingMode = (uint_fast8_t)rm
 
-#define SOFTFLOAT_POSTLUDE(res)                                                \
-  zfloat_result = res.v;                                                       \
-  zfloat_fflags = (mach_bits)softfloat_exceptionFlags
+mach_bits softfloat_float_flags(unit u)
+{
+  return (mach_bits)softfloat_exceptionFlags;
+}
 
-unit softfloat_f16add(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f16add(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -27,12 +28,10 @@ unit softfloat_f16add(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f16_add(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16sub(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f16sub(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -41,12 +40,10 @@ unit softfloat_f16sub(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f16_sub(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16mul(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f16mul(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -55,12 +52,10 @@ unit softfloat_f16mul(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f16_mul(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16div(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f16div(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -69,12 +64,10 @@ unit softfloat_f16div(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f16_div(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -83,12 +76,10 @@ unit softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f32_add(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -97,12 +88,10 @@ unit softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f32_sub(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -111,12 +100,10 @@ unit softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f32_mul(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -125,12 +112,10 @@ unit softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f32_div(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -139,12 +124,10 @@ unit softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f64_add(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -153,12 +136,10 @@ unit softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f64_sub(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -167,12 +148,10 @@ unit softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f64_mul(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2)
+mach_bits softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -181,12 +160,11 @@ unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2)
   b.v = v2;
   res = f64_div(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3)
+mach_bits softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2,
+                              mach_bits v3)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -196,12 +174,11 @@ unit softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3)
   c.v = v3;
   res = f16_mulAdd(a, b, c);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3)
+mach_bits softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2,
+                              mach_bits v3)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -211,12 +188,11 @@ unit softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3)
   c.v = v3;
   res = f32_mulAdd(a, b, c);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3)
+mach_bits softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2,
+                              mach_bits v3)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -226,12 +202,10 @@ unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3)
   c.v = v3;
   res = f64_mulAdd(a, b, c);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16sqrt(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16sqrt(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -239,12 +213,10 @@ unit softfloat_f16sqrt(mach_bits rm, mach_bits v)
   a.v = v;
   res = f16_sqrt(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32sqrt(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32sqrt(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -252,12 +224,10 @@ unit softfloat_f32sqrt(mach_bits rm, mach_bits v)
   a.v = v;
   res = f32_sqrt(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64sqrt(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64sqrt(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -265,15 +235,13 @@ unit softfloat_f64sqrt(mach_bits rm, mach_bits v)
   a.v = v;
   res = f64_sqrt(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
 // The boolean 'true' argument in the conversion calls below selects
 // 'exact' conversion, which sets the Inexact exception flag if
 // needed.
-unit softfloat_f16toi32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16toi32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -283,12 +251,10 @@ unit softfloat_f16toi32(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f16_to_i32(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16toui32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16toui32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -298,12 +264,10 @@ unit softfloat_f16toui32(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f16_to_ui32(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16toi64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16toi64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -313,12 +277,10 @@ unit softfloat_f16toi64(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f16_to_i64(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16toui64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16toui64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -328,12 +290,10 @@ unit softfloat_f16toui64(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f16_to_ui64(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32toi32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32toi32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -342,12 +302,10 @@ unit softfloat_f32toi32(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f32_to_i32(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32toui32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32toui32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -356,12 +314,10 @@ unit softfloat_f32toui32(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f32_to_ui32(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32toi64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32toi64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -371,12 +327,10 @@ unit softfloat_f32toi64(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f32_to_i64(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32toui64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32toui64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -386,12 +340,10 @@ unit softfloat_f32toui64(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f32_to_ui64(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64toi32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64toi32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -401,12 +353,10 @@ unit softfloat_f64toi32(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f64_to_i32(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64toui32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64toui32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -416,12 +366,10 @@ unit softfloat_f64toui32(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f64_to_ui32(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64toi64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64toi64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -430,12 +378,10 @@ unit softfloat_f64toi64(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f64_to_i64(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64toui64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64toui64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -444,156 +390,130 @@ unit softfloat_f64toui64(mach_bits rm, mach_bits v)
   a.v = v;
   res.v = f64_to_ui64(a, rm8, true);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_i32tof16(mach_bits rm, mach_bits v)
+mach_bits softfloat_i32tof16(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float16_t res;
   res = i32_to_f16((int32_t)v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_ui32tof16(mach_bits rm, mach_bits v)
+mach_bits softfloat_ui32tof16(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float16_t res;
   res = ui32_to_f16((uint32_t)v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_i64tof16(mach_bits rm, mach_bits v)
+mach_bits softfloat_i64tof16(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float16_t res;
   res = i64_to_f16(v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_ui64tof16(mach_bits rm, mach_bits v)
+mach_bits softfloat_ui64tof16(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float16_t res;
   res = ui64_to_f16(v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_i32tof32(mach_bits rm, mach_bits v)
+mach_bits softfloat_i32tof32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float32_t res;
   res = i32_to_f32((int32_t)v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_ui32tof32(mach_bits rm, mach_bits v)
+mach_bits softfloat_ui32tof32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float32_t res;
   res = ui32_to_f32((uint32_t)v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_i64tof32(mach_bits rm, mach_bits v)
+mach_bits softfloat_i64tof32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float32_t res;
   res = i64_to_f32(v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_ui64tof32(mach_bits rm, mach_bits v)
+mach_bits softfloat_ui64tof32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float32_t res;
   res = ui64_to_f32(v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_i32tof64(mach_bits rm, mach_bits v)
+mach_bits softfloat_i32tof64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float64_t res;
   res = i32_to_f64((int32_t)v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_ui32tof64(mach_bits rm, mach_bits v)
+mach_bits softfloat_ui32tof64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float64_t res;
   res = ui32_to_f64((uint32_t)v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_i64tof64(mach_bits rm, mach_bits v)
+mach_bits softfloat_i64tof64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float64_t res;
   res = i64_to_f64(v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_ui64tof64(mach_bits rm, mach_bits v)
+mach_bits softfloat_ui64tof64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
   float64_t res;
   res = ui64_to_f64(v);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16tof32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16tof32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -602,12 +522,10 @@ unit softfloat_f16tof32(mach_bits rm, mach_bits v)
   a.v = v;
   res = f16_to_f32(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16tof64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f16tof64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -616,12 +534,10 @@ unit softfloat_f16tof64(mach_bits rm, mach_bits v)
   a.v = v;
   res = f16_to_f64(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32tof64(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32tof64(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -630,12 +546,10 @@ unit softfloat_f32tof64(mach_bits rm, mach_bits v)
   a.v = v;
   res = f32_to_f64(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32tof16(mach_bits rm, mach_bits v)
+mach_bits softfloat_f32tof16(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -644,12 +558,10 @@ unit softfloat_f32tof16(mach_bits rm, mach_bits v)
   a.v = v;
   res = f32_to_f16(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64tof16(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64tof16(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -658,12 +570,10 @@ unit softfloat_f64tof16(mach_bits rm, mach_bits v)
   a.v = v;
   res = f64_to_f16(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64tof32(mach_bits rm, mach_bits v)
+mach_bits softfloat_f64tof32(mach_bits rm, mach_bits v)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -672,12 +582,10 @@ unit softfloat_f64tof32(mach_bits rm, mach_bits v)
   a.v = v;
   res = f64_to_f32(a);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f16lt(mach_bits v1, mach_bits v2)
+bool softfloat_f16lt(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -686,12 +594,10 @@ unit softfloat_f16lt(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f16_lt(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f16lt_quiet(mach_bits v1, mach_bits v2)
+bool softfloat_f16lt_quiet(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -700,12 +606,10 @@ unit softfloat_f16lt_quiet(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f16_lt_quiet(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f16le(mach_bits v1, mach_bits v2)
+bool softfloat_f16le(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -714,12 +618,10 @@ unit softfloat_f16le(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f16_le(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f16le_quiet(mach_bits v1, mach_bits v2)
+bool softfloat_f16le_quiet(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -728,12 +630,10 @@ unit softfloat_f16le_quiet(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f16_le_quiet(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f16eq(mach_bits v1, mach_bits v2)
+bool softfloat_f16eq(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -742,12 +642,10 @@ unit softfloat_f16eq(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f16_eq(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f32lt(mach_bits v1, mach_bits v2)
+bool softfloat_f32lt(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -756,12 +654,10 @@ unit softfloat_f32lt(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f32_lt(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f32lt_quiet(mach_bits v1, mach_bits v2)
+bool softfloat_f32lt_quiet(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -770,12 +666,10 @@ unit softfloat_f32lt_quiet(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f32_lt_quiet(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f32le(mach_bits v1, mach_bits v2)
+bool softfloat_f32le(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -784,12 +678,10 @@ unit softfloat_f32le(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f32_le(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f32le_quiet(mach_bits v1, mach_bits v2)
+bool softfloat_f32le_quiet(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -798,12 +690,10 @@ unit softfloat_f32le_quiet(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f32_le_quiet(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f32eq(mach_bits v1, mach_bits v2)
+bool softfloat_f32eq(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -812,12 +702,10 @@ unit softfloat_f32eq(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f32_eq(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f64lt(mach_bits v1, mach_bits v2)
+bool softfloat_f64lt(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -826,12 +714,10 @@ unit softfloat_f64lt(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f64_lt(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f64lt_quiet(mach_bits v1, mach_bits v2)
+bool softfloat_f64lt_quiet(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -840,12 +726,10 @@ unit softfloat_f64lt_quiet(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f64_lt_quiet(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f64le(mach_bits v1, mach_bits v2)
+bool softfloat_f64le(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -854,12 +738,10 @@ unit softfloat_f64le(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f64_le(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f64le_quiet(mach_bits v1, mach_bits v2)
+bool softfloat_f64le_quiet(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -868,12 +750,10 @@ unit softfloat_f64le_quiet(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f64_le_quiet(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f64eq(mach_bits v1, mach_bits v2)
+bool softfloat_f64eq(mach_bits v1, mach_bits v2)
 {
   SOFTFLOAT_PRELUDE(0);
 
@@ -882,12 +762,10 @@ unit softfloat_f64eq(mach_bits v1, mach_bits v2)
   b.v = v2;
   res.v = f64_eq(a, b);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v != 0;
 }
 
-unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact)
+mach_bits softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -896,12 +774,10 @@ unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact)
   a.v = v;
   res = f16_roundToInt(a, rm8, exact);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact)
+mach_bits softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -910,12 +786,10 @@ unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact)
   a.v = v;
   res = f32_roundToInt(a, rm8, exact);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
 
-unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact)
+mach_bits softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact)
 {
   SOFTFLOAT_PRELUDE(rm);
 
@@ -924,7 +798,5 @@ unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact)
   a.v = v;
   res = f64_roundToInt(a, rm8, exact);
 
-  SOFTFLOAT_POSTLUDE(res);
-
-  return UNIT;
+  return res.v;
 }
diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h
index fc7b2252e..2ef0d1ed9 100644
--- a/c_emulator/riscv_softfloat.h
+++ b/c_emulator/riscv_softfloat.h
@@ -1,85 +1,87 @@
 #pragma once
 
-unit softfloat_f16add(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f16sub(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f16mul(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f16div(mach_bits rm, mach_bits v1, mach_bits v2);
-
-unit softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2);
-
-unit softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2);
-unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2);
-
-unit softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2,
-                         mach_bits v3);
-unit softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2,
-                         mach_bits v3);
-unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2,
-                         mach_bits v3);
-
-unit softfloat_f16sqrt(mach_bits rm, mach_bits v);
-unit softfloat_f32sqrt(mach_bits rm, mach_bits v);
-unit softfloat_f64sqrt(mach_bits rm, mach_bits v);
-
-unit softfloat_f16toi32(mach_bits rm, mach_bits v);
-unit softfloat_f16toui32(mach_bits rm, mach_bits v);
-unit softfloat_f16toi64(mach_bits rm, mach_bits v);
-unit softfloat_f16toui64(mach_bits rm, mach_bits v);
-
-unit softfloat_f32toi32(mach_bits rm, mach_bits v);
-unit softfloat_f32toui32(mach_bits rm, mach_bits v);
-unit softfloat_f32toi64(mach_bits rm, mach_bits v);
-unit softfloat_f32toui64(mach_bits rm, mach_bits v);
-
-unit softfloat_f64toi32(mach_bits rm, mach_bits v);
-unit softfloat_f64toui32(mach_bits rm, mach_bits v);
-unit softfloat_f64toi64(mach_bits rm, mach_bits v);
-unit softfloat_f64toui64(mach_bits rm, mach_bits v);
-
-unit softfloat_i32tof16(mach_bits rm, mach_bits v);
-unit softfloat_ui32tof16(mach_bits rm, mach_bits v);
-unit softfloat_i64tof16(mach_bits rm, mach_bits v);
-unit softfloat_ui64tof16(mach_bits rm, mach_bits v);
-
-unit softfloat_i32tof32(mach_bits rm, mach_bits v);
-unit softfloat_ui32tof32(mach_bits rm, mach_bits v);
-unit softfloat_i64tof32(mach_bits rm, mach_bits v);
-unit softfloat_ui64tof32(mach_bits rm, mach_bits v);
-
-unit softfloat_i32tof64(mach_bits rm, mach_bits v);
-unit softfloat_ui32tof64(mach_bits rm, mach_bits v);
-unit softfloat_i64tof64(mach_bits rm, mach_bits v);
-unit softfloat_ui64tof64(mach_bits rm, mach_bits v);
-
-unit softfloat_f16tof32(mach_bits rm, mach_bits v);
-unit softfloat_f16tof64(mach_bits rm, mach_bits v);
-unit softfloat_f32tof64(mach_bits rm, mach_bits v);
-
-unit softfloat_f32tof16(mach_bits rm, mach_bits v);
-unit softfloat_f64tof16(mach_bits rm, mach_bits v);
-unit softfloat_f64tof32(mach_bits rm, mach_bits v);
-
-unit softfloat_f16lt(mach_bits v1, mach_bits v2);
-unit softfloat_f16lt_quiet(mach_bits v1, mach_bits v2);
-unit softfloat_f16le(mach_bits v1, mach_bits v2);
-unit softfloat_f16le_quiet(mach_bits v1, mach_bits v2);
-unit softfloat_f16eq(mach_bits v1, mach_bits v2);
-unit softfloat_f32lt(mach_bits v1, mach_bits v2);
-unit softfloat_f32lt_quiet(mach_bits v1, mach_bits v2);
-unit softfloat_f32le(mach_bits v1, mach_bits v2);
-unit softfloat_f32le_quiet(mach_bits v1, mach_bits v2);
-unit softfloat_f32eq(mach_bits v1, mach_bits v2);
-unit softfloat_f64lt(mach_bits v1, mach_bits v2);
-unit softfloat_f64lt_quiet(mach_bits v1, mach_bits v2);
-unit softfloat_f64le(mach_bits v1, mach_bits v2);
-unit softfloat_f64le_quiet(mach_bits v1, mach_bits v2);
-unit softfloat_f64eq(mach_bits v1, mach_bits v2);
-
-unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact);
-unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact);
-unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact);
+mach_bits softfloat_float_flags(unit);
+
+mach_bits softfloat_f16add(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f16sub(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f16mul(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f16div(mach_bits rm, mach_bits v1, mach_bits v2);
+
+mach_bits softfloat_f32add(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f32sub(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f32mul(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f32div(mach_bits rm, mach_bits v1, mach_bits v2);
+
+mach_bits softfloat_f64add(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f64sub(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f64mul(mach_bits rm, mach_bits v1, mach_bits v2);
+mach_bits softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2);
+
+mach_bits softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2,
+                              mach_bits v3);
+mach_bits softfloat_f32muladd(mach_bits rm, mach_bits v1, mach_bits v2,
+                              mach_bits v3);
+mach_bits softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2,
+                              mach_bits v3);
+
+mach_bits softfloat_f16sqrt(mach_bits rm, mach_bits v);
+mach_bits softfloat_f32sqrt(mach_bits rm, mach_bits v);
+mach_bits softfloat_f64sqrt(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_f16toi32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f16toui32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f16toi64(mach_bits rm, mach_bits v);
+mach_bits softfloat_f16toui64(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_f32toi32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f32toui32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f32toi64(mach_bits rm, mach_bits v);
+mach_bits softfloat_f32toui64(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_f64toi32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f64toui32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f64toi64(mach_bits rm, mach_bits v);
+mach_bits softfloat_f64toui64(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_i32tof16(mach_bits rm, mach_bits v);
+mach_bits softfloat_ui32tof16(mach_bits rm, mach_bits v);
+mach_bits softfloat_i64tof16(mach_bits rm, mach_bits v);
+mach_bits softfloat_ui64tof16(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_i32tof32(mach_bits rm, mach_bits v);
+mach_bits softfloat_ui32tof32(mach_bits rm, mach_bits v);
+mach_bits softfloat_i64tof32(mach_bits rm, mach_bits v);
+mach_bits softfloat_ui64tof32(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_i32tof64(mach_bits rm, mach_bits v);
+mach_bits softfloat_ui32tof64(mach_bits rm, mach_bits v);
+mach_bits softfloat_i64tof64(mach_bits rm, mach_bits v);
+mach_bits softfloat_ui64tof64(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_f16tof32(mach_bits rm, mach_bits v);
+mach_bits softfloat_f16tof64(mach_bits rm, mach_bits v);
+mach_bits softfloat_f32tof64(mach_bits rm, mach_bits v);
+
+mach_bits softfloat_f32tof16(mach_bits rm, mach_bits v);
+mach_bits softfloat_f64tof16(mach_bits rm, mach_bits v);
+mach_bits softfloat_f64tof32(mach_bits rm, mach_bits v);
+
+bool softfloat_f16lt(mach_bits v1, mach_bits v2);
+bool softfloat_f16lt_quiet(mach_bits v1, mach_bits v2);
+bool softfloat_f16le(mach_bits v1, mach_bits v2);
+bool softfloat_f16le_quiet(mach_bits v1, mach_bits v2);
+bool softfloat_f16eq(mach_bits v1, mach_bits v2);
+bool softfloat_f32lt(mach_bits v1, mach_bits v2);
+bool softfloat_f32lt_quiet(mach_bits v1, mach_bits v2);
+bool softfloat_f32le(mach_bits v1, mach_bits v2);
+bool softfloat_f32le_quiet(mach_bits v1, mach_bits v2);
+bool softfloat_f32eq(mach_bits v1, mach_bits v2);
+bool softfloat_f64lt(mach_bits v1, mach_bits v2);
+bool softfloat_f64lt_quiet(mach_bits v1, mach_bits v2);
+bool softfloat_f64le(mach_bits v1, mach_bits v2);
+bool softfloat_f64le_quiet(mach_bits v1, mach_bits v2);
+bool softfloat_f64eq(mach_bits v1, mach_bits v2);
+
+mach_bits softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact);
+mach_bits softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact);
+mach_bits softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact);
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 3e5e7e054..6fbc67af5 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -99,488 +99,489 @@ type bits_WU     = bits(32)   /* Unsigned integer */
 type bits_L      = bits(64)   /* Signed integer */
 type bits_LU     = bits(64)   /* Unsigned integer */
 
-/* ***************************************************************** */
-/* Internal registers to pass results across the softfloat interface
- * to avoid return types involving structures.
- */
-register float_result : bits(64)
-register float_fflags : bits(64)
+/* ******************************************************************* */
+/* Get the floating point flags set by the most recent floating point  */
+/* operation. This is called after each operation to avoid having to   */
+/* use a return type involving structures.                             */
+
+val extern_float_flags = {c: "softfloat_float_flags", ocaml: "Softfloat.float_flags", lem: "softfloat_float_flags"} : (unit) -> bits_LU
 
 /* **************************************************************** */
 /* ADD/SUB/MUL/DIV                                                  */
 
-val     extern_f16Add = {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Add = {c: "softfloat_f16add", ocaml: "Softfloat.f16_add", lem: "softfloat_f16_add"} : (bits_rm, bits_H, bits_H) -> bits_H
 val      riscv_f16Add : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Add (rm, v1, v2) = {
-  extern_f16Add(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16Add(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Sub = {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Sub = {c: "softfloat_f16sub", ocaml: "Softfloat.f16_sub", lem: "softfloat_f16_sub"} : (bits_rm, bits_H, bits_H) -> bits_H
 val      riscv_f16Sub : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Sub (rm, v1, v2) = {
-  extern_f16Sub(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16Sub(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Mul = {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Mul = {c: "softfloat_f16mul", ocaml: "Softfloat.f16_mul", lem: "softfloat_f16_mul"} : (bits_rm, bits_H, bits_H) -> bits_H
 val      riscv_f16Mul : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Mul (rm, v1, v2) = {
-  extern_f16Mul(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16Mul(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Div = {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> unit
+val     extern_f16Div = {c: "softfloat_f16div", ocaml: "Softfloat.f16_div", lem: "softfloat_f16_div"} : (bits_rm, bits_H, bits_H) -> bits_H
 val      riscv_f16Div : (bits_rm, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Div (rm, v1, v2) = {
-  extern_f16Div(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16Div(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Add = {c: "softfloat_f32add", ocaml: "Softfloat.f32_add", lem: "softfloat_f32_add"} : (bits_rm, bits_S, bits_S) -> bits_S
 val      riscv_f32Add : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Add (rm, v1, v2) = {
-  extern_f32Add(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32Add(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Sub = {c: "softfloat_f32sub", ocaml: "Softfloat.f32_sub", lem: "softfloat_f32_sub"} : (bits_rm, bits_S, bits_S) -> bits_S
 val      riscv_f32Sub : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Sub (rm, v1, v2) = {
-  extern_f32Sub(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32Sub(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Mul = {c: "softfloat_f32mul", ocaml: "Softfloat.f32_mul", lem: "softfloat_f32_mul"} : (bits_rm, bits_S, bits_S) -> bits_S
 val      riscv_f32Mul : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Mul (rm, v1, v2) = {
-  extern_f32Mul(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32Mul(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> unit
+val     extern_f32Div = {c: "softfloat_f32div", ocaml: "Softfloat.f32_div", lem: "softfloat_f32_div"} : (bits_rm, bits_S, bits_S) -> bits_S
 val      riscv_f32Div : (bits_rm, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Div (rm, v1, v2) = {
-  extern_f32Div(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32Div(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: "softfloat_f64_add"} : (bits_rm, bits_D, bits_D) -> bits_D
 val      riscv_f64Add : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Add (rm, v1, v2) = {
-  extern_f64Add(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64Add(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Sub = {c: "softfloat_f64sub", ocaml: "Softfloat.f64_sub", lem: "softfloat_f64_sub"} : (bits_rm, bits_D, bits_D) -> bits_D
 val      riscv_f64Sub : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Sub (rm, v1, v2) = {
-  extern_f64Sub(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64Sub(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Mul = {c: "softfloat_f64mul", ocaml: "Softfloat.f64_mul", lem: "softfloat_f64_mul"} : (bits_rm, bits_D, bits_D) -> bits_D
 val      riscv_f64Mul : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Mul (rm, v1, v2) = {
-  extern_f64Mul(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64Mul(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> unit
+val     extern_f64Div = {c: "softfloat_f64div", ocaml: "Softfloat.f64_div", lem: "softfloat_f64_div"} : (bits_rm, bits_D, bits_D) -> bits_D
 val      riscv_f64Div : (bits_rm, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Div (rm, v1, v2) = {
-  extern_f64Div(rm, v1, v2);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64Div(rm, v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
 /* **************************************************************** */
 /* MULTIPLY-ADD                                                     */
 
-val     extern_f16MulAdd = {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> unit
+val     extern_f16MulAdd = {c: "softfloat_f16muladd", ocaml: "Softfloat.f16_muladd", lem: "softfloat_f16_muladd"} : (bits_rm, bits_H, bits_H, bits_H) -> bits_H
 val      riscv_f16MulAdd : (bits_rm, bits_H, bits_H, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16MulAdd (rm, v1, v2, v3) = {
-  extern_f16MulAdd(rm, v1, v2, v3);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16MulAdd(rm, v1, v2, v3);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> unit
+val     extern_f32MulAdd = {c: "softfloat_f32muladd", ocaml: "Softfloat.f32_muladd", lem: "softfloat_f32_muladd"} : (bits_rm, bits_S, bits_S, bits_S) -> bits_S
 val      riscv_f32MulAdd : (bits_rm, bits_S, bits_S, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32MulAdd (rm, v1, v2, v3) = {
-  extern_f32MulAdd(rm, v1, v2, v3);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32MulAdd(rm, v1, v2, v3);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> unit
+val     extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_muladd", lem: "softfloat_f64_muladd"} : (bits_rm, bits_D, bits_D, bits_D) -> bits_D
 val      riscv_f64MulAdd : (bits_rm, bits_D, bits_D, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64MulAdd (rm, v1, v2, v3) = {
-  extern_f64MulAdd(rm, v1, v2, v3);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64MulAdd(rm, v1, v2, v3);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
 /* **************************************************************** */
 /* SQUARE ROOT                                                      */
 
-val     extern_f16Sqrt = {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> unit
+val     extern_f16Sqrt = {c: "softfloat_f16sqrt", ocaml: "Softfloat.f16_sqrt", lem: "softfloat_f16_sqrt"} : (bits_rm, bits_H) -> bits_H
 val      riscv_f16Sqrt : (bits_rm, bits_H) -> (bits_fflags, bits_H)
 function riscv_f16Sqrt (rm, v) = {
-  extern_f16Sqrt(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16Sqrt(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> unit
+val     extern_f32Sqrt = {c: "softfloat_f32sqrt", ocaml: "Softfloat.f32_sqrt", lem: "softfloat_f32_sqrt"} : (bits_rm, bits_S) -> bits_S
 val      riscv_f32Sqrt : (bits_rm, bits_S) -> (bits_fflags, bits_S)
 function riscv_f32Sqrt (rm, v) = {
-  extern_f32Sqrt(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32Sqrt(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> unit
+val     extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", lem: "softfloat_f64_sqrt"} : (bits_rm, bits_D) -> bits_D
 val      riscv_f64Sqrt : (bits_rm, bits_D) -> (bits_fflags, bits_D)
 function riscv_f64Sqrt (rm, v) = {
-  extern_f64Sqrt(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64Sqrt(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
 /* **************************************************************** */
 /* CONVERSIONS                                                      */
 
-val     extern_f16ToI32 = {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToI32 = {c: "softfloat_f16toi32", ocaml: "Softfloat.f16_to_i32", lem: "softfloat_f16_to_i32"} : (bits_rm, bits_H) -> bits_W
 val      riscv_f16ToI32 : (bits_rm, bits_H) -> (bits_fflags, bits_W)
 function riscv_f16ToI32 (rm, v) = {
-  extern_f16ToI32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f16ToI32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16ToUi32 = {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToUi32 = {c: "softfloat_f16toui32", ocaml: "Softfloat.f16_to_ui32", lem: "softfloat_f16_to_ui32"} : (bits_rm, bits_H) -> bits_WU
 val      riscv_f16ToUi32 : (bits_rm, bits_H) -> (bits_fflags, bits_WU)
 function riscv_f16ToUi32 (rm, v) = {
-  extern_f16ToUi32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f16ToUi32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_i32ToF16 = {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> unit
+val     extern_i32ToF16 = {c: "softfloat_i32tof16", ocaml: "Softfloat.i32_to_f16", lem: "softfloat_i32_to_f16"} : (bits_rm, bits_W) -> bits_H
 val      riscv_i32ToF16 : (bits_rm, bits_W) -> (bits_fflags, bits_H)
 function riscv_i32ToF16 (rm, v) = {
-  extern_i32ToF16(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_i32ToF16(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_ui32ToF16 = {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> unit
+val     extern_ui32ToF16 = {c: "softfloat_ui32tof16", ocaml: "Softfloat.ui32_to_f16", lem: "softfloat_ui32_to_f16"} : (bits_rm, bits_WU) -> bits_H
 val      riscv_ui32ToF16 : (bits_rm, bits_WU) -> (bits_fflags, bits_H)
 function riscv_ui32ToF16 (rm, v) = {
-  extern_ui32ToF16(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_ui32ToF16(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64", lem: "softfloat_f16_to_i64"} : (bits_rm, bits_H) -> bits_L
 val      riscv_f16ToI64 : (bits_rm, bits_H) -> (bits_fflags, bits_L)
 function riscv_f16ToI64 (rm, v) = {
-  extern_f16ToI64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f16ToI64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16ToUi64 = {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToUi64 = {c: "softfloat_f16toui64", ocaml: "Softfloat.f16_to_ui64", lem: "softfloat_f16_to_ui64"} : (bits_rm, bits_H) -> bits_LU
 val      riscv_f16ToUi64 : (bits_rm, bits_H) -> (bits_fflags, bits_LU)
 function riscv_f16ToUi64 (rm, v) = {
-  extern_f16ToUi64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f16ToUi64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_i64ToF16 = {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> unit
+val     extern_i64ToF16 = {c: "softfloat_i64tof16", ocaml: "Softfloat.i64_to_f16", lem: "softfloat_i64_to_f16"} : (bits_rm, bits_L) -> bits_H
 val      riscv_i64ToF16 : (bits_rm, bits_L) -> (bits_fflags, bits_H)
 function riscv_i64ToF16 (rm, v) = {
-  extern_i64ToF16(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_i64ToF16(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_ui64ToF16 = {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> unit
+val     extern_ui64ToF16 = {c: "softfloat_ui64tof16", ocaml: "Softfloat.ui64_to_f16", lem: "softfloat_ui64_to_f16"} : (bits_rm, bits_L) -> bits_H
 val      riscv_ui64ToF16 : (bits_rm, bits_LU) -> (bits_fflags, bits_H)
 function riscv_ui64ToF16 (rm, v) = {
-  extern_ui64ToF16(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_ui64ToF16(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-
-val     extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> bits_W
 val      riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W)
 function riscv_f32ToI32 (rm, v) = {
-  extern_f32ToI32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32ToI32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToUi32 = {c: "softfloat_f32toui32", ocaml: "Softfloat.f32_to_ui32", lem: "softfloat_f32_to_ui32"} : (bits_rm, bits_S) -> bits_WU
 val      riscv_f32ToUi32 : (bits_rm, bits_S) -> (bits_fflags, bits_WU)
 function riscv_f32ToUi32 (rm, v) = {
-  extern_f32ToUi32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32ToUi32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> unit
+val     extern_i32ToF32 = {c: "softfloat_i32tof32", ocaml: "Softfloat.i32_to_f32", lem: "softfloat_i32_to_f32"} : (bits_rm, bits_W) -> bits_S
 val      riscv_i32ToF32 : (bits_rm, bits_W) -> (bits_fflags, bits_S)
 function riscv_i32ToF32 (rm, v) = {
-  extern_i32ToF32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_i32ToF32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> unit
+val     extern_ui32ToF32 = {c: "softfloat_ui32tof32", ocaml: "Softfloat.ui32_to_f32", lem: "softfloat_ui32_to_f32"} : (bits_rm, bits_WU) -> bits_S
 val      riscv_ui32ToF32 : (bits_rm, bits_WU) -> (bits_fflags, bits_S)
 function riscv_ui32ToF32 (rm, v) = {
-  extern_ui32ToF32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_ui32ToF32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64", lem: "softfloat_f32_to_i64"} : (bits_rm, bits_S) -> bits_L
 val      riscv_f32ToI64 : (bits_rm, bits_S) -> (bits_fflags, bits_L)
 function riscv_f32ToI64 (rm, v) = {
-  extern_f32ToI64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f32ToI64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToUi64 = {c: "softfloat_f32toui64", ocaml: "Softfloat.f32_to_ui64", lem: "softfloat_f32_to_ui64"} : (bits_rm, bits_S) -> bits_LU
 val      riscv_f32ToUi64 : (bits_rm, bits_S) -> (bits_fflags, bits_LU)
 function riscv_f32ToUi64 (rm, v) = {
-  extern_f32ToUi64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f32ToUi64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> unit
+val     extern_i64ToF32 = {c: "softfloat_i64tof32", ocaml: "Softfloat.i64_to_f32", lem: "softfloat_i64_to_f32"} : (bits_rm, bits_L) -> bits_S
 val      riscv_i64ToF32 : (bits_rm, bits_L) -> (bits_fflags, bits_S)
 function riscv_i64ToF32 (rm, v) = {
-  extern_i64ToF32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_i64ToF32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> unit
+val     extern_ui64ToF32 = {c: "softfloat_ui64tof32", ocaml: "Softfloat.ui64_to_f32", lem: "softfloat_ui64_to_f32"} : (bits_rm, bits_L) -> bits_S
 val      riscv_ui64ToF32 : (bits_rm, bits_LU) -> (bits_fflags, bits_S)
 function riscv_ui64ToF32 (rm, v) = {
-  extern_ui64ToF32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_ui64ToF32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToI32 = {c: "softfloat_f64toi32", ocaml: "Softfloat.f64_to_i32", lem: "softfloat_f64_to_i32"} : (bits_rm, bits_D) -> bits_W
 val      riscv_f64ToI32 : (bits_rm, bits_D) -> (bits_fflags, bits_W)
 function riscv_f64ToI32 (rm, v) = {
-  extern_f64ToI32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f64ToI32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToUi32 = {c: "softfloat_f64toui32", ocaml: "Softfloat.f64_to_ui32", lem: "softfloat_f64_to_ui32"} : (bits_rm, bits_D) -> bits_WU
 val      riscv_f64ToUi32 : (bits_rm, bits_D) -> (bits_fflags, bits_WU)
 function riscv_f64ToUi32 (rm, v) = {
-  extern_f64ToUi32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f64ToUi32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> unit
+val     extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64", lem: "softfloat_i32_to_f64"} : (bits_rm, bits_W) -> bits_D
 val      riscv_i32ToF64 : (bits_rm, bits_W) -> (bits_fflags, bits_D)
 function riscv_i32ToF64 (rm, v) = {
-  extern_i32ToF64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_i32ToF64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> unit
+val     extern_ui32ToF64 = {c: "softfloat_ui32tof64", ocaml: "Softfloat.ui32_to_f64", lem: "softfloat_ui32_to_f64"} : (bits_rm, bits_WU) -> bits_D
 val      riscv_ui32ToF64 : (bits_rm, bits_WU) -> (bits_fflags, bits_D)
 function riscv_ui32ToF64 (rm, v) = {
-  extern_ui32ToF64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_ui32ToF64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToI64 = {c: "softfloat_f64toi64", ocaml: "Softfloat.f64_to_i64", lem: "softfloat_f64_to_i64"} : (bits_rm, bits_D) -> bits_L
 val      riscv_f64ToI64 : (bits_rm, bits_D) -> (bits_fflags, bits_L)
 function riscv_f64ToI64 (rm, v) = {
-  extern_f64ToI64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64ToI64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToUi64 = {c: "softfloat_f64toui64", ocaml: "Softfloat.f64_to_ui64", lem: "softfloat_f64_to_ui64"} : (bits_rm, bits_D) -> bits_LU
 val      riscv_f64ToUi64 : (bits_rm, bits_D) -> (bits_fflags, bits_LU)
 function riscv_f64ToUi64 (rm, v) = {
-  extern_f64ToUi64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64ToUi64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> unit
+val     extern_i64ToF64 = {c: "softfloat_i64tof64", ocaml: "Softfloat.i64_to_f64", lem: "softfloat_i64_to_f64"} : (bits_rm, bits_L) -> bits_D
 val      riscv_i64ToF64 : (bits_rm, bits_L) -> (bits_fflags, bits_D)
 function riscv_i64ToF64 (rm, v) = {
-  extern_i64ToF64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_i64ToF64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> unit
+val     extern_ui64ToF64 = {c: "softfloat_ui64tof64", ocaml: "Softfloat.ui64_to_f64", lem: "softfloat_ui64_to_f64"} : (bits_rm, bits_LU) -> bits_D
 val      riscv_ui64ToF64 : (bits_rm, bits_LU) -> (bits_fflags, bits_D)
 function riscv_ui64ToF64 (rm, v) = {
-  extern_ui64ToF64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_ui64ToF64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> bits_S
 val      riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S)
 function riscv_f16ToF32 (rm, v) = {
-  extern_f16ToF32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f16ToF32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> unit
+val     extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64", lem: "softfloat_f16_to_f64"} : (bits_rm, bits_H) -> bits_D
 val      riscv_f16ToF64 : (bits_rm, bits_H) -> (bits_fflags, bits_D)
 function riscv_f16ToF64 (rm, v) = {
-  extern_f16ToF64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f16ToF64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> bits_D
 val      riscv_f32ToF64 : (bits_rm, bits_S) -> (bits_fflags, bits_D)
 function riscv_f32ToF64 (rm, v) = {
-  extern_f32ToF64(rm, v);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f32ToF64(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit
+val     extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> bits_H
 val      riscv_f32ToF16 : (bits_rm, bits_S) -> (bits_fflags, bits_H)
 function riscv_f32ToF16 (rm, v) = {
-  extern_f32ToF16(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f32ToF16(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> bits_H
 val      riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H)
 function riscv_f64ToF16 (rm, v) = {
-  extern_f64ToF16(rm, v);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f64ToF16(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> unit
+val     extern_f64ToF32 = {c: "softfloat_f64tof32", ocaml: "Softfloat.f64_to_f32", lem: "softfloat_f64_to_f32"} : (bits_rm, bits_D) -> bits_S
 val      riscv_f64ToF32 : (bits_rm, bits_D) -> (bits_fflags, bits_S)
 function riscv_f64ToF32 (rm, v) = {
-  extern_f64ToF32(rm, v);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f64ToF32(rm, v);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
 /* **************************************************************** */
 /* COMPARISONS                                                      */
 
-val     extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> unit
+val     extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "softfloat_f16_lt"} : (bits_H, bits_H) -> bool
 val      riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Lt (v1, v2) = {
-  extern_f16Lt(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f16Lt(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit
+val     extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> bool
 val      riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Lt_quiet (v1, v2) = {
-  extern_f16Lt_quiet(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f16Lt_quiet(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit
+val     extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> bool
 val      riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Le (v1, v2) = {
-  extern_f16Le(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f16Le(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit
+val     extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> bool
 val      riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Le_quiet (v1, v2) = {
-  extern_f16Le_quiet(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f16Le_quiet(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit
+val     extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> bool
 val      riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool)
 function riscv_f16Eq (v1, v2) = {
-  extern_f16Eq(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f16Eq(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit
+val     extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> bool
 val      riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Lt (v1, v2) = {
-  extern_f32Lt(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f32Lt(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit
+val     extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> bool
 val      riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Lt_quiet (v1, v2) = {
-  extern_f32Lt_quiet(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f32Lt_quiet(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit
+val     extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> bool
 val      riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Le (v1, v2) = {
-  extern_f32Le(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f32Le(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit
+val     extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> bool
 val      riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Le_quiet (v1, v2) = {
-  extern_f32Le_quiet(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f32Le_quiet(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit
+val     extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> bool
 val      riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool)
 function riscv_f32Eq (v1, v2) = {
-  extern_f32Eq(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f32Eq(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit
+val     extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> bool
 val      riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Lt (v1, v2) = {
-  extern_f64Lt(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f64Lt(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit
+val     extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> bool
 val      riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Lt_quiet (v1, v2) = {
-  extern_f64Lt_quiet(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f64Lt_quiet(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit
+
+val     extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> bool
 val      riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Le (v1, v2) = {
-  extern_f64Le(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f64Le(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit
+val     extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> bool
 val      riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Le_quiet (v1, v2) = {
-  extern_f64Le_quiet(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f64Le_quiet(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit
+val     extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> bool
 val      riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool)
 function riscv_f64Eq (v1, v2) = {
-  extern_f64Eq(v1, v2);
-  (float_fflags[4 .. 0], bit_to_bool(float_result[0]))
+  let float_result = extern_f64Eq(v1, v2);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit
+val     extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> bits_H
 val      riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H)
 function riscv_f16roundToInt (rm, v, exact) = {
-  extern_f16roundToInt(rm, v, exact);
-  (float_fflags[4 .. 0], float_result[15 .. 0])
+  let float_result = extern_f16roundToInt(rm, v, exact);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit
+val     extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> bits_S
 val      riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S)
 function riscv_f32roundToInt (rm, v, exact) = {
-  extern_f32roundToInt(rm, v, exact);
-  (float_fflags[4 .. 0], float_result[31 .. 0])
+  let float_result = extern_f32roundToInt(rm, v, exact);
+  (extern_float_flags()[4 .. 0], float_result)
 }
 
-val     extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit
+val     extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> bits_D
 val      riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D)
 function riscv_f64roundToInt (rm, v, exact) = {
-  extern_f64roundToInt(rm, v, exact);
-  (float_fflags[4 .. 0], float_result)
+  let float_result = extern_f64roundToInt(rm, v, exact);
+  (extern_float_flags()[4 .. 0], float_result)
 }
+
 /* **************************************************************** */