From 0e889e2c4d2d9468a8785ded67d4a918b6b7ca90 Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Mon, 8 Apr 2024 07:19:42 -0700 Subject: [PATCH] Add Zfa and Zfh support for Q --- .../SoftFloat-3e/source/include/softfloat.h | 6 +- c_emulator/riscv_softfloat.c | 431 ++++++++++-------- c_emulator/riscv_softfloat.h | 10 +- model/riscv_freg_type.sail | 2 +- model/riscv_insts_qext.sail | 8 +- model/riscv_insts_zfa.sail | 260 +++++++++++ model/riscv_insts_zfh.sail | 54 ++- model/riscv_softfloat_interface.sail | 186 ++++---- model/riscv_sys_regs.sail | 4 + ocaml_emulator/softfloat.ml | 51 ++- 10 files changed, 725 insertions(+), 287 deletions(-) diff --git a/c_emulator/SoftFloat-3e/source/include/softfloat.h b/c_emulator/SoftFloat-3e/source/include/softfloat.h index 1efd8c423..d2c4eade0 100644 --- a/c_emulator/SoftFloat-3e/source/include/softfloat.h +++ b/c_emulator/SoftFloat-3e/source/include/softfloat.h @@ -147,9 +147,9 @@ int_fast32_t f16_to_i32_r_minMag( float16_t, bool ); int_fast64_t f16_to_i64_r_minMag( float16_t, bool ); float32_t f16_to_f32( float16_t ); float64_t f16_to_f64( float16_t ); +float128_t f16_to_f128( float16_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t f16_to_extF80( float16_t ); -float128_t f16_to_f128( float16_t ); #endif void f16_to_extF80M( float16_t, extFloat80_t * ); void f16_to_f128M( float16_t, float128_t * ); @@ -309,19 +309,19 @@ bool extF80M_isSignalingNaN( const extFloat80_t * ); | 128-bit (quadruple-precision) floating-point operations. *----------------------------------------------------------------------------*/ #ifdef SOFTFLOAT_FAST_INT64 +extFloat80_t f128_to_extF80( float128_t ); +#endif uint_fast32_t f128_to_ui32_r_minMag( float128_t, bool ); uint_fast64_t f128_to_ui64_r_minMag( float128_t, bool ); int_fast32_t f128_to_i32_r_minMag( float128_t, bool ); int_fast64_t f128_to_i64_r_minMag( float128_t, bool ); float16_t f128_to_f16( float128_t ); -extFloat80_t f128_to_extF80( float128_t ); float128_t f128_roundToInt( float128_t, uint_fast8_t, bool ); float128_t f128_rem( float128_t, float128_t ); bool f128_eq_signaling( float128_t, float128_t ); bool f128_le_quiet( float128_t, float128_t ); bool f128_lt_quiet( float128_t, float128_t ); bool f128_isSignalingNaN( float128_t ); -#endif bool f128_eq( float128_t, float128_t ); bool f128_le( float128_t, float128_t ); bool f128_lt( float128_t, float128_t ); diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c index 7463c5af1..b5dd9dcb2 100644 --- a/c_emulator/riscv_softfloat.c +++ b/c_emulator/riscv_softfloat.c @@ -595,6 +595,70 @@ unit softfloat_f64toui64(mach_bits rm, mach_bits v) return UNIT; } +unit softfloat_f128toi32(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float32_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v); + res.v = f128_to_i32(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128toui32(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float32_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v); + res.v = f128_to_ui32(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128toi64(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float64_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v); + res.v = f128_to_i64(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128toui64(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float64_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v); + res.v = f128_to_ui64(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_i32tof16(mach_bits rm, mach_bits v) { SOFTFLOAT_PRELUDE(rm); @@ -739,6 +803,66 @@ unit softfloat_ui64tof64(mach_bits rm, mach_bits v) return UNIT; } +unit softfloat_i32tof128(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + int32_t a; + float128_t res; + + a = (int32_t)v; + res = i32_to_f128(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +unit softfloat_ui32tof128(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + uint32_t a; + float128_t res; + + a = (uint32_t)v; + res = ui32_to_f128(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +unit softfloat_i64tof128(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + int64_t a; + float128_t res; + + a = (int64_t)v; + res = i64_to_f128(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +unit softfloat_ui64tof128(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + uint64_t a; + float128_t res; + + a = (uint64_t)v; + res = ui64_to_f128(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + unit softfloat_f16tof32(mach_bits rm, mach_bits v) { SOFTFLOAT_PRELUDE(rm); @@ -767,6 +891,35 @@ unit softfloat_f16tof64(mach_bits rm, mach_bits v) return UNIT; } +unit softfloat_f16tof128(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float16_t a; + float128_t res; + + a.v = v; + res = f16_to_f128(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +unit softfloat_f32tof16(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float32_t a; + float16_t res; + a.v = v; + res = f32_to_f16(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f32tof64(mach_bits rm, mach_bits v) { SOFTFLOAT_PRELUDE(rm); @@ -781,16 +934,17 @@ unit softfloat_f32tof64(mach_bits rm, mach_bits v) return UNIT; } -unit softfloat_f32tof16(mach_bits rm, mach_bits v) +unit softfloat_f32tof128(mach_bits rm, mach_bits v) { SOFTFLOAT_PRELUDE(rm); float32_t a; - float16_t res; + float128_t res; + a.v = v; - res = f32_to_f16(a); + res = f32_to_f128(a); - SOFTFLOAT_POSTLUDE(res); + SOFTFLOAT_POSTLUDE_128(res); return UNIT; } @@ -823,6 +977,66 @@ unit softfloat_f64tof32(mach_bits rm, mach_bits v) return UNIT; } +unit softfloat_f64tof128(mach_bits rm, mach_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float64_t a; + float128_t res; + + a.v = v; + res = f64_to_f128(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +unit softfloat_f128tof16(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float16_t res; + + a = to_float128(v); + res = f128_to_f16(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128tof32(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float32_t res; + + a = to_float128(v); + res = f128_to_f32(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128tof64(mach_bits rm, sail_bits v) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float64_t res; + + a = to_float128(v); + res = f128_to_f64(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f16lt(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -1033,49 +1247,37 @@ unit softfloat_f64eq(mach_bits v1, mach_bits v2) return UNIT; } -unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact) -{ - SOFTFLOAT_PRELUDE(rm); - - float16_t a, res; - uint_fast8_t rm8 = uint8_of_rm(rm); - a.v = v; - res = f16_roundToInt(a, rm8, exact); - - SOFTFLOAT_POSTLUDE(res); - - return UNIT; -} - -unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact) +unit softfloat_f128lt(sail_bits v1, sail_bits v2) { - SOFTFLOAT_PRELUDE(rm); + SOFTFLOAT_PRELUDE(0); - float32_t a, res; - uint_fast8_t rm8 = uint8_of_rm(rm); - a.v = v; - res = f32_roundToInt(a, rm8, exact); + float128_t a, b; + float64_t res; + a = to_float128(v1); + b = to_float128(v2); + res.v = f128_lt(a, b); SOFTFLOAT_POSTLUDE(res); return UNIT; } -unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact) +unit softfloat_f128lt_quiet(sail_bits v1, sail_bits v2) { - SOFTFLOAT_PRELUDE(rm); + SOFTFLOAT_PRELUDE(0); - float64_t a, res; - uint_fast8_t rm8 = uint8_of_rm(rm); - a.v = v; - res = f64_roundToInt(a, rm8, exact); + float128_t a, b; + float64_t res; + a = to_float128(v1); + b = to_float128(v2); + res.v = f128_lt_quiet(a, b); SOFTFLOAT_POSTLUDE(res); return UNIT; } -unit softfloat_f128lt(sail_bits v1, sail_bits v2) +unit softfloat_f128le(sail_bits v1, sail_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -1083,13 +1285,14 @@ unit softfloat_f128lt(sail_bits v1, sail_bits v2) float64_t res; a = to_float128(v1); b = to_float128(v2); - res.v = f128_lt(a, b); + res.v = f128_le(a, b); SOFTFLOAT_POSTLUDE(res); return UNIT; } -unit softfloat_f128le(sail_bits v1, sail_bits v2) + +unit softfloat_f128le_quiet(sail_bits v1, sail_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -1097,12 +1300,13 @@ unit softfloat_f128le(sail_bits v1, sail_bits v2) float64_t res; a = to_float128(v1); b = to_float128(v2); - res.v = f128_le(a, b); + res.v = f128_le_quiet(a, b); SOFTFLOAT_POSTLUDE(res); return UNIT; } + unit softfloat_f128eq(sail_bits v1, sail_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -1118,187 +1322,58 @@ unit softfloat_f128eq(sail_bits v1, sail_bits v2) return UNIT; } -unit softfloat_f128toi32(mach_bits rm, sail_bits v) +unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact) { SOFTFLOAT_PRELUDE(rm); - float128_t a; - float32_t res; + float16_t a, res; uint_fast8_t rm8 = uint8_of_rm(rm); - - a = to_float128(v); - res.v = f128_to_i32(a, rm8, true); + a.v = v; + res = f16_roundToInt(a, rm8, exact); SOFTFLOAT_POSTLUDE(res); return UNIT; } -unit softfloat_f128toui32(mach_bits rm, sail_bits v) +unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact) { SOFTFLOAT_PRELUDE(rm); - float128_t a; - float32_t res; + float32_t a, res; uint_fast8_t rm8 = uint8_of_rm(rm); - - a = to_float128(v); - res.v = f128_to_ui32(a, rm8, true); + a.v = v; + res = f32_roundToInt(a, rm8, exact); SOFTFLOAT_POSTLUDE(res); return UNIT; } -unit softfloat_f128toi64(mach_bits rm, sail_bits v) +unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact) { SOFTFLOAT_PRELUDE(rm); - float128_t a; - float64_t res; + float64_t a, res; uint_fast8_t rm8 = uint8_of_rm(rm); - - a = to_float128(v); - res.v = f128_to_i64(a, rm8, true); + a.v = v; + res = f64_roundToInt(a, rm8, exact); SOFTFLOAT_POSTLUDE(res); return UNIT; } -unit softfloat_f128toui64(mach_bits rm, sail_bits v) +unit softfloat_f128roundToInt(mach_bits rm, sail_bits v, bool exact) { SOFTFLOAT_PRELUDE(rm); - float128_t a; - float64_t res; + float128_t a, res; uint_fast8_t rm8 = uint8_of_rm(rm); - a = to_float128(v); - res.v = f128_to_ui64(a, rm8, true); - - SOFTFLOAT_POSTLUDE(res); - - return UNIT; -} - -unit softfloat_i32tof128(mach_bits rm, mach_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - int32_t a; - float128_t res; - - a = (int32_t)v; - res = i32_to_f128(a); - - SOFTFLOAT_POSTLUDE_128(res); - - return UNIT; -} - -unit softfloat_ui32tof128(mach_bits rm, mach_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - uint32_t a; - float128_t res; - - a = (uint32_t)v; - res = ui32_to_f128(a); - - SOFTFLOAT_POSTLUDE_128(res); - - return UNIT; -} - -unit softfloat_i64tof128(mach_bits rm, mach_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - int64_t a; - float128_t res; - - a = (int64_t)v; - res = i64_to_f128(a); - - SOFTFLOAT_POSTLUDE_128(res); - - return UNIT; -} - -unit softfloat_ui64tof128(mach_bits rm, mach_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - uint64_t a; - float128_t res; - - a = (uint64_t)v; - res = ui64_to_f128(a); - - SOFTFLOAT_POSTLUDE_128(res); - - return UNIT; -} - -unit softfloat_f32tof128(mach_bits rm, sail_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - float128_t tmp; - float32_t a; - float128_t res; - - tmp = to_float128(v); - a.v = (uint32_t)tmp.v[1]; - res = f32_to_f128(a); - - SOFTFLOAT_POSTLUDE_128(res); - - return UNIT; -} -unit softfloat_f64tof128(mach_bits rm, sail_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - float128_t tmp; - float64_t a; - float128_t res; - - tmp = to_float128(v); - a.v = (uint64_t)tmp.v[1]; - res = f64_to_f128(a); + res = f128_roundToInt(a, rm8, exact); SOFTFLOAT_POSTLUDE_128(res); return UNIT; } -unit softfloat_f128tof32(mach_bits rm, sail_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - float128_t a; - float32_t res; - - a = to_float128(v); - res = f128_to_f32(a); - - SOFTFLOAT_POSTLUDE(res); - - return UNIT; -} -unit softfloat_f128tof64(mach_bits rm, sail_bits v) -{ - SOFTFLOAT_PRELUDE(rm); - - float128_t a; - float64_t res; - - a = to_float128(v); - res = f128_to_f64(a); - - SOFTFLOAT_POSTLUDE(res); - - return UNIT; -} diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h index 380cb7f0b..dc74fd054 100644 --- a/c_emulator/riscv_softfloat.h +++ b/c_emulator/riscv_softfloat.h @@ -76,14 +76,15 @@ unit softfloat_ui64tof128(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_f16tof128(mach_bits rm, mach_bits v); unit softfloat_f32tof64(mach_bits rm, mach_bits v); +unit softfloat_f32tof128(mach_bits rm, mach_bits v); +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_f32tof128(mach_bits rm, sail_bits v); -unit softfloat_f64tof128(mach_bits rm, sail_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); @@ -103,9 +104,12 @@ 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_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); diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail index c9478271f..38c92b5ab 100644 --- a/model/riscv_freg_type.sail +++ b/model/riscv_freg_type.sail @@ -38,7 +38,7 @@ enum f_madd_op_H = {FMADD_H, FMSUB_H, FNMSUB_H, FNMADD_H} enum f_bin_rm_op_H = {FADD_H, FSUB_H, FMUL_H, FDIV_H} enum f_un_rm_op_H = {FSQRT_H, FCVT_W_H, FCVT_WU_H, FCVT_H_W, FCVT_H_WU, // RV32 and RV64 - FCVT_H_S, FCVT_H_D, FCVT_S_H, FCVT_D_H, + FCVT_H_S, FCVT_H_D, FCVT_H_Q, FCVT_S_H, FCVT_D_H, FCVT_Q_H, FCVT_L_H, FCVT_LU_H, FCVT_H_L, FCVT_H_LU} // RV64 only enum f_un_op_H = {FCLASS_H, FMV_X_H, FMV_H_X} /* RV32 and RV64 */ diff --git a/model/riscv_insts_qext.sail b/model/riscv_insts_qext.sail index 124827dab..a2c8ace09 100644 --- a/model/riscv_insts_qext.sail +++ b/model/riscv_insts_qext.sail @@ -508,14 +508,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_S_Q)) = { let (fflags, rd_val_S) = riscv_f128ToF32 (rm_3b, rs1_val_Q); accrue_fflags(fflags); - F_Q(rd) = rd_val_S; + F_S(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_S)) = { - let rs1_val_S = F_Q(rs1); + let rs1_val_S = F_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -538,14 +538,14 @@ function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_D_Q)) = { let (fflags, rd_val_D) = riscv_f128ToF64 (rm_3b, rs1_val_Q); accrue_fflags(fflags); - F_Q(rd) = rd_val_D; + F_D(rd) = rd_val_D; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D)) = { - let rs1_val_D = F_Q(rs1); + let rs1_val_D = F_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 9f1e19925..7a75a4caa 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -153,6 +153,55 @@ function clause execute (RISCV_FLI_D(constantidx, rd)) = { RETIRE_SUCCESS } +/* FLI.Q */ + +union clause ast = RISCV_FLI_Q : (bits(5), regidx) + +mapping clause encdec = RISCV_FLI_Q(rs1, rd) if haveQExt() & haveZfa() + <-> 0b111_1011 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FLI_Q(constantidx, rd) + <-> "fli.q" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) + +function clause execute (RISCV_FLI_Q(constantidx, rd)) = { + let bits : bits(128) = match constantidx { + 0b00000 => { 0xbfff0000000000000000000000000000 }, /* -1.0 */ + 0b00001 => { 0x00010000000000000000000000000000 }, /* minimum positive normal */ + 0b00010 => { 0x3fef0000000000000000000000000000 }, /* 1.0 * 2^-16 */ + 0b00011 => { 0x3ff00000000000000000000000000000 }, /* 1.0 * 2^-15 */ + 0b00100 => { 0x3ff70000000000000000000000000000 }, /* 1.0 * 2^-8 */ + 0b00101 => { 0x3ff80000000000000000000000000000 }, /* 1.0 * 2^-7 */ + 0b00110 => { 0x3ffb0000000000000000000000000000 }, /* 1.0 * 2^-4 */ + 0b00111 => { 0x3ffc0000000000000000000000000000 }, /* 1.0 * 2^-3 */ + 0b01000 => { 0x3ffd0000000000000000000000000000 }, /* 0.25 */ + 0b01001 => { 0x3ffd4000000000000000000000000000 }, /* 0.3125 */ + 0b01010 => { 0x3ffd8000000000000000000000000000 }, /* 0.375 */ + 0b01011 => { 0x3ffdc000000000000000000000000000 }, /* 0.4375 */ + 0b01100 => { 0x3ffe0000000000000000000000000000 }, /* 0.5 */ + 0b01101 => { 0x3ffe4000000000000000000000000000 }, /* 0.625 */ + 0b01110 => { 0x3ffe8000000000000000000000000000 }, /* 0.75 */ + 0b01111 => { 0x3ffec000000000000000000000000000 }, /* 0.875 */ + 0b10000 => { 0x3fff0000000000000000000000000000 }, /* 1.0 */ + 0b10001 => { 0x3fff4000000000000000000000000000 }, /* 1.25 */ + 0b10010 => { 0x3fff8000000000000000000000000000 }, /* 1.5 */ + 0b10011 => { 0x3fffc000000000000000000000000000 }, /* 1.75 */ + 0b10100 => { 0x40000000000000000000000000000000 }, /* 2.0 */ + 0b10101 => { 0x40004000000000000000000000000000 }, /* 2.5 */ + 0b10110 => { 0x40008000000000000000000000000000 }, /* 3 */ + 0b10111 => { 0x40010000000000000000000000000000 }, /* 4 */ + 0b11000 => { 0x40020000000000000000000000000000 }, /* 8 */ + 0b11001 => { 0x40030000000000000000000000000000 }, /* 16 */ + 0b11010 => { 0x40060000000000000000000000000000 }, /* 2^7 */ + 0b11011 => { 0x40070000000000000000000000000000 }, /* 2^8 */ + 0b11100 => { 0x400e0000000000000000000000000000 }, /* 2^15 */ + 0b11101 => { 0x400f0000000000000000000000000000 }, /* 2^16 */ + 0b11110 => { 0x7fff0000000000000000000000000000 }, /* +inf */ + 0b11111 => { canonical_NaN_Q() }, + }; + F_Q(rd) = bits; + RETIRE_SUCCESS +} + /* FMINM.H */ union clause ast = RISCV_FMINM_H : (regidx, regidx, regidx) @@ -333,6 +382,66 @@ function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = { RETIRE_SUCCESS } +/* FMINM.Q */ + +union clause ast = RISCV_FMINM_Q : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMINM_Q(rs2, rs1, rd) if haveQExt() & haveZfa() + <-> 0b001_0111 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FMINM_Q(rs2, rs1, rd) + <-> "fminm.q" ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +function clause execute (RISCV_FMINM_Q(rs2, rs1, rd)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let is_quiet = true; + let (rs1_lt_rs2, fflags) = fle_Q (rs1_val_Q, rs2_val_Q, is_quiet); + + let rd_val_Q = if (f_is_NaN_Q(rs1_val_Q) | f_is_NaN_Q(rs2_val_Q)) then canonical_NaN_Q() + else if (f_is_neg_zero_Q(rs1_val_Q) & f_is_pos_zero_Q(rs2_val_Q)) then rs1_val_Q + else if (f_is_neg_zero_Q(rs2_val_Q) & f_is_pos_zero_Q(rs1_val_Q)) then rs2_val_Q + else if rs1_lt_rs2 then rs1_val_Q + else rs2_val_Q; + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +/* FMAXM.Q */ + +union clause ast = RISCV_FMAXM_Q : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMAXM_Q(rs2, rs1, rd) if haveQExt() & haveZfa() + <-> 0b001_0111 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FMAXM_Q(rs2, rs1, rd) + <-> "fmaxm.q" ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +function clause execute (RISCV_FMAXM_Q(rs2, rs1, rd)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let is_quiet = true; + let (rs2_lt_rs1, fflags) = fle_Q (rs2_val_Q, rs1_val_Q, is_quiet); + + let rd_val_Q = if (f_is_NaN_Q(rs1_val_Q) | f_is_NaN_Q(rs2_val_Q)) then canonical_NaN_Q() + else if (f_is_neg_zero_Q(rs1_val_Q) & f_is_pos_zero_Q(rs2_val_Q)) then rs2_val_Q + else if (f_is_neg_zero_Q(rs2_val_Q) & f_is_pos_zero_Q(rs1_val_Q)) then rs1_val_Q + else if rs2_lt_rs1 then rs1_val_Q + else rs2_val_Q; + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + /* FROUND.H */ union clause ast = RISCV_FROUND_H : (regidx, rounding_mode, regidx) @@ -501,6 +610,62 @@ function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = { } } +/* FROUND.Q */ + +union clause ast = RISCV_FROUND_Q : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUND_Q(rs1, rm, rd) if haveQExt() & haveZfa() + <-> 0b010_0011 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FROUND_Q(rs1, rm, rd) + <-> "fround.q" ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUND_Q(rs1, rm, rd)) = { + let rs1_val_Q = F_Q(rs1); + + match (select_instr_or_fcsr_rm(rm)) { + None() => { handle_illegal(); RETIRE_FAIL }, + Some(rm') => { + let rm_3b = encdec_rounding_mode(rm'); + let (fflags, rd_val_Q) = riscv_f128roundToInt(rm_3b, rs1_val_Q, false); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +/* FROUNDNX.Q */ + +union clause ast = RISCV_FROUNDNX_Q : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUNDNX_Q(rs1, rm, rd) if haveQExt() & haveZfa() + <-> 0b010_0011 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FROUNDNX_Q(rs1, rm, rd) + <-> "froundnx.q" ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUNDNX_Q(rs1, rm, rd)) = { + let rs1_val_Q = F_Q(rs1); + + match (select_instr_or_fcsr_rm(rm)) { + None() => { handle_illegal(); RETIRE_FAIL }, + Some(rm') => { + let rm_3b = encdec_rounding_mode(rm'); + let (fflags, rd_val_Q) = riscv_f128roundToInt(rm_3b, rs1_val_Q, true); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + /* FMVH.X.D */ union clause ast = RISCV_FMVH_X_D : (regidx, regidx) @@ -546,6 +711,53 @@ function clause execute (RISCV_FMVP_D_X(rs2, rs1, rd)) = { RETIRE_SUCCESS } +/* FMVH.X.Q */ + +union clause ast = RISCV_FMVH_X_Q : (regidx, regidx) + +mapping clause encdec = RISCV_FMVH_X_Q(rs1, rd) if haveQExt() & haveZfa() & in64BitMode() + <-> 0b111_0011 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveQExt() & haveZfa() & in64BitMode() + +mapping clause assembly = RISCV_FMVH_X_Q(rs1, rd) + <-> "fmvh.x.q" ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_name(rs1) + +function clause execute (RISCV_FMVH_X_Q(rs1, rd)) = { + assert(sizeof(xlen) == 64); + let rs1_val_Q = F_Q(rs1)[127..64]; + let rd_val_X : xlenbits = sign_extend(rs1_val_Q); + X(rd) = rd_val_X; + RETIRE_SUCCESS +} + +/* FMVP.X.D */ + +union clause ast = RISCV_FMVP_Q_X : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMVP_Q_X(rs2, rs1, rd) if haveQExt() & haveZfa() & in64BitMode() + <-> 0b101_1011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveQExt() & haveZfa() & in64BitMode() + +mapping clause assembly = RISCV_FMVP_Q_X(rs2, rs1, rd) + <-> "fmvp.q.x" ^ spc() ^ freg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ reg_name(rs2) + +function clause execute (RISCV_FMVP_Q_X(rs2, rs1, rd)) = { + assert(sizeof(xlen) ==64); + let rs1_val_X = X(rs1)[63..0]; + let rs2_val_X = X(rs2)[63..0]; + + /* Concatenate the two values using '@' operator */ + /* e.g. */ + /* rs1 = 0x01234567 */ + /* rs2 = 0x89abcdef */ + /* rd = rs1 @ rs2 => 0x89abcdef01234567 */ + let rd_val_Q = rs2_val_X @ rs1_val_X; + + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + /* FLEQ.H */ union clause ast = RISCV_FLEQ_H : (regidx, regidx, regidx) @@ -691,6 +903,54 @@ function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = { RETIRE_SUCCESS } +/* FLEQ.Q */ + +union clause ast = RISCV_FLEQ_Q : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLEQ_Q(rs2, rs1, rd) if haveQExt() & haveZfa() + <-> 0b101_0011 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FLEQ_Q(rs2, rs1, rd) + <-> "fleq.q" ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +function clause execute(RISCV_FLEQ_Q(rs2, rs1, rd)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Le_quiet (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* FLTQ.Q */ + +union clause ast = RISCV_FLTQ_Q : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLTQ_Q(rs2, rs1, rd) if haveQExt() & haveZfa() + <-> 0b101_0011 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveQExt() & haveZfa() + +mapping clause assembly = RISCV_FLTQ_Q(rs2, rs1, rd) + <-> "fltq.q" ^ spc() ^ freg_name(rd) + ^ sep() ^ freg_name(rs1) + ^ sep() ^ freg_name(rs2) + +function clause execute(RISCV_FLTQ_Q(rs2, rs1, rd)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Lt_quiet (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + /* FCVTMOD.W.D */ /* diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index f16d99895..2093c7b12 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -542,6 +542,10 @@ mapping clause encdec = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D) if haveHalfFPU() <-> 0b010_0010 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() +mapping clause encdec = + F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_Q) if haveHalfFPU() +<-> 0b010_0010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() + mapping clause encdec = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H) if haveHalfFPU() <-> 0b010_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() @@ -550,8 +554,9 @@ mapping clause encdec = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H) if haveHalfFPU() <-> 0b010_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() -// TODO: -/* FCVT_H_Q, FCVT_Q_H : Will be added with Q Extension */ +mapping clause encdec = + F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_Q_H) if haveHalfFPU() +<-> 0b010_0011 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() /* F instructions, RV64 only */ @@ -678,6 +683,21 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = { } } +function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_Q)) = { + let rs1_val_Q = F_Q(rs1); + match (select_instr_or_fcsr_rm (rm)) { + None() => { handle_illegal(); RETIRE_FAIL }, + Some(rm') => { + let rm_3b = encdec_rounding_mode(rm'); + let (fflags, rd_val_H) = riscv_f128ToF16 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + F_or_X_H(rd) = rd_val_H; + RETIRE_SUCCESS + } + } +} + function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { @@ -693,7 +713,6 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { } } - function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = { let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { @@ -709,6 +728,21 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = { } } +function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_Q_H)) = { + let rs1_val_H = F_or_X_H(rs1); + match (select_instr_or_fcsr_rm (rm)) { + None() => { handle_illegal(); RETIRE_FAIL }, + Some(rm') => { + let rm_3b = encdec_rounding_mode(rm'); + let (fflags, rd_val_Q) = riscv_f16ToF128 (rm_3b, rs1_val_H); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = { assert(sizeof(xlen) >= 64); let rs1_val_H = F_or_X_H(rs1); @@ -784,8 +818,10 @@ mapping f_un_rm_type_mnemonic_H : f_un_rm_op_H <-> string = { FCVT_H_S <-> "fcvt.h.s", FCVT_H_D <-> "fcvt.h.d", + FCVT_H_Q <-> "fcvt.h.q", FCVT_S_H <-> "fcvt.s.h", FCVT_D_H <-> "fcvt.d.h", + FCVT_Q_H <-> "fcvt.q.h", FCVT_L_H <-> "fcvt.l.h", FCVT_LU_H <-> "fcvt.lu.h", @@ -859,6 +895,12 @@ mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) +mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_Q) + <-> f_un_rm_type_mnemonic_H(FCVT_H_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H) <-> f_un_rm_type_mnemonic_H(FCVT_S_H) ^ spc() ^ freg_or_reg_name(rd) @@ -871,6 +913,12 @@ mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H) ^ sep() ^ freg_or_reg_name(rs1) ^ sep() ^ frm_mnemonic(rm) +mapping clause assembly = F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_Q_H) + <-> f_un_rm_type_mnemonic_H(FCVT_Q_H) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + /* ****************************************************************** */ /* Unary, no rounding mode */ diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index ece2fd6b3..4f4e31937 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -282,7 +282,6 @@ function riscv_ui64ToF16 (rm, v) = { (float_fflags[4 .. 0], float_result[15 .. 0]) } - val extern_f32ToI32 = {c: "softfloat_f32toi32", ocaml: "Softfloat.f32_to_i32", lem: "softfloat_f32_to_i32"} : (bits_rm, bits_S) -> unit val riscv_f32ToI32 : (bits_rm, bits_S) -> (bits_fflags, bits_W) function riscv_f32ToI32 (rm, v) = { @@ -395,6 +394,62 @@ function riscv_ui64ToF64 (rm, v) = { (float_fflags[4 .. 0], float_result[63..0]) } +val extern_f128ToI32 = {c: "softfloat_f128toi32", ocaml: "Softfloat.f128_to_i32"} : (bits_rm, bits_Q) -> unit +val riscv_f128ToI32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W) +function riscv_f128ToI32 (rm, v) = { + extern_f128ToI32(rm, v); + (float_fflags[4 .. 0], float_result[31..0]) +} + +val extern_f128ToUi32 = {c: "softfloat_f128toui32", ocaml: "Softfloat.f128_to_ui32"} : (bits_rm, bits_Q) -> unit +val riscv_f128ToUi32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W) +function riscv_f128ToUi32 (rm, v) = { + extern_f128ToUi32(rm, v); + (float_fflags[4 .. 0], float_result[31..0]) +} + +val extern_i32ToF128 = {c: "softfloat_i32tof128", ocaml: "Softfloat.i32_to_f128"} : (bits_rm, bits_W) -> unit +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]) +} + +val extern_ui32ToF128 = {c: "softfloat_ui32tof128", ocaml: "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]) +} + +val extern_f128ToI64 = {c: "softfloat_f128toi64", ocaml: "Softfloat.f128_to_i64"} : (bits_rm, bits_Q) -> 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]) +} + +val extern_f128ToUi64 = {c: "softfloat_f128toui64", ocaml: "Softfloat.f128_to_ui64"} : (bits_rm, bits_Q) -> 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]) +} + +val extern_i64ToF128 = {c: "softfloat_i64tof128", ocaml: "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]) +} + +val extern_ui64ToF128 = {c: "softfloat_ui64tof128", ocaml: "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]) +} + val extern_f16ToF32 = {c: "softfloat_f16tof32", ocaml: "Softfloat.f16_to_f32", lem: "softfloat_f16_to_f32"} : (bits_rm, bits_H) -> unit val riscv_f16ToF32 : (bits_rm, bits_H) -> (bits_fflags, bits_S) function riscv_f16ToF32 (rm, v) = { @@ -409,11 +464,11 @@ function riscv_f16ToF64 (rm, v) = { (float_fflags[4 .. 0], float_result[63..0]) } -val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit -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]) +val extern_f16ToF128 = {c: "softfloat_f16tof128", ocaml: "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]) } val extern_f32ToF16 = {c: "softfloat_f32tof16", ocaml: "Softfloat.f32_to_f16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit @@ -423,6 +478,20 @@ function riscv_f32ToF16 (rm, v) = { (float_fflags[4 .. 0], float_result[15 .. 0]) } +val extern_f32ToF64 = {c: "softfloat_f32tof64", ocaml: "Softfloat.f32_to_f64", lem: "softfloat_f32_to_f64"} : (bits_rm, bits_S) -> unit +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]) +} + +val extern_f32ToF128 = {c: "softfloat_f32tof128", ocaml: "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]) +} + val extern_f64ToF16 = {c: "softfloat_f64tof16", ocaml: "Softfloat.f64_to_f16", lem: "softfloat_f64_to_f16"} : (bits_rm, bits_D) -> unit val riscv_f64ToF16 : (bits_rm, bits_D) -> (bits_fflags, bits_H) function riscv_f64ToF16 (rm, v) = { @@ -437,92 +506,34 @@ function riscv_f64ToF32 (rm, v) = { (float_fflags[4 .. 0], float_result[31 .. 0]) } -val extern_f128ToI32 = {c: "softfloat_f128toi32", ocaml: "Softfloat.f128_to_i32"} : (bits_rm, bits_Q) -> unit -val riscv_f128ToI32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W) -function riscv_f128ToI32 (rm, v) = { - extern_f128ToI32(rm, v); - (float_fflags[4 .. 0], float_result[31..0]) -} - -val extern_f128ToUi32 = {c: "softfloat_f128toui32", ocaml: "Softfloat.f128_to_ui32"} : (bits_rm, bits_Q) -> unit -val riscv_f128ToUi32 : (bits_rm, bits_Q) -> (bits_fflags, bits_W) -function riscv_f128ToUi32 (rm, v) = { - extern_f128ToUi32(rm, v); - (float_fflags[4 .. 0], float_result[31..0]) -} - -val extern_i32ToF128 = {c: "softfloat_i32tof128", ocaml: "Softfloat.i32_to_f128"} : (bits_rm, bits_W) -> unit -val riscv_i32ToF128 : (bits_rm, bits_W) -> (bits_fflags, bits_Q) -function riscv_i32ToF128 (rm, v) = { - extern_i32ToF128(rm, v); +val extern_f64ToF128 = {c: "softfloat_f64tof128", ocaml: "Softfloat.f64_to_f128"} : (bits_rm, bits_D) -> unit +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]) } -val extern_ui32ToF128 = {c: "softfloat_ui32tof128", ocaml: "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]) +val extern_f128ToF16 = {c: "softfloat_f128tof16", ocaml: "Softfloat.f128_to_f16"} : (bits_rm, bits_Q) -> unit +val riscv_f128ToF16 : (bits_rm, bits_Q) -> (bits_fflags, bits_H) +function riscv_f128ToF16 (rm, v) = { + extern_f128ToF16(rm, v); + (float_fflags[4 .. 0], float_result[15..0]) } val extern_f128ToF32 = {c: "softfloat_f128tof32", ocaml: "Softfloat.f128_to_f32"} : (bits_rm, bits_Q) -> unit -val riscv_f128ToF32 : (bits_rm, bits_Q) -> (bits_fflags, bits_Q) +val riscv_f128ToF32 : (bits_rm, bits_Q) -> (bits_fflags, bits_S) function riscv_f128ToF32 (rm, v) = { extern_f128ToF32(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) -} - -val extern_f32ToF128 = {c: "softfloat_f32tof128", ocaml: "Softfloat.f32_to_f128"} : (bits_rm, bits_Q) -> unit -val riscv_f32ToF128 : (bits_rm, bits_Q) -> (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[31..0]) } val extern_f128ToF64 = {c: "softfloat_f128tof64", ocaml: "Softfloat.f128_to_f64"} : (bits_rm, bits_Q) -> unit -val riscv_f128ToF64 : (bits_rm, bits_Q) -> (bits_fflags, bits_Q) +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[127..0]) -} - -val extern_f64ToF128 = {c: "softfloat_f64tof128", ocaml: "Softfloat.f64_to_f128"} : (bits_rm, bits_Q) -> unit -val riscv_f64ToF128 : (bits_rm, bits_Q) -> (bits_fflags, bits_Q) -function riscv_f64ToF128 (rm, v) = { - extern_f64ToF128(rm, v); - (float_fflags[4 .. 0], float_result[127..0]) -} - -val extern_f128ToI64 = {c: "softfloat_f128toi64", ocaml: "Softfloat.f128_to_i64"} : (bits_rm, bits_Q) -> 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]) -} - -val extern_i64ToF128 = {c: "softfloat_i64tof128", ocaml: "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]) -} - -val extern_f128ToUi64 = {c: "softfloat_f128toui64", ocaml: "Softfloat.f128_to_ui64"} : (bits_rm, bits_Q) -> 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]) } -val extern_ui64ToF128 = {c: "softfloat_ui64tof128", ocaml: "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]) -} - - - /* **************************************************************** */ /* COMPARISONS */ @@ -631,7 +642,6 @@ 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"} : (bits_Q, bits_Q) -> unit val riscv_f128Lt : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Lt (v1, v2) = { @@ -639,6 +649,13 @@ function riscv_f128Lt (v1, v2) = { (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 riscv_f128Lt_quiet : (bits_Q, bits_Q) -> (bits_fflags, bool) +function riscv_f128Lt_quiet (v1, v2) = { + extern_f128Lt_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f128Le = {c: "softfloat_f128le", ocaml: "Softfloat.f128_le"} : (bits_Q, bits_Q) -> unit val riscv_f128Le : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Le (v1, v2) = { @@ -646,6 +663,13 @@ function riscv_f128Le (v1, v2) = { (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 riscv_f128Le_quiet : (bits_Q, bits_Q) -> (bits_fflags, bool) +function riscv_f128Le_quiet (v1, v2) = { + extern_f128Le_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f128Eq = {c: "softfloat_f128eq", ocaml: "Softfloat.f128_eq"} : (bits_Q, bits_Q) -> unit val riscv_f128Eq : (bits_Q, bits_Q) -> (bits_fflags, bool) function riscv_f128Eq (v1, v2) = { @@ -673,4 +697,12 @@ function riscv_f64roundToInt (rm, v, exact) = { extern_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 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]) +} + /* **************************************************************** */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 465469b33..4d45dad2a 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -301,6 +301,10 @@ function in32BitMode() -> bool = { cur_Architecture() == RV32 } +function in64BitMode() -> bool = { + cur_Architecture() == RV64 +} + /* F, D and Q extensions have to enabled both via misa.{FDQ} as well as mstatus.FS */ function haveFExt() -> bool = (misa[F] == 0b1) & (mstatus[FS] != 0b00) function haveDExt() -> bool = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64 diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml index 88ab68590..0afa32174 100644 --- a/ocaml_emulator/softfloat.ml +++ b/ocaml_emulator/softfloat.ml @@ -144,58 +144,64 @@ let i64_to_f64 rm v = let ui64_to_f64 rm v = () -let f16_to_f32 rm v = +let f128_to_i32 rm v = () -let f16_to_f64 rm v = +let f128_to_ui32 rm v = () -let f32_to_f64 rm v = +let i32_to_f128 rm v = () -let f32_to_f16 rm v = +let ui32_to_f128 rm v = () -let f64_to_f16 rm v = +let f128_to_i64 rm v = () -let f64_to_f32 rm v = +let f128_to_ui64 rm v = () -let f128_to_i32 rm v = +let i64_to_f128 rm v = () -let f128_to_ui32 rm v = +let ui64_to_f128 rm v = () -let i32_to_f128 rm v = +let f16_to_f32 rm v = () -let ui32_to_f128 rm v = +let f16_to_f64 rm v = () -let f32_to_f128 rm v = +let f16_to_f128 rm v = () -let f128_to_f32 rm v = +let f32_to_f16 rm v = () -let f128_to_f64 rm v = +let f32_to_f64 rm v = () -let f64_to_f128 rm v = +let f32_to_f128 rm v = () -let f128_to_i64 rm v = +let f64_to_f16 rm v = () -let i64_to_f128 rm v = +let f64_to_f32 rm v = () -let f128_to_ui64 rm v = +let f64_to_f128 rm v = () -let ui64_to_f128 rm v = +let f128_to_f16 rm v = + () + +let f128_to_f32 rm v = + () + +let f128_to_f64 rm v = () @@ -247,9 +253,15 @@ let f64_eq v1 v2 = let f128_lt v1 v2 = () +let f128_lt_quiet v1 v2 = + () + let f128_le v1 v2 = () +let f128_le_quiet v1 v2 = + () + let f128_eq v1 v2 = () @@ -261,3 +273,6 @@ let f32_round_to_int exact rm v = let f64_round_to_int exact rm v = () + +let f128_round_to_int exact rm v = + ()