diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c
index bdf20e20b..2ba5e176f 100644
--- a/c_emulator/riscv_softfloat.c
+++ b/c_emulator/riscv_softfloat.c
@@ -67,7 +67,7 @@ mach_bits softfloat_f16div(mach_bits rm, mach_bits v1, mach_bits v2)
   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);
 
@@ -76,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);
 
@@ -90,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);
 
@@ -104,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);
 
@@ -118,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);
 
@@ -132,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);
 
@@ -146,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);
 
@@ -160,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);
 
@@ -174,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);
 
@@ -189,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);
 
@@ -204,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);
 
@@ -219,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);
 
@@ -232,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);
 
@@ -245,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);
 
@@ -258,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);
 
@@ -276,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);
 
@@ -291,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);
 
@@ -306,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);
 
@@ -321,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);
 
@@ -335,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);
 
@@ -349,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);
 
@@ -364,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);
 
@@ -379,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);
 
@@ -394,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);
 
@@ -409,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);
 
@@ -423,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);
 
@@ -437,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);
 
@@ -595,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);
 
@@ -609,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);
 
@@ -623,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);
 
@@ -637,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);
 
@@ -651,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);
 
@@ -665,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);
 
@@ -679,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);
 
@@ -693,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);
 
@@ -707,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);
 
@@ -721,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);
 
@@ -735,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);
 
@@ -749,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);
 
@@ -763,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);
 
@@ -777,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);
 
@@ -791,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);
 
@@ -805,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);
 
@@ -819,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);
 
@@ -833,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);
 
@@ -847,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);
 
@@ -861,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);
 
@@ -875,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);
 
@@ -889,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);
 
@@ -903,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);
 
@@ -917,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 09639b79a..2ef0d1ed9 100644
--- a/c_emulator/riscv_softfloat.h
+++ b/c_emulator/riscv_softfloat.h
@@ -7,81 +7,81 @@ 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);
 
-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_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_insts_dext.sail b/model/riscv_insts_dext.sail
index 5afde5c97..573549ab3 100644
--- a/model/riscv_insts_dext.sail
+++ b/model/riscv_insts_dext.sail
@@ -349,7 +349,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = {
           FNMSUB_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, rs3_val_64b),
           FNMADD_D => riscv_f64MulAdd (rm_3b, negate_D (rs1_val_64b), rs2_val_64b, negate_D (rs3_val_64b))
         };
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_64b;
       RETIRE_SUCCESS
     }
@@ -413,7 +413,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = {
         FMUL_D  => riscv_f64Mul (rm_3b, rs1_val_64b, rs2_val_64b),
         FDIV_D  => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b)
       };
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_64b;
       RETIRE_SUCCESS
     }
@@ -501,7 +501,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_f64Sqrt   (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -516,7 +516,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_W) = riscv_f64ToI32 (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend (rd_val_W);
       RETIRE_SUCCESS
     }
@@ -531,7 +531,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_WU) = riscv_f64ToUi32 (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend (rd_val_WU);
       RETIRE_SUCCESS
     }
@@ -546,7 +546,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -561,7 +561,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -576,7 +576,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -591,7 +591,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -607,7 +607,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_L) = riscv_f64ToI64 (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend(rd_val_L);
       RETIRE_SUCCESS
     }
@@ -623,7 +623,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend(rd_val_LU);
       RETIRE_SUCCESS
     }
@@ -639,7 +639,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -655,7 +655,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -862,7 +862,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Eq (rs1_val_D, rs2_val_D);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -874,7 +874,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Lt (rs1_val_D, rs2_val_D);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -886,7 +886,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Le (rs1_val_D, rs2_val_D);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index e60b96b5d..172081d1b 100644
--- a/model/riscv_insts_fext.sail
+++ b/model/riscv_insts_fext.sail
@@ -526,7 +526,7 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = {
           FNMSUB_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, rs3_val_32b),
           FNMADD_S => riscv_f32MulAdd (rm_3b, negate_S (rs1_val_32b), rs2_val_32b, negate_S (rs3_val_32b))
         };
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_32b;
       RETIRE_SUCCESS
     }
@@ -590,7 +590,7 @@ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = {
         FMUL_S  => riscv_f32Mul (rm_3b, rs1_val_32b, rs2_val_32b),
         FDIV_S  => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b)
       };
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_32b;
       RETIRE_SUCCESS
     }
@@ -670,7 +670,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_f32Sqrt   (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -685,7 +685,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_W) = riscv_f32ToI32 (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend (rd_val_W);
       RETIRE_SUCCESS
     }
@@ -700,7 +700,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_WU) = riscv_f32ToUi32 (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend (rd_val_WU);
       RETIRE_SUCCESS
     }
@@ -715,7 +715,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -730,7 +730,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -746,7 +746,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_L) = riscv_f32ToI64 (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend(rd_val_L);
       RETIRE_SUCCESS
     }
@@ -762,7 +762,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_LU) = riscv_f32ToUi64 (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend(rd_val_LU);
       RETIRE_SUCCESS
     }
@@ -778,7 +778,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -794,7 +794,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -986,7 +986,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Eq (rs1_val_S, rs2_val_S);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -998,7 +998,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Lt (rs1_val_S, rs2_val_S);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -1010,7 +1010,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Le (rs1_val_S, rs2_val_S);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail
index cad5b1cde..634636a49 100644
--- a/model/riscv_insts_zfa.sail
+++ b/model/riscv_insts_zfa.sail
@@ -416,7 +416,7 @@ function clause execute (RISCV_FROUND_H(rs1, rm, rd)) = {
       let rm_3b =  encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, false);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -444,7 +444,7 @@ function clause execute (RISCV_FROUNDNX_H(rs1, rm, rd)) = {
       let rm_3b =  encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, true);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -472,7 +472,7 @@ function clause execute (RISCV_FROUND_S(rs1, rm, rd)) = {
       let rm_3b =  encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, false);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -500,7 +500,7 @@ function clause execute (RISCV_FROUNDNX_S(rs1, rm, rd)) = {
       let rm_3b =  encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, true);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -528,7 +528,7 @@ function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = {
       let rm_3b =  encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, false);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -556,7 +556,7 @@ function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = {
       let rm_3b =  encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, true);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -627,7 +627,7 @@ function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Le_quiet   (rs1_val_H, rs2_val_H);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -651,7 +651,7 @@ function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Lt_quiet   (rs1_val_H, rs2_val_H);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -675,7 +675,7 @@ function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Le_quiet   (rs1_val_S, rs2_val_S);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -699,7 +699,7 @@ function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f32Lt_quiet   (rs1_val_S, rs2_val_S);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -724,7 +724,7 @@ function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Le_quiet   (rs1_val_D, rs2_val_D);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -748,7 +748,7 @@ function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f64Lt_quiet   (rs1_val_D, rs2_val_D);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -828,7 +828,7 @@ mapping clause assembly = RISCV_FCVTMOD_W_D(rs1, rd)
 function clause execute(RISCV_FCVTMOD_W_D(rs1, rd)) = {
   let rs1_val_D = F_D(rs1);
   let (fflags, rd_val) = fcvtmod_helper(rs1_val_D);
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = sign_extend(rd_val);
   RETIRE_SUCCESS
 }
diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail
index b071c8b2a..3cc8bec21 100644
--- a/model/riscv_insts_zfh.sail
+++ b/model/riscv_insts_zfh.sail
@@ -338,7 +338,7 @@ function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = {
           FNMSUB_H => riscv_f16MulAdd (rm_3b, negate_H (rs1_val_16b), rs2_val_16b, rs3_val_16b),
           FNMADD_H => riscv_f16MulAdd (rm_3b, negate_H (rs1_val_16b), rs2_val_16b, negate_H (rs3_val_16b))
         };
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_16b;
       RETIRE_SUCCESS
     }
@@ -477,7 +477,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Eq (rs1_val_H, rs2_val_H);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -489,7 +489,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Lt (rs1_val_H, rs2_val_H);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -501,7 +501,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)) = {
   let (fflags, rd_val) : (bits_fflags, bool) =
       riscv_f16Le (rs1_val_H, rs2_val_H);
 
-  write_fflags(fflags);
+  accrue_fflags(fflags);
   X(rd) = zero_extend(bool_to_bits(rd_val));
   RETIRE_SUCCESS
 }
@@ -643,7 +643,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_f16Sqrt   (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -658,7 +658,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_W) = riscv_f16ToI32 (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend (rd_val_W);
       RETIRE_SUCCESS
     }
@@ -673,7 +673,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_WU) = riscv_f16ToUi32 (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend (rd_val_WU);
       RETIRE_SUCCESS
     }
@@ -688,7 +688,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_i32ToF16 (rm_3b, rs1_val_W);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -703,7 +703,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_ui32ToF16 (rm_3b, rs1_val_WU);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -718,7 +718,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_f32ToF16 (rm_3b, rs1_val_S);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -733,7 +733,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_f64ToF16 (rm_3b, rs1_val_D);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -748,7 +748,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_S) = riscv_f16ToF32 (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_S(rd) = rd_val_S;
       RETIRE_SUCCESS
     }
@@ -764,7 +764,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_D) = riscv_f16ToF64 (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_D(rd) = rd_val_D;
       RETIRE_SUCCESS
     }
@@ -780,7 +780,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_L) = riscv_f16ToI64 (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend(rd_val_L);
       RETIRE_SUCCESS
     }
@@ -796,7 +796,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_LU) = riscv_f16ToUi64 (rm_3b, rs1_val_H);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       X(rd) = sign_extend(rd_val_LU);
       RETIRE_SUCCESS
     }
@@ -812,7 +812,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_i64ToF16 (rm_3b, rs1_val_L);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
@@ -828,7 +828,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)) = {
       let rm_3b = encdec_rounding_mode(rm');
       let (fflags, rd_val_H) = riscv_ui64ToF16 (rm_3b, rs1_val_LU);
 
-      write_fflags(fflags);
+      accrue_fflags(fflags);
       F_or_X_H(rd) = rd_val_H;
       RETIRE_SUCCESS
     }
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 339769bf0..ae42688e5 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/model/riscv_softfloat_interface.sail
@@ -137,449 +137,451 @@ function riscv_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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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) effect {rreg}
 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)
 }
+
 /* **************************************************************** */