From da346ccc2581158da96a79ea7cd406bc32b2beb6 Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Thu, 18 Apr 2024 00:06:47 -0700 Subject: [PATCH] Use two 64 bit values for f128 Softfloat interface --- c_emulator/riscv_sail.h | 3 +- c_emulator/riscv_softfloat.c | 186 ++++++++------------- c_emulator/riscv_softfloat.h | 51 +++--- handwritten_support/riscv_extras_fdext.lem | 38 ++--- model/riscv_softfloat_interface.sail | 153 +++++++++-------- ocaml_emulator/softfloat.ml | 38 ++--- 6 files changed, 223 insertions(+), 246 deletions(-) diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index ef328912d..804a3e0fb 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -64,8 +64,7 @@ extern mach_bits zmstatus; extern mach_bits zmepc, zmtval; extern mach_bits zsepc, zstval; -extern mach_bits zfloat_fflags; -extern sail_bits zfloat_result; +extern mach_bits zfloat_fflags, zfloat_result, zfloat_result_high; struct zMcause { mach_bits zMcause_chunk_0; diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c index 1caff12bf..46edb3627 100644 --- a/c_emulator/riscv_softfloat.c +++ b/c_emulator/riscv_softfloat.c @@ -3,7 +3,6 @@ #include "riscv_sail.h" #include "riscv_softfloat.h" #include "softfloat.h" -#include "gmp.h" static uint_fast8_t uint8_of_rm(mach_bits rm) { @@ -11,74 +10,26 @@ static uint_fast8_t uint8_of_rm(mach_bits rm) return (uint_fast8_t)rm; } -#define SOFTFLOAT_PRELUDE(rm) \ - softfloat_exceptionFlags = 0; \ - softfloat_roundingMode = (uint_fast8_t)rm - -#define SOFTFLOAT_POSTLUDE(res) \ - recreate_lbits_of_fbits(&zfloat_result, res.v, 128ull, true); \ - zfloat_fflags = (mach_bits)softfloat_exceptionFlags - -static float128_t to_float128(sail_bits v1) +static float128_t to_float128(mach_bits low, mach_bits high) { - static mpz_t tmp; - static bool isInitialized = false; - float128_t res; - uint32_t lo; - uint32_t hi; - mpz_t *from = v1.bits; - - // I don't know if you mind a small memory leak or not - // malloc not being released - if (!isInitialized) { - mpz_init(tmp); - isInitialized = true; - } - - mpz_mod_2exp(tmp, *from, 64); // lower 64 bits of v1 - lo = mpz_get_ui(tmp); - mpz_div_2exp(tmp, tmp, 32); - hi = mpz_get_ui(tmp); - - res.v[0] = (((uint64_t)hi) << 32) + lo; - - mpz_div_2exp(tmp, *from, 64); // higher 64 bits of v1 - lo = mpz_get_ui(tmp); - mpz_div_2exp(tmp, tmp, 32); - hi = mpz_get_ui(tmp); - - res.v[1] = (((uint64_t)hi) << 32) + lo; - + res.v[0] = low; + res.v[1] = high; return res; } -#define SOFTFLOAT_POSTLUDE_128 softfloat_postlude_128 - -static void softfloat_postlude_128(float128_t res) -{ - static sail_int _64; - static mpz_t lo; - static bool isInitialized = false; - - // I don't know if you mind a small memory leak or not - if (!isInitialized) { - create_sail_int_of_mach_int(&_64, 64ull); - mpz_init(lo); - } - - // set upper 64 bits - recreate_lbits_of_fbits(&zfloat_result, res.v[1], 128ull, true); - shiftl(&zfloat_result, zfloat_result, _64); +#define SOFTFLOAT_PRELUDE(rm) \ + softfloat_exceptionFlags = 0; \ + softfloat_roundingMode = (uint_fast8_t)rm - // set lower 64 bits - mpz_set_ui(lo, (uint32_t)(res.v[0] >> 32)); - mpz_mul_2exp(lo, lo, 32); - mpz_add_ui(lo, lo, (uint32_t)res.v[0]); - add_bits_int(&zfloat_result, zfloat_result, lo); +#define SOFTFLOAT_POSTLUDE(res) \ + zfloat_result = res.v; \ + zfloat_fflags = (mach_bits)softfloat_exceptionFlags - zfloat_fflags = (mach_bits)softfloat_exceptionFlags; -} +#define SOFTFLOAT_POSTLUDE_128(res) \ + zfloat_result = res.v[0]; \ + zfloat_result_high = res.v[1]; \ + zfloat_fflags = (mach_bits)softfloat_exceptionFlags unit softfloat_f16add(mach_bits rm, mach_bits v1, mach_bits v2) { @@ -248,13 +199,14 @@ unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2) return UNIT; } -unit softfloat_f128add(mach_bits rm, sail_bits v1, sail_bits v2) +unit softfloat_f128add(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high) { SOFTFLOAT_PRELUDE(rm); float128_t a, b, res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res = f128_add(a, b); SOFTFLOAT_POSTLUDE_128(res); @@ -262,13 +214,14 @@ unit softfloat_f128add(mach_bits rm, sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128sub(mach_bits rm, sail_bits v1, sail_bits v2) +unit softfloat_f128sub(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high) { SOFTFLOAT_PRELUDE(rm); float128_t a, b, res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res = f128_sub(a, b); SOFTFLOAT_POSTLUDE_128(res); @@ -276,13 +229,14 @@ unit softfloat_f128sub(mach_bits rm, sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128div(mach_bits rm, sail_bits v1, sail_bits v2) +unit softfloat_f128div(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high) { SOFTFLOAT_PRELUDE(rm); float128_t a, b, res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res = f128_div(a, b); SOFTFLOAT_POSTLUDE_128(res); @@ -290,13 +244,14 @@ unit softfloat_f128div(mach_bits rm, sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128mul(mach_bits rm, sail_bits v1, sail_bits v2) +unit softfloat_f128mul(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high) { SOFTFLOAT_PRELUDE(rm); float128_t a, b, res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res = f128_mul(a, b); SOFTFLOAT_POSTLUDE_128(res); @@ -349,15 +304,16 @@ unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3) return UNIT; } -unit softfloat_f128muladd(mach_bits rm, sail_bits v1, sail_bits v2, - sail_bits v3) +unit softfloat_f128muladd(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high, mach_bits v3_low, + mach_bits v3_high) { SOFTFLOAT_PRELUDE(rm); float128_t a, b, c, res; - a = to_float128(v1); - b = to_float128(v2); - c = to_float128(v3); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); + c = to_float128(v3_low, v3_high); res = f128_mulAdd(a, b, c); SOFTFLOAT_POSTLUDE_128(res); @@ -404,12 +360,12 @@ unit softfloat_f64sqrt(mach_bits rm, mach_bits v) return UNIT; } -unit softfloat_f128sqrt(mach_bits rm, sail_bits v) +unit softfloat_f128sqrt(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); float128_t a, res; - a = to_float128(v); + a = to_float128(v_low, v_high); res = f128_sqrt(a); SOFTFLOAT_POSTLUDE_128(res); @@ -596,7 +552,7 @@ unit softfloat_f64toui64(mach_bits rm, mach_bits v) return UNIT; } -unit softfloat_f128toi32(mach_bits rm, sail_bits v) +unit softfloat_f128toi32(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); @@ -604,7 +560,7 @@ unit softfloat_f128toi32(mach_bits rm, sail_bits v) float32_t res; uint_fast8_t rm8 = uint8_of_rm(rm); - a = to_float128(v); + a = to_float128(v_low, v_high); res.v = f128_to_i32(a, rm8, true); SOFTFLOAT_POSTLUDE(res); @@ -612,7 +568,7 @@ unit softfloat_f128toi32(mach_bits rm, sail_bits v) return UNIT; } -unit softfloat_f128toui32(mach_bits rm, sail_bits v) +unit softfloat_f128toui32(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); @@ -620,7 +576,7 @@ unit softfloat_f128toui32(mach_bits rm, sail_bits v) float32_t res; uint_fast8_t rm8 = uint8_of_rm(rm); - a = to_float128(v); + a = to_float128(v_low, v_high); res.v = f128_to_ui32(a, rm8, true); SOFTFLOAT_POSTLUDE(res); @@ -628,7 +584,7 @@ unit softfloat_f128toui32(mach_bits rm, sail_bits v) return UNIT; } -unit softfloat_f128toi64(mach_bits rm, sail_bits v) +unit softfloat_f128toi64(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); @@ -636,7 +592,7 @@ unit softfloat_f128toi64(mach_bits rm, sail_bits v) float64_t res; uint_fast8_t rm8 = uint8_of_rm(rm); - a = to_float128(v); + a = to_float128(v_low, v_high); res.v = f128_to_i64(a, rm8, true); SOFTFLOAT_POSTLUDE(res); @@ -644,7 +600,7 @@ unit softfloat_f128toi64(mach_bits rm, sail_bits v) return UNIT; } -unit softfloat_f128toui64(mach_bits rm, sail_bits v) +unit softfloat_f128toui64(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); @@ -652,7 +608,7 @@ unit softfloat_f128toui64(mach_bits rm, sail_bits v) float64_t res; uint_fast8_t rm8 = uint8_of_rm(rm); - a = to_float128(v); + a = to_float128(v_low, v_high); res.v = f128_to_ui64(a, rm8, true); SOFTFLOAT_POSTLUDE(res); @@ -993,14 +949,14 @@ unit softfloat_f64tof128(mach_bits rm, mach_bits v) return UNIT; } -unit softfloat_f128tof16(mach_bits rm, sail_bits v) +unit softfloat_f128tof16(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); float128_t a; float16_t res; - a = to_float128(v); + a = to_float128(v_low, v_high); res = f128_to_f16(a); SOFTFLOAT_POSTLUDE(res); @@ -1008,14 +964,14 @@ unit softfloat_f128tof16(mach_bits rm, sail_bits v) return UNIT; } -unit softfloat_f128tof32(mach_bits rm, sail_bits v) +unit softfloat_f128tof32(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); float128_t a; float32_t res; - a = to_float128(v); + a = to_float128(v_low, v_high); res = f128_to_f32(a); SOFTFLOAT_POSTLUDE(res); @@ -1023,14 +979,14 @@ unit softfloat_f128tof32(mach_bits rm, sail_bits v) return UNIT; } -unit softfloat_f128tof64(mach_bits rm, sail_bits v) +unit softfloat_f128tof64(mach_bits rm, mach_bits v_low, mach_bits v_high) { SOFTFLOAT_PRELUDE(rm); float128_t a; float64_t res; - a = to_float128(v); + a = to_float128(v_low, v_high); res = f128_to_f64(a); SOFTFLOAT_POSTLUDE(res); @@ -1248,14 +1204,15 @@ unit softfloat_f64eq(mach_bits v1, mach_bits v2) return UNIT; } -unit softfloat_f128lt(sail_bits v1, sail_bits v2) +unit softfloat_f128lt(mach_bits v1_low, mach_bits v1_high, mach_bits v2_low, + mach_bits v2_high) { SOFTFLOAT_PRELUDE(0); float128_t a, b; float64_t res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res.v = f128_lt(a, b); SOFTFLOAT_POSTLUDE(res); @@ -1263,14 +1220,15 @@ unit softfloat_f128lt(sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128lt_quiet(sail_bits v1, sail_bits v2) +unit softfloat_f128lt_quiet(mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high) { SOFTFLOAT_PRELUDE(0); float128_t a, b; float64_t res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res.v = f128_lt_quiet(a, b); SOFTFLOAT_POSTLUDE(res); @@ -1278,14 +1236,15 @@ unit softfloat_f128lt_quiet(sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128le(sail_bits v1, sail_bits v2) +unit softfloat_f128le(mach_bits v1_low, mach_bits v1_high, mach_bits v2_low, + mach_bits v2_high) { SOFTFLOAT_PRELUDE(0); float128_t a, b; float64_t res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res.v = f128_le(a, b); SOFTFLOAT_POSTLUDE(res); @@ -1293,14 +1252,15 @@ unit softfloat_f128le(sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128le_quiet(sail_bits v1, sail_bits v2) +unit softfloat_f128le_quiet(mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high) { SOFTFLOAT_PRELUDE(0); float128_t a, b; float64_t res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res.v = f128_le_quiet(a, b); SOFTFLOAT_POSTLUDE(res); @@ -1308,14 +1268,15 @@ unit softfloat_f128le_quiet(sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128eq(sail_bits v1, sail_bits v2) +unit softfloat_f128eq(mach_bits v1_low, mach_bits v1_high, mach_bits v2_low, + mach_bits v2_high) { SOFTFLOAT_PRELUDE(0); float128_t a, b; float64_t res; - a = to_float128(v1); - b = to_float128(v2); + a = to_float128(v1_low, v1_high); + b = to_float128(v2_low, v2_high); res.v = f128_eq(a, b); SOFTFLOAT_POSTLUDE(res); @@ -1365,13 +1326,14 @@ unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact) return UNIT; } -unit softfloat_f128roundToInt(mach_bits rm, sail_bits v, bool exact) +unit softfloat_f128roundToInt(mach_bits rm, mach_bits v_low, mach_bits v_high, + bool exact) { SOFTFLOAT_PRELUDE(rm); float128_t a, res; uint_fast8_t rm8 = uint8_of_rm(rm); - a = to_float128(v); + a = to_float128(v_low, v_high); res = f128_roundToInt(a, rm8, exact); SOFTFLOAT_POSTLUDE_128(res); diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h index dc74fd054..3b3f9220e 100644 --- a/c_emulator/riscv_softfloat.h +++ b/c_emulator/riscv_softfloat.h @@ -15,10 +15,14 @@ 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_f128add(mach_bits rm, sail_bits v1, sail_bits v2); -unit softfloat_f128sub(mach_bits rm, sail_bits v1, sail_bits v2); -unit softfloat_f128mul(mach_bits rm, sail_bits v1, sail_bits v2); -unit softfloat_f128div(mach_bits rm, sail_bits v1, sail_bits v2); +unit softfloat_f128add(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high); +unit softfloat_f128sub(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high); +unit softfloat_f128mul(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high); +unit softfloat_f128div(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high); unit softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3); @@ -26,13 +30,14 @@ 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_f128muladd(mach_bits rm, sail_bits v1, sail_bits v2, - sail_bits v3); +unit softfloat_f128muladd(mach_bits rm, mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high, mach_bits v3_low, + mach_bits v3_high); 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_f128sqrt(mach_bits rm, sail_bits v); +unit softfloat_f128sqrt(mach_bits rm, mach_bits v_low, mach_bits v_high); unit softfloat_f16toi32(mach_bits rm, mach_bits v); unit softfloat_f16toui32(mach_bits rm, mach_bits v); @@ -49,10 +54,10 @@ 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_f128toi32(mach_bits rm, sail_bits v); -unit softfloat_f128toui32(mach_bits rm, sail_bits v); -unit softfloat_f128toi64(mach_bits rm, sail_bits v); -unit softfloat_f128toui64(mach_bits rm, sail_bits v); +unit softfloat_f128toi32(mach_bits rm, mach_bits v_low, mach_bits v_high); +unit softfloat_f128toui32(mach_bits rm, mach_bits v_low, mach_bits v_high); +unit softfloat_f128toi64(mach_bits rm, mach_bits v_low, mach_bits v_high); +unit softfloat_f128toui64(mach_bits rm, mach_bits v_low, mach_bits v_high); unit softfloat_i32tof16(mach_bits rm, mach_bits v); unit softfloat_ui32tof16(mach_bits rm, mach_bits v); @@ -84,9 +89,9 @@ unit softfloat_f64tof128(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_f128tof16(mach_bits rm, sail_bits v); -unit softfloat_f128tof32(mach_bits rm, sail_bits v); -unit softfloat_f128tof64(mach_bits rm, sail_bits v); +unit softfloat_f128tof16(mach_bits rm, mach_bits v_low, mach_bits v_high); +unit softfloat_f128tof32(mach_bits rm, mach_bits v_low, mach_bits v_high); +unit softfloat_f128tof64(mach_bits rm, mach_bits v_low, mach_bits v_high); unit softfloat_f16lt(mach_bits v1, mach_bits v2); unit softfloat_f16lt_quiet(mach_bits v1, mach_bits v2); @@ -103,13 +108,19 @@ 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_f128lt(sail_bits v1, sail_bits v2); -unit softfloat_f128lt_quiet(sail_bits v1, sail_bits v2); -unit softfloat_f128le(sail_bits v1, sail_bits v2); -unit softfloat_f128le_quiet(sail_bits v1, sail_bits v2); -unit softfloat_f128eq(sail_bits v1, sail_bits v2); +unit softfloat_f128lt(mach_bits v1_low, mach_bits v1_high, mach_bits v2_low, + mach_bits v2_high); +unit softfloat_f128lt_quiet(mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high); +unit softfloat_f128le(mach_bits v1_low, mach_bits v1_high, mach_bits v2_low, + mach_bits v2_high); +unit softfloat_f128le_quiet(mach_bits v1_low, mach_bits v1_high, + mach_bits v2_low, mach_bits v2_high); +unit softfloat_f128eq(mach_bits v1_low, mach_bits v1_high, mach_bits v2_low, + mach_bits v2_high); 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); -unit softfloat_f128roundToInt(mach_bits rm, sail_bits v, bool exact); +unit softfloat_f128roundToInt(mach_bits rm, mach_bits v_low, mach_bits v_high, + bool exact); diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem index 21b45928c..3ddadf4da 100644 --- a/handwritten_support/riscv_extras_fdext.lem +++ b/handwritten_support/riscv_extras_fdext.lem @@ -89,7 +89,7 @@ let softfloat_f32_round_to_int _ _ _ = () val softfloat_f64_round_to_int : bitvector -> bitvector -> bool -> unit let softfloat_f64_round_to_int _ _ _ = () -val softfloat_f128_round_to_int : bitvector -> bitvector -> bool -> unit +val softfloat_f128_round_to_int : bitvector -> bitvector -> bitvector -> bool -> unit let softfloat_f128_round_to_int _ _ _ = () val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit @@ -128,16 +128,16 @@ let softfloat_f64_mul _ _ _ = () val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_div _ _ _ = () -val softfloat_f128_add : bitvector -> bitvector -> bitvector -> unit +val softfloat_f128_add : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f128_add _ _ _ = () -val softfloat_f128_sub : bitvector -> bitvector -> bitvector -> unit +val softfloat_f128_sub : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f128_sub _ _ _ = () -val softfloat_f128_mul : bitvector -> bitvector -> bitvector -> unit +val softfloat_f128_mul : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f128_mul _ _ _ = () -val softfloat_f128_div : bitvector -> bitvector -> bitvector -> unit +val softfloat_f128_div : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f128_div _ _ _ = () @@ -150,7 +150,7 @@ let softfloat_f32_muladd _ _ _ _ = () val softfloat_f64_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f64_muladd _ _ _ _ = () -val softfloat_f128_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit +val softfloat_f128_muladd : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f128_muladd _ _ _ _ = () @@ -163,7 +163,7 @@ let softfloat_f32_sqrt _ _ = () val softfloat_f64_sqrt : bitvector -> bitvector -> unit let softfloat_f64_sqrt _ _ = () -val softfloat_f128_sqrt : bitvector -> bitvector -> unit +val softfloat_f128_sqrt : bitvector -> bitvector -> bitvector -> unit let softfloat_f128_sqrt _ _ = () @@ -241,10 +241,10 @@ let softfloat_i64_to_f64 _ _ = () val softfloat_ui64_to_f64: bitvector -> bitvector -> unit let softfloat_ui64_to_f64 _ _ = () -val softfloat_f128_to_i32: bitvector -> bitvector -> unit +val softfloat_f128_to_i32: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_i32 _ _ = () -val softfloat_f128_to_ui32: bitvector -> bitvector -> unit +val softfloat_f128_to_ui32: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_ui32 _ _ = () val softfloat_i32_to_f128: bitvector -> bitvector -> unit @@ -253,10 +253,10 @@ let softfloat_i32_to_f128 _ _ = () val softfloat_ui32_to_f128: bitvector -> bitvector -> unit let softfloat_ui32_to_f128 _ _ = () -val softfloat_f128_to_i64: bitvector -> bitvector -> unit +val softfloat_f128_to_i64: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_i64 _ _ = () -val softfloat_f128_to_ui64: bitvector -> bitvector -> unit +val softfloat_f128_to_ui64: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_ui64 _ _ = () val softfloat_i64_to_f128: bitvector -> bitvector -> unit @@ -293,13 +293,13 @@ let softfloat_f64_to_f32 _ _ = () val softfloat_f64_to_f128: bitvector -> bitvector -> unit let softfloat_f64_to_f128 _ _ = () -val softfloat_f128_to_f16: bitvector -> bitvector -> unit +val softfloat_f128_to_f16: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_f16 _ _ = () -val softfloat_f128_to_f32: bitvector -> bitvector -> unit +val softfloat_f128_to_f32: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_f32 _ _ = () -val softfloat_f128_to_f64: bitvector -> bitvector -> unit +val softfloat_f128_to_f64: bitvector -> bitvector -> bitvector -> unit let softfloat_f128_to_f64 _ _ = () @@ -348,17 +348,17 @@ let softfloat_f64_le_quiet _ _ = () val softfloat_f64_eq : bitvector -> bitvector -> unit let softfloat_f64_eq _ _ = () -val softfloat_f128_lt : bitvector -> bitvector -> unit +val softfloat_f128_lt : bitvector -> bitvector -> bitvector -> unit let softfloat_f128_lt _ _ = () -val softfloat_f128_lt_quiet : bitvector -> bitvector -> unit +val softfloat_f128_lt_quiet : bitvector -> bitvector -> bitvector -> unit let softfloat_f128_lt_quiet _ _ = () -val softfloat_f128_le : bitvector -> bitvector -> unit +val softfloat_f128_le : bitvector -> bitvector -> bitvector -> unit let softfloat_f128_le _ _ = () -val softfloat_f128_le_quiet : bitvector -> bitvector -> unit +val softfloat_f128_le_quiet : bitvector -> bitvector -> bitvector -> unit let softfloat_f128_le_quiet _ _ = () -val softfloat_f128_eq : bitvector -> bitvector -> unit +val softfloat_f128_eq : bitvector -> bitvector -> bitvector -> unit let softfloat_f128_eq _ _ = () diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 0a6dedfec..b325d67fd 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -31,6 +31,8 @@ type bits_H = bits(16) /* Half-precision float value */ type bits_S = bits(32) /* Single-precision float value */ type bits_D = bits(64) /* Double-precision float value */ type bits_Q = bits(128) /* Quad-precision float value */ +type bits_Q_low = bits(64) /* Quad-precision float low bits */ +type bits_Q_high = bits(64) /* Quad-precision float high bits */ type bits_W = bits(32) /* Signed integer */ type bits_WU = bits(32) /* Unsigned integer */ @@ -42,7 +44,8 @@ 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(128) +register float_result : bits(64) +register float_result_high : bits(64) register float_fflags : bits(64) /* **************************************************************** */ @@ -108,57 +111,57 @@ val extern_f64Add = {c: "softfloat_f64add", ocaml: "Softfloat.f64_add", lem: 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[4 .. 0], float_result) } -val extern_f128Add = {c: "softfloat_f128add", ocaml: "Softfloat.f128_add", lem: "softfloat_f128_add"} : (bits_rm, bits_Q, bits_Q) -> unit +val extern_f128Add = {c: "softfloat_f128add", ocaml: "Softfloat.f128_add", lem: "softfloat_f128_add"} : (bits_rm, bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Add : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q) function riscv_f128Add (rm, v1, v2) = { - extern_f128Add(rm, v1, v2); - (float_fflags[4 .. 0], float_result[127..0]) + extern_f128Add(rm, v1[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) } -val extern_f128Sub = {c: "softfloat_f128sub", ocaml: "Softfloat.f128_sub", lem: "softfloat_f128_sub"} : (bits_rm, bits_Q, bits_Q) -> unit +val extern_f128Sub = {c: "softfloat_f128sub", ocaml: "Softfloat.f128_sub", lem: "softfloat_f128_sub"} : (bits_rm, bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Sub : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q) function riscv_f128Sub (rm, v1, v2) = { - extern_f128Sub(rm, v1, v2); - (float_fflags[4 .. 0], float_result[127..0]) + extern_f128Sub(rm, v1[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) } -val extern_f128Mul = {c: "softfloat_f128mul", ocaml: "Softfloat.f128_mul", lem: "softfloat_f128_mul"} : (bits_rm, bits_Q, bits_Q) -> unit +val extern_f128Mul = {c: "softfloat_f128mul", ocaml: "Softfloat.f128_mul", lem: "softfloat_f128_mul"} : (bits_rm, bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Mul : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q) function riscv_f128Mul (rm, v1, v2) = { - extern_f128Mul(rm, v1, v2); - (float_fflags[4 .. 0], float_result[127..0]) + extern_f128Mul(rm, v1[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) } -val extern_f128Div = {c: "softfloat_f128div", ocaml: "Softfloat.f128_div", lem: "softfloat_f128_div"} : (bits_rm, bits_Q, bits_Q) -> unit +val extern_f128Div = {c: "softfloat_f128div", ocaml: "Softfloat.f128_div", lem: "softfloat_f128_div"} : (bits_rm, bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Div : (bits_rm, bits_Q, bits_Q) -> (bits_fflags, bits_Q) function riscv_f128Div (rm, v1, v2) = { - extern_f128Div(rm, v1, v2); - (float_fflags[4 .. 0], float_result[127..0]) + extern_f128Div(rm, v1[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) } /* **************************************************************** */ /* MULTIPLY-ADD */ @@ -181,14 +184,15 @@ val extern_f64MulAdd = {c: "softfloat_f64muladd", ocaml: "Softfloat.f64_mula 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[63..0]) + (float_fflags[4 .. 0], float_result) } -val extern_f128MulAdd = {c: "softfloat_f128muladd", ocaml: "Softfloat.f128_muladd", lem: "softfloat_f128_muladd"} : (bits_rm, bits_Q, bits_Q, bits_Q) -> unit +val extern_f128MulAdd = {c: "softfloat_f128muladd", ocaml: "Softfloat.f128_muladd", lem: "softfloat_f128_muladd"} : (bits_rm, bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128MulAdd : (bits_rm, bits_Q, bits_Q, bits_Q) -> (bits_fflags, bits_Q) function riscv_f128MulAdd (rm, v1, v2, v3) = { - extern_f128MulAdd(rm, v1, v2, v3); - (float_fflags[4 .. 0], float_result[127..0]) + extern_f128MulAdd(rm, v1[63..0], v1[127..64], v2[63..0], v2[127..64], v3[63..0], v3[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) + } @@ -213,14 +217,15 @@ val extern_f64Sqrt = {c: "softfloat_f64sqrt", ocaml: "Softfloat.f64_sqrt", l 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[63..0]) + (float_fflags[4 .. 0], float_result) } -val extern_f128Sqrt = {c: "softfloat_f128sqrt", ocaml: "Softfloat.f128_sqrt", lem: "softfloat_f128_sqrt"} : (bits_rm, bits_Q) -> unit +val extern_f128Sqrt = {c: "softfloat_f128sqrt", ocaml: "Softfloat.f128_sqrt", lem: "softfloat_f128_sqrt"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128Sqrt : (bits_rm, bits_Q) -> (bits_fflags, bits_Q) function riscv_f128Sqrt (rm, v) = { - extern_f128Sqrt(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + extern_f128Sqrt(rm, v[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) + } /* **************************************************************** */ @@ -258,14 +263,14 @@ val extern_f16ToI64 = {c: "softfloat_f16toi64", ocaml: "Softfloat.f16_to_i64 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 @@ -314,14 +319,14 @@ val extern_f32ToI64 = {c: "softfloat_f32toi64", ocaml: "Softfloat.f32_to_i64 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 @@ -356,55 +361,55 @@ val extern_i32ToF64 = {c: "softfloat_i32tof64", ocaml: "Softfloat.i32_to_f64 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[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 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[63..0]) + (float_fflags[4 .. 0], float_result) } -val extern_f128ToI32 = {c: "softfloat_f128toi32", ocaml: "Softfloat.f128_to_i32", lem: "softfloat_f128_to_i32"} : (bits_rm, bits_Q) -> unit +val extern_f128ToI32 = {c: "softfloat_f128toi32", ocaml: "Softfloat.f128_to_i32", lem: "softfloat_f128_to_i32"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToI32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W) function riscv_f128ToI32 (rm, v) = { - extern_f128ToI32(rm, v); + extern_f128ToI32(rm, v[63..0], v[127..64]); (float_fflags[4 .. 0], float_result[31..0]) } -val extern_f128ToUi32 = {c: "softfloat_f128toui32", ocaml: "Softfloat.f128_to_ui32", lem: "softfloat_f128_to_ui32"} : (bits_rm, bits_Q) -> unit +val extern_f128ToUi32 = {c: "softfloat_f128toui32", ocaml: "Softfloat.f128_to_ui32", lem: "softfloat_f128_to_ui32"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToUi32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W) function riscv_f128ToUi32 (rm, v) = { - extern_f128ToUi32(rm, v); + extern_f128ToUi32(rm, v[63..0], v[127..64]); (float_fflags[4 .. 0], float_result[31..0]) } @@ -412,42 +417,42 @@ val extern_i32ToF128 = {c: "softfloat_i32tof128", ocaml: "Softfloat.i32_to_f val riscv_i32ToF128 : (bits_rm, bits_W) -> (bits_fflags, bits_Q) function riscv_i32ToF128 (rm, v) = { extern_i32ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } val extern_ui32ToF128 = {c: "softfloat_ui32tof128", ocaml: "Softfloat.ui32_to_f128", lem: "softfloat_ui32_to_f128"} : (bits_rm, bits_W) -> unit val riscv_ui32ToF128 : (bits_rm, bits_W) -> (bits_fflags, bits_Q) function riscv_ui32ToF128 (rm, v) = { extern_ui32ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } -val extern_f128ToI64 = {c: "softfloat_f128toi64", ocaml: "Softfloat.f128_to_i64", lem: "softfloat_f128_to_i64"} : (bits_rm, bits_Q) -> unit +val extern_f128ToI64 = {c: "softfloat_f128toi64", ocaml: "Softfloat.f128_to_i64", lem: "softfloat_f128_to_i64"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToI64 : (bits_rm, bits_Q) -> (bits_fflags, bits_L) function riscv_f128ToI64 (rm, v) = { - extern_f128ToI64(rm, v); - (float_fflags[4 .. 0], float_result[63..0]) + extern_f128ToI64(rm, v[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result) } -val extern_f128ToUi64 = {c: "softfloat_f128toui64", ocaml: "Softfloat.f128_to_ui64", lem: "softfloat_f128_to_ui64"} : (bits_rm, bits_Q) -> unit +val extern_f128ToUi64 = {c: "softfloat_f128toui64", ocaml: "Softfloat.f128_to_ui64", lem: "softfloat_f128_to_ui64"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToUi64 : (bits_rm, bits_Q) -> (bits_fflags, bits_LU) function riscv_f128ToUi64 (rm, v) = { - extern_f128ToUi64(rm, v); - (float_fflags[4 .. 0], float_result[63..0]) + extern_f128ToUi64(rm, v[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result) } val extern_i64ToF128 = {c: "softfloat_i64tof128", ocaml: "Softfloat.i64_to_f128", lem: "softfloat_i64_to_f128"} : (bits_rm, bits_L) -> unit val riscv_i64ToF128 : (bits_rm, bits_L) -> (bits_fflags, bits_Q) function riscv_i64ToF128 (rm, v) = { extern_i64ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } val extern_ui64ToF128 = {c: "softfloat_ui64tof128", ocaml: "Softfloat.ui64_to_f128", lem: "softfloat_ui64_to_f128"} : (bits_rm, bits_LU) -> unit val riscv_ui64ToF128 : (bits_rm, bits_LU) -> (bits_fflags, bits_Q) function riscv_ui64ToF128 (rm, v) = { extern_ui64ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } val extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit @@ -461,14 +466,14 @@ val extern_f16ToF64 = {c: "softfloat_f16tof64", ocaml: "Softfloat.f16_to_f64 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[63..0]) + (float_fflags[4 .. 0], float_result) } val extern_f16ToF128 = {c: "softfloat_f16tof128", ocaml: "Softfloat.f16_to_f128", lem: "softfloat_f16_to_f128"} : (bits_rm, bits_H) -> unit val riscv_f16ToF128 : (bits_rm, bits_H) -> (bits_fflags, bits_Q) function riscv_f16ToF128 (rm, v) = { extern_f16ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } val extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit @@ -482,14 +487,14 @@ val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64 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[63..0]) + (float_fflags[4 .. 0], float_result) } val extern_f32ToF128 = {c: "softfloat_f32tof128", ocaml: "Softfloat.f32_to_f128", lem: "softfloat_f32_to_f128"} : (bits_rm, bits_S) -> unit val riscv_f32ToF128 : (bits_rm, bits_S) -> (bits_fflags, bits_Q) function riscv_f32ToF128 (rm, v) = { extern_f32ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } val extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit @@ -510,28 +515,28 @@ val extern_f64ToF128 = {c: "softfloat_f64tof128", ocaml: "Softfloat.f64_to_f val riscv_f64ToF128 : (bits_rm, bits_D) -> (bits_fflags, bits_Q) function riscv_f64ToF128 (rm, v) = { extern_f64ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) + (float_fflags[4 .. 0], float_result_high @ float_result) } -val extern_f128ToF16 = {c: "softfloat_f128tof16", ocaml: "Softfloat.f128_to_f16", lem: "softfloat_f128_to_f16"} : (bits_rm, bits_Q) -> unit +val extern_f128ToF16 = {c: "softfloat_f128tof16", ocaml: "Softfloat.f128_to_f16", lem: "softfloat_f128_to_f16"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToF16 : (bits_rm, bits_Q) -> (bits_fflags, bits_H) function riscv_f128ToF16 (rm, v) = { - extern_f128ToF16(rm, v); + extern_f128ToF16(rm, v[63..0], v[127..64]); (float_fflags[4 .. 0], float_result[15..0]) } -val extern_f128ToF32 = {c: "softfloat_f128tof32", ocaml: "Softfloat.f128_to_f32", lem: "softfloat_f128_to_f32"} : (bits_rm, bits_Q) -> unit +val extern_f128ToF32 = {c: "softfloat_f128tof32", ocaml: "Softfloat.f128_to_f32", lem: "softfloat_f128_to_f32"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToF32 : (bits_rm, bits_Q) -> (bits_fflags, bits_S) function riscv_f128ToF32 (rm, v) = { - extern_f128ToF32(rm, v); + extern_f128ToF32(rm, v[63..0], v[127..64]); (float_fflags[4 .. 0], float_result[31..0]) } -val extern_f128ToF64 = {c: "softfloat_f128tof64", ocaml: "Softfloat.f128_to_f64", lem: "softfloat_f128_to_f64"} : (bits_rm, bits_Q) -> unit +val extern_f128ToF64 = {c: "softfloat_f128tof64", ocaml: "Softfloat.f128_to_f64", lem: "softfloat_f128_to_f64"} : (bits_rm, bits_Q_low, bits_Q_high) -> unit val riscv_f128ToF64 : (bits_rm, bits_Q) -> (bits_fflags, bits_D) function riscv_f128ToF64 (rm, v) = { - extern_f128ToF64(rm, v); - (float_fflags[4 .. 0], float_result[63..0]) + extern_f128ToF64(rm, v[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result) } /* **************************************************************** */ @@ -642,38 +647,38 @@ function riscv_f64Eq (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f128Lt = {c: "softfloat_f128lt", ocaml: "Softfloat.f128_lt", lem: "softfloat_f128_lt"} : (bits_Q, bits_Q) -> unit +val extern_f128Lt = {c: "softfloat_f128lt", ocaml: "Softfloat.f128_lt", lem: "softfloat_f128_lt"} : (bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Lt : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Lt (v1, v2) = { - extern_f128Lt(v1, v2); + extern_f128Lt(v1[63..0], v1[127..64], v2[63..0], v2[127..64]); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f128Lt_quiet = {c: "softfloat_f128lt_quiet", ocaml: "Softfloat.f128_lt_quiet", lem: "softfloat_f128_lt_quiet"} : (bits_Q, bits_Q) -> unit +val extern_f128Lt_quiet = {c: "softfloat_f128lt_quiet", ocaml: "Softfloat.f128_lt_quiet", lem: "softfloat_f128_lt_quiet"} : (bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Lt_quiet : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Lt_quiet (v1, v2) = { - extern_f128Lt_quiet(v1, v2); + extern_f128Lt_quiet(v1[63..0], v1[127..64], v2[63..0], v2[127..64]); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f128Le = {c: "softfloat_f128le", ocaml: "Softfloat.f128_le", lem: "softfloat_f128_le"} : (bits_Q, bits_Q) -> unit +val extern_f128Le = {c: "softfloat_f128le", ocaml: "Softfloat.f128_le", lem: "softfloat_f128_le"} : (bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Le : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Le (v1, v2) = { - extern_f128Le(v1, v2); + extern_f128Le(v1[63..0], v1[127..64], v2[63..0], v2[127..64]); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f128Le_quiet = {c: "softfloat_f128le_quiet", ocaml: "Softfloat.f128_le_quiet", lem: "softfloat_f128_le_quiet"} : (bits_Q, bits_Q) -> unit +val extern_f128Le_quiet = {c: "softfloat_f128le_quiet", ocaml: "Softfloat.f128_le_quiet", lem: "softfloat_f128_le_quiet"} : (bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Le_quiet : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Le_quiet (v1, v2) = { - extern_f128Le_quiet(v1, v2); + extern_f128Le_quiet(v1[63..0], v1[127..64], v2[63..0], v2[127..64]); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } -val extern_f128Eq = {c: "softfloat_f128eq", ocaml: "Softfloat.f128_eq", lem: "softfloat_f128_eq"} : (bits_Q, bits_Q) -> unit +val extern_f128Eq = {c: "softfloat_f128eq", ocaml: "Softfloat.f128_eq", lem: "softfloat_f128_eq"} : (bits_Q_low, bits_Q_high, bits_Q_low, bits_Q_high) -> unit val riscv_f128Eq : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Eq (v1, v2) = { - extern_f128Eq(v1, v2); + extern_f128Eq(v1[63..0], v1[127..64], v2[63..0], v2[127..64]); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } @@ -698,11 +703,11 @@ function riscv_f64roundToInt (rm, v, exact) = { (float_fflags[4 .. 0], float_result[63 .. 0]) } -val extern_f128roundToInt = {c: "softfloat_f128roundToInt", ocaml: "Softfloat.f128_round_to_int", lem: "softfloat_f128_round_to_int"} : (bits_rm, bits_Q, bool) -> unit +val extern_f128roundToInt = {c: "softfloat_f128roundToInt", ocaml: "Softfloat.f128_round_to_int", lem: "softfloat_f128_round_to_int"} : (bits_rm, bits_Q_low, bits_Q_high, bool) -> unit val riscv_f128roundToInt : (bits_rm, bits_Q, bool) -> (bits_fflags, bits_Q) function riscv_f128roundToInt (rm, v, exact) = { - extern_f128roundToInt(rm, v, exact); - (float_fflags[4 .. 0], float_result[127 .. 0]) + extern_f128roundToInt(rm, v[63..0], v[127..64], exact); + (float_fflags[4 .. 0], float_result_high @ float_result) } /* **************************************************************** */ diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml index 0afa32174..b065fb291 100644 --- a/ocaml_emulator/softfloat.ml +++ b/ocaml_emulator/softfloat.ml @@ -35,16 +35,16 @@ let f64_mul rm v1 v2 = let f64_div rm v1 v2 = () -let f128_add rm v1 v2 = +let f128_add rm v1_low v1_high v2_low v2_high = () -let f128_sub rm v1 v2 = +let f128_sub rm v1_low v1_high v2_low v2_high = () -let f128_mul rm v1 v2 = +let f128_mul rm v1_low v1_high v2_low v2_high = () -let f128_div rm v1 v2 = +let f128_div rm v1_low v1_high v2_low v2_high = () let f16_muladd rm v1 v2 v3 = @@ -56,7 +56,7 @@ let f32_muladd rm v1 v2 v3 = let f64_muladd rm v1 v2 v3 = () -let f128_muladd rm v1 v2 v3 = +let f128_muladd rm v1_low v1_high v2_low v2_high v3_low v3_high = () @@ -69,7 +69,7 @@ let f32_sqrt rm v = let f64_sqrt rm v = () -let f128_sqrt rm v = +let f128_sqrt rm v_low v_high = () let f16_to_i32 rm v = @@ -144,10 +144,10 @@ let i64_to_f64 rm v = let ui64_to_f64 rm v = () -let f128_to_i32 rm v = +let f128_to_i32 rm v_low v_high = () -let f128_to_ui32 rm v = +let f128_to_ui32 rm v_low v_high = () let i32_to_f128 rm v = @@ -156,10 +156,10 @@ let i32_to_f128 rm v = let ui32_to_f128 rm v = () -let f128_to_i64 rm v = +let f128_to_i64 rm v_low v_high = () -let f128_to_ui64 rm v = +let f128_to_ui64 rm v_low v_high = () let i64_to_f128 rm v = @@ -195,13 +195,13 @@ let f64_to_f32 rm v = let f64_to_f128 rm v = () -let f128_to_f16 rm v = +let f128_to_f16 rm v_low v_high = () -let f128_to_f32 rm v = +let f128_to_f32 rm v_low v_high = () -let f128_to_f64 rm v = +let f128_to_f64 rm v_low v_high = () @@ -250,19 +250,19 @@ let f64_le_quiet v1 v2 = let f64_eq v1 v2 = () -let f128_lt v1 v2 = +let f128_lt v1_low v1_high v2_low v2_high = () -let f128_lt_quiet v1 v2 = +let f128_lt_quiet v1_low v1_high v2_low v2_high = () -let f128_le v1 v2 = +let f128_le v1_low v1_high v2_low v2_high = () -let f128_le_quiet v1 v2 = +let f128_le_quiet v1_low v1_high v2_low v2_high = () -let f128_eq v1 v2 = +let f128_eq v1_low v1_high v2_low v2_high = () let f16_round_to_int exact rm v = @@ -274,5 +274,5 @@ let f32_round_to_int exact rm v = let f64_round_to_int exact rm v = () -let f128_round_to_int exact rm v = +let f128_round_to_int exact rm v_low v_high = ()