From 9e66fc33f4e21725fab8d6b20c1b2da30646077b Mon Sep 17 00:00:00 2001 From: Jordan Carlin Date: Fri, 5 Apr 2024 00:55:08 -0700 Subject: [PATCH] Q extension floating point support Complete Q extension implementation including Zfa instructions Based on original work by 'LiuTaowen-Tony' in #187 --- Makefile | 3 +- .../SoftFloat-3e/source/include/softfloat.h | 46 +- c_emulator/riscv_sail.h | 2 +- c_emulator/riscv_softfloat.c | 420 +++++++- c_emulator/riscv_softfloat.h | 41 + handwritten_support/riscv_extras_fdext.lem | 82 +- model/riscv_fdext_control.sail | 15 +- model/riscv_fdext_regs.sail | 115 ++- model/riscv_flen_Q.sail | 13 + model/riscv_freg_type.sail | 16 +- model/riscv_insts_aext.sail | 21 +- model/riscv_insts_base.sail | 3 +- model/riscv_insts_dext.sail | 8 +- model/riscv_insts_fext.sail | 41 +- model/riscv_insts_qext.sail | 976 ++++++++++++++++++ model/riscv_insts_zfa.sail | 260 +++++ model/riscv_insts_zfh.sail | 60 +- model/riscv_softfloat_interface.sail | 201 +++- model/riscv_sys_control.sail | 9 +- model/riscv_sys_regs.sail | 4 + model/riscv_types.sail | 21 +- 21 files changed, 2236 insertions(+), 121 deletions(-) create mode 100644 model/riscv_flen_Q.sail create mode 100644 model/riscv_insts_qext.sail diff --git a/Makefile b/Makefile index 34fd2bf68..1d0bee57b 100644 --- a/Makefile +++ b/Makefile @@ -19,7 +19,7 @@ else endif SAIL_XLEN += riscv_xlen.sail -SAIL_FLEN := riscv_flen_D.sail +SAIL_FLEN := riscv_flen_Q.sail SAIL_VLEN := riscv_vlen.sail # Instruction sources, depending on target @@ -27,6 +27,7 @@ SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_mis SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_zca.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_zcf.sail SAIL_DEFAULT_INST += riscv_insts_dext.sail riscv_insts_zcd.sail +SAIL_DEFAULT_INST += riscv_insts_qext.sail SAIL_DEFAULT_INST += riscv_insts_svinval.sail diff --git a/c_emulator/SoftFloat-3e/source/include/softfloat.h b/c_emulator/SoftFloat-3e/source/include/softfloat.h index b33374cd6..d2c4eade0 100644 --- a/c_emulator/SoftFloat-3e/source/include/softfloat.h +++ b/c_emulator/SoftFloat-3e/source/include/softfloat.h @@ -100,36 +100,36 @@ void softfloat_raiseFlags( uint_fast8_t ); float16_t ui32_to_f16( uint32_t ); float32_t ui32_to_f32( uint32_t ); float64_t ui32_to_f64( uint32_t ); +float128_t ui32_to_f128( uint32_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t ui32_to_extF80( uint32_t ); -float128_t ui32_to_f128( uint32_t ); #endif void ui32_to_extF80M( uint32_t, extFloat80_t * ); void ui32_to_f128M( uint32_t, float128_t * ); float16_t ui64_to_f16( uint64_t ); float32_t ui64_to_f32( uint64_t ); float64_t ui64_to_f64( uint64_t ); +float128_t ui64_to_f128( uint64_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t ui64_to_extF80( uint64_t ); -float128_t ui64_to_f128( uint64_t ); #endif void ui64_to_extF80M( uint64_t, extFloat80_t * ); void ui64_to_f128M( uint64_t, float128_t * ); float16_t i32_to_f16( int32_t ); float32_t i32_to_f32( int32_t ); float64_t i32_to_f64( int32_t ); +float128_t i32_to_f128( int32_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t i32_to_extF80( int32_t ); -float128_t i32_to_f128( int32_t ); #endif void i32_to_extF80M( int32_t, extFloat80_t * ); void i32_to_f128M( int32_t, float128_t * ); float16_t i64_to_f16( int64_t ); float32_t i64_to_f32( int64_t ); float64_t i64_to_f64( int64_t ); +float128_t i64_to_f128( int64_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t i64_to_extF80( int64_t ); -float128_t i64_to_f128( int64_t ); #endif void i64_to_extF80M( int64_t, extFloat80_t * ); void i64_to_f128M( int64_t, float128_t * ); @@ -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 * ); @@ -182,9 +182,9 @@ int_fast32_t f32_to_i32_r_minMag( float32_t, bool ); int_fast64_t f32_to_i64_r_minMag( float32_t, bool ); float16_t f32_to_f16( float32_t ); float64_t f32_to_f64( float32_t ); +float128_t f32_to_f128( float32_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t f32_to_extF80( float32_t ); -float128_t f32_to_f128( float32_t ); #endif void f32_to_extF80M( float32_t, extFloat80_t * ); void f32_to_f128M( float32_t, float128_t * ); @@ -217,9 +217,9 @@ int_fast32_t f64_to_i32_r_minMag( float64_t, bool ); int_fast64_t f64_to_i64_r_minMag( float64_t, bool ); float16_t f64_to_f16( float64_t ); float32_t f64_to_f32( float64_t ); +float128_t f64_to_f128( float64_t ); #ifdef SOFTFLOAT_FAST_INT64 extFloat80_t f64_to_extF80( float64_t ); -float128_t f64_to_f128( float64_t ); #endif void f64_to_extF80M( float64_t, extFloat80_t * ); void f64_to_f128M( float64_t, float128_t * ); @@ -309,34 +309,34 @@ bool extF80M_isSignalingNaN( const extFloat80_t * ); | 128-bit (quadruple-precision) floating-point operations. *----------------------------------------------------------------------------*/ #ifdef SOFTFLOAT_FAST_INT64 -uint_fast32_t f128_to_ui32( float128_t, uint_fast8_t, bool ); -uint_fast64_t f128_to_ui64( float128_t, uint_fast8_t, bool ); -int_fast32_t f128_to_i32( float128_t, uint_fast8_t, bool ); -int_fast64_t f128_to_i64( float128_t, uint_fast8_t, bool ); +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 ); +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 ); +bool f128_eq( float128_t, float128_t ); +bool f128_le( float128_t, float128_t ); +bool f128_lt( float128_t, float128_t ); +float128_t f128_sqrt( float128_t ); float32_t f128_to_f32( float128_t ); float64_t f128_to_f64( float128_t ); -extFloat80_t f128_to_extF80( float128_t ); -float128_t f128_roundToInt( float128_t, uint_fast8_t, bool ); +uint_fast32_t f128_to_ui32( float128_t, uint_fast8_t, bool ); +uint_fast64_t f128_to_ui64( float128_t, uint_fast8_t, bool ); +int_fast32_t f128_to_i32( float128_t, uint_fast8_t, bool ); +int_fast64_t f128_to_i64( float128_t, uint_fast8_t, bool ); float128_t f128_add( float128_t, float128_t ); float128_t f128_sub( float128_t, float128_t ); float128_t f128_mul( float128_t, float128_t ); float128_t f128_mulAdd( float128_t, float128_t, float128_t ); float128_t f128_div( float128_t, float128_t ); -float128_t f128_rem( float128_t, float128_t ); -float128_t f128_sqrt( float128_t ); -bool f128_eq( float128_t, float128_t ); -bool f128_le( float128_t, float128_t ); -bool f128_lt( 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 uint_fast32_t f128M_to_ui32( const float128_t *, uint_fast8_t, bool ); uint_fast64_t f128M_to_ui64( const float128_t *, uint_fast8_t, bool ); int_fast32_t f128M_to_i32( const float128_t *, uint_fast8_t, bool ); diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index da29c2ba9..804a3e0fb 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -64,7 +64,7 @@ extern mach_bits zmstatus; extern mach_bits zmepc, zmtval; extern mach_bits zsepc, zstval; -extern mach_bits zfloat_result, zfloat_fflags; +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 2c2d0d2b2..46edb3627 100644 --- a/c_emulator/riscv_softfloat.c +++ b/c_emulator/riscv_softfloat.c @@ -10,6 +10,14 @@ static uint_fast8_t uint8_of_rm(mach_bits rm) return (uint_fast8_t)rm; } +static float128_t to_float128(mach_bits low, mach_bits high) +{ + float128_t res; + res.v[0] = low; + res.v[1] = high; + return res; +} + #define SOFTFLOAT_PRELUDE(rm) \ softfloat_exceptionFlags = 0; \ softfloat_roundingMode = (uint_fast8_t)rm @@ -18,6 +26,11 @@ static uint_fast8_t uint8_of_rm(mach_bits rm) zfloat_result = res.v; \ 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) { SOFTFLOAT_PRELUDE(rm); @@ -186,6 +199,66 @@ unit softfloat_f64div(mach_bits rm, mach_bits v1, mach_bits v2) return UNIT; } +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res = f128_add(a, b); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res = f128_sub(a, b); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res = f128_div(a, b); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res = f128_mul(a, b); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + unit softfloat_f16muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3) { SOFTFLOAT_PRELUDE(rm); @@ -231,6 +304,23 @@ unit softfloat_f64muladd(mach_bits rm, mach_bits v1, mach_bits v2, mach_bits v3) return UNIT; } +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_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); + + return UNIT; +} + unit softfloat_f16sqrt(mach_bits rm, mach_bits v) { SOFTFLOAT_PRELUDE(rm); @@ -270,6 +360,19 @@ unit softfloat_f64sqrt(mach_bits rm, mach_bits v) return UNIT; } +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_low, v_high); + res = f128_sqrt(a); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} + // The boolean 'true' argument in the conversion calls below selects // 'exact' conversion, which sets the Inexact exception flag if // needed. @@ -449,6 +552,70 @@ unit softfloat_f64toui64(mach_bits rm, mach_bits v) return UNIT; } +unit softfloat_f128toi32(mach_bits rm, mach_bits v_low, mach_bits v_high) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float32_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v_low, v_high); + res.v = f128_to_i32(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128toui32(mach_bits rm, mach_bits v_low, mach_bits v_high) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float32_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v_low, v_high); + res.v = f128_to_ui32(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128toi64(mach_bits rm, mach_bits v_low, mach_bits v_high) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float64_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v_low, v_high); + res.v = f128_to_i64(a, rm8, true); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f128toui64(mach_bits rm, mach_bits v_low, mach_bits v_high) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float64_t res; + uint_fast8_t rm8 = uint8_of_rm(rm); + + a = to_float128(v_low, v_high); + 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); @@ -593,6 +760,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); @@ -621,6 +848,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); @@ -635,16 +891,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; } @@ -677,6 +934,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, mach_bits v_low, mach_bits v_high) +{ + SOFTFLOAT_PRELUDE(rm); + + float128_t a; + float16_t res; + + a = to_float128(v_low, v_high); + res = f128_to_f16(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +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_low, v_high); + res = f128_to_f32(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +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_low, v_high); + res = f128_to_f64(a); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f16lt(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -887,6 +1204,86 @@ unit softfloat_f64eq(mach_bits v1, mach_bits v2) return UNIT; } +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res.v = f128_lt(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res.v = f128_lt_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res.v = f128_le(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res.v = f128_le_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +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_low, v1_high); + b = to_float128(v2_low, v2_high); + res.v = f128_eq(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact) { SOFTFLOAT_PRELUDE(rm); @@ -928,3 +1325,18 @@ unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact) return UNIT; } + +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_low, v_high); + res = f128_roundToInt(a, rm8, exact); + + SOFTFLOAT_POSTLUDE_128(res); + + return UNIT; +} diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h index fc7b2252e..3b3f9220e 100644 --- a/c_emulator/riscv_softfloat.h +++ b/c_emulator/riscv_softfloat.h @@ -15,16 +15,29 @@ 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, 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); 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, 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, 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); @@ -41,6 +54,11 @@ 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, 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); unit softfloat_i64tof16(mach_bits rm, mach_bits v); @@ -56,13 +74,24 @@ 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_i32tof128(mach_bits rm, mach_bits v); +unit softfloat_ui32tof128(mach_bits rm, mach_bits v); +unit softfloat_i64tof128(mach_bits rm, mach_bits v); +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_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); @@ -79,7 +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(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, 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 81c6af504..3ddadf4da 100644 --- a/handwritten_support/riscv_extras_fdext.lem +++ b/handwritten_support/riscv_extras_fdext.lem @@ -89,6 +89,9 @@ 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 -> bitvector -> bool -> unit +let softfloat_f128_round_to_int _ _ _ = () + val softfloat_f16_add : bitvector -> bitvector -> bitvector -> unit let softfloat_f16_add _ _ _ = () @@ -125,6 +128,18 @@ let softfloat_f64_mul _ _ _ = () val softfloat_f64_div : bitvector -> bitvector -> bitvector -> unit let softfloat_f64_div _ _ _ = () +val softfloat_f128_add : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_add _ _ _ = () + +val softfloat_f128_sub : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_sub _ _ _ = () + +val softfloat_f128_mul : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_mul _ _ _ = () + +val softfloat_f128_div : bitvector -> bitvector -> bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_div _ _ _ = () + val softfloat_f16_muladd : bitvector -> bitvector -> bitvector -> bitvector -> unit let softfloat_f16_muladd _ _ _ _ = () @@ -135,6 +150,9 @@ 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 -> bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_muladd _ _ _ _ = () + val softfloat_f16_sqrt : bitvector -> bitvector -> unit let softfloat_f16_sqrt _ _ = () @@ -145,6 +163,9 @@ let softfloat_f32_sqrt _ _ = () val softfloat_f64_sqrt : bitvector -> bitvector -> unit let softfloat_f64_sqrt _ _ = () +val softfloat_f128_sqrt : bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_sqrt _ _ = () + val softfloat_f16_to_i32: bitvector -> bitvector -> unit let softfloat_f16_to_i32 _ _ = () @@ -220,6 +241,30 @@ 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 -> bitvector -> unit +let softfloat_f128_to_i32 _ _ = () + +val softfloat_f128_to_ui32: bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_to_ui32 _ _ = () + +val softfloat_i32_to_f128: bitvector -> bitvector -> unit +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 -> bitvector -> unit +let softfloat_f128_to_i64 _ _ = () + +val softfloat_f128_to_ui64: bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_to_ui64 _ _ = () + +val softfloat_i64_to_f128: bitvector -> bitvector -> unit +let softfloat_i64_to_f128 _ _ = () + +val softfloat_ui64_to_f128: bitvector -> bitvector -> unit +let softfloat_ui64_to_f128 _ _ = () + val softfloat_f16_to_f32: bitvector -> bitvector -> unit let softfloat_f16_to_f32 _ _ = () @@ -227,18 +272,36 @@ let softfloat_f16_to_f32 _ _ = () val softfloat_f16_to_f64: bitvector -> bitvector -> unit let softfloat_f16_to_f64 _ _ = () -val softfloat_f32_to_f64: bitvector -> bitvector -> unit -let softfloat_f32_to_f64 _ _ = () +val softfloat_f16_to_f128: bitvector -> bitvector -> unit +let softfloat_f16_to_f128 _ _ = () val softfloat_f32_to_f16: bitvector -> bitvector -> unit let softfloat_f32_to_f16 _ _ = () +val softfloat_f32_to_f64: bitvector -> bitvector -> unit +let softfloat_f32_to_f64 _ _ = () + +val softfloat_f32_to_f128: bitvector -> bitvector -> unit +let softfloat_f32_to_f128 _ _ = () + val softfloat_f64_to_f16: bitvector -> bitvector -> unit let softfloat_f64_to_f16 _ _ = () val softfloat_f64_to_f32: bitvector -> bitvector -> unit 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 -> bitvector -> unit +let softfloat_f128_to_f16 _ _ = () + +val softfloat_f128_to_f32: bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_to_f32 _ _ = () + +val softfloat_f128_to_f64: bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_to_f64 _ _ = () + val softfloat_f16_lt : bitvector -> bitvector -> unit let softfloat_f16_lt _ _ = () @@ -284,3 +347,18 @@ let softfloat_f64_le_quiet _ _ = () val softfloat_f64_eq : bitvector -> bitvector -> unit let softfloat_f64_eq _ _ = () + +val softfloat_f128_lt : bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_lt _ _ = () + +val softfloat_f128_lt_quiet : bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_lt_quiet _ _ = () + +val softfloat_f128_le : bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_le _ _ = () + +val softfloat_f128_le_quiet : bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_le_quiet _ _ = () + +val softfloat_f128_eq : bitvector -> bitvector -> bitvector -> unit +let softfloat_f128_eq _ _ = () diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 11b8e425e..fda085ab8 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -6,14 +6,14 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* **************************************************************** */ -/* Floating point register file and accessors for F, D extensions */ -/* Floating point CSR and accessors */ -/* **************************************************************** */ +/* ***************************************************************** */ +/* Floating point register file and accessors for F, D, Q extensions */ +/* Floating point CSR and accessors */ +/* ***************************************************************** */ -/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ -/* **************************************************************** */ +/* ***************************************************************** */ enum clause extension = Ext_F function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b00) @@ -21,6 +21,9 @@ function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b0 enum clause extension = Ext_D function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64 +enum clause extension = Ext_Q +function clause extensionEnabled(Ext_Q) = (misa[Q] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 128 + enum clause extension = Ext_Zfinx function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx() diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 63652da88..7d52700b6 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -6,64 +6,100 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* **************************************************************** */ -/* Floating point register file and accessors for F, D extensions */ -/* Floating point CSR and accessors */ -/* **************************************************************** */ +/* ***************************************************************** */ +/* Floating point register file and accessors for F, D, Q extensions */ +/* Floating point CSR and accessors */ +/* ***************************************************************** */ /* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ /* **************************************************************** */ /* NaN boxing/unboxing. */ -/* When 16-bit floats (half-precision) are stored in 32/64-bit regs */ -/* they must be 'NaN boxed'. */ -/* When 16-bit floats (half-precision) are read from 32/64-bit regs */ -/* they must be 'NaN unboxed'. */ -/* When 32-bit floats (single-precision) are stored in 64-bit regs */ +/* When 16-bit floats (half-precision) are stored in 32/64/128-bit */ +/* regs they must be 'NaN boxed'. */ +/* When 16-bit floats (half-precision) are read from 32/64/128-bit */ +/* regs they must be 'NaN unboxed'. */ +/* When 32-bit floats (single-precision) are stored in 64/128-bit */ +/* regs they must be 'NaN boxed'. */ +/* When 32-bit floats (single-precision) are read from 64/128-bit */ +/* regs they must be 'NaN unboxed'. */ +/* When 64-bit floats (double-precision) are stored in 128-bit regs */ /* they must be 'NaN boxed' (upper 32b all ones). */ -/* When 32-bit floats (single-precision) are read from 64-bit regs */ +/* When 64-bit floats (double-precision) are read from 128-bit regs */ /* they must be 'NaN unboxed'. */ function canonical_NaN_H() -> bits(16) = 0x_7e00 function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000 function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000 +function canonical_NaN_Q() -> bits(128) = 0x_7fff_0000_0000_0000_0000_0000_0000_0000 val nan_box_H : bits(16) -> flenbits function nan_box_H val_16b = - if (sizeof(flen) == 32) - then 0x_FFFF @ val_16b - else 0x_FFFF_FFFF_FFFF @ val_16b + match (sizeof(flen)) { + 32 => 0x_FFFF @ val_16b, + 64 => 0x_FFFF_FFFF_FFFF @ val_16b, + _ => 0x_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF @ val_16b // flen = 128 + } val nan_unbox_H : flenbits -> bits(16) -function nan_unbox_H regval = - if (sizeof(flen) == 32) - then if regval [31..16] == 0x_FFFF - then regval [15..0] - else canonical_NaN_H() - else if regval [63..16] == 0x_FFFF_FFFF_FFFF - then regval [15..0] - else canonical_NaN_H() +function nan_unbox_H regval = { + match sizeof(flen) { + 32 if regval [31..16] == 0x_FFFF + => regval[15..0], + 64 if regval [63..16] == 0x_FFFF_FFFF_FFFF + => regval[15..0], + 128 if regval [127..16] == 0x_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF + => regval[15..0], + _ => canonical_NaN_H() + } +} val nan_box_S : bits(32) -> flenbits function nan_box_S val_32b = { assert(sys_enable_fdext()); - if (sizeof(flen) == 32) - then val_32b - else 0x_FFFF_FFFF @ val_32b + match sizeof(flen) { + 32 => val_32b, + 64 => 0x_FFFF_FFFF @ val_32b, + _ => 0x_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF @ val_32b // flen = 128 + } } val nan_unbox_S : flenbits -> bits(32) function nan_unbox_S regval = { assert(sys_enable_fdext()); - if (sizeof(flen) == 32) - then regval - else if regval [63..32] == 0x_FFFF_FFFF - then regval [31..0] - else canonical_NaN_S() + match sizeof(flen) { + 32 => regval, + 64 if regval [63..32] == 0x_FFFF_FFFF + => regval [31..0], + 128 if regval [127..32] == 0x_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF + => regval [31..0], + _ => canonical_NaN_S() + } +} + +val nan_box_D : bits(64) -> flenbits +function nan_box_D val_64b = { + assert(sys_enable_fdext()); + assert(sizeof(flen) >= 64); + if (sizeof(flen) ==64) + then val_64b + else 0x_FFFF_FFFF_FFFF_FFFF @ val_64b + } + +val nan_unbox_D : flenbits -> bits(64) +function nan_unbox_D regval = { + assert(sys_enable_fdext()); + assert(sizeof(flen) >= 64); + match sizeof(flen) { + 64 => regval, + 128 if regval [127..64] == 0x_FFFF_FFFF_FFFF_FFFF + => regval [63..0], + _ => canonical_NaN_D() + } } -overload nan_box = { nan_box_H, nan_box_S } -overload nan_unbox = { nan_unbox_H, nan_unbox_S } +overload nan_box = { nan_box_H, nan_box_S, nan_box_D } +overload nan_unbox = { nan_unbox_H, nan_unbox_S, nan_unbox_D } /* **************************************************************** */ /* Floating point register file */ @@ -240,19 +276,34 @@ val rF_D : regidx -> bits(64) function rF_D(i) = { assert(sizeof(flen) >= 64); assert(sys_enable_fdext() & not(sys_enable_zfinx())); - F(i) + nan_unbox(F(i)) } val wF_D : (regidx, bits(64)) -> unit function wF_D(i, data) = { assert(sizeof(flen) >= 64); assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) = nan_box(data) +} + +val rF_Q : bits(5) -> bits(128) +function rF_Q(i) = { + assert(sizeof(flen) >= 128); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) +} + +val wF_Q : (bits(5), bits(128)) -> unit +function wF_Q(i, data) = { + assert(sizeof(flen) >= 128); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); F(i) = data } overload F_H = { rF_H, wF_H } overload F_S = { rF_S, wF_S } overload F_D = { rF_D, wF_D } +overload F_Q = { rF_Q, wF_Q } val rF_or_X_H : regidx -> bits(16) function rF_or_X_H(i) = { diff --git a/model/riscv_flen_Q.sail b/model/riscv_flen_Q.sail new file mode 100644 index 000000000..4e08a1a1d --- /dev/null +++ b/model/riscv_flen_Q.sail @@ -0,0 +1,13 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* Define the FLEN value for the 'Q' extension. */ + +type flen : Int = 128 +type flen_bytes : Int = 16 +type flenbits = bits(flen) diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail index a084c0f73..a7eaf0903 100644 --- a/model/riscv_freg_type.sail +++ b/model/riscv_freg_type.sail @@ -6,7 +6,7 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -/* Definitions for floating point registers (F and D extensions) */ +/* Definitions for floating point registers (F, D and Q extensions) */ /* default register type */ type fregtype = flenbits @@ -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 */ @@ -70,3 +70,15 @@ enum f_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FL enum f_un_op_D = {FCLASS_D, /* RV32 and RV64 */ FMV_X_D, FMV_D_X} /* RV64 only */ + +enum f_madd_op_Q = {FMADD_Q, FMSUB_Q, FNMSUB_Q, FNMADD_Q} + +enum f_bin_rm_op_Q = {FADD_Q, FSUB_Q, FMUL_Q, FDIV_Q} + +enum f_un_rm_op_Q = {FSQRT_Q, FCVT_W_Q, FCVT_WU_Q, FCVT_Q_W, FCVT_Q_WU, // RV32 and RV64 + FCVT_S_Q, FCVT_Q_S, FCVT_D_Q, FCVT_Q_D, + FCVT_L_Q, FCVT_LU_Q, FCVT_Q_L, FCVT_Q_LU} // RV64 only + +enum f_bin_op_Q = {FSGNJ_Q, FSGNJN_Q, FSGNJX_Q, FMIN_Q, FMAX_Q, FEQ_Q, FLT_Q, FLE_Q} + +enum f_un_op_Q = {FCLASS_Q} diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 18c047e49..f194c2128 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -23,14 +23,6 @@ function aqrl_str(aq : bool, rl : bool) -> string = (true, true) => ".aqrl" } -function lrsc_width_str(width : word_width) -> string = - match width { - BYTE => ".b", - HALF => ".h", - WORD => ".w", - DOUBLE => ".d" - } - /** * RISC-V A-extension defines LR / SC / AMOs for word and double * RISC-V Zabha extension defines AMOs for byte and halfword @@ -49,6 +41,7 @@ function amo_width_valid(size : word_width) -> bool = { HALF => extensionEnabled(Ext_Zabha), WORD => true, DOUBLE => sizeof(xlen) >= 64, + _ => false } } @@ -58,8 +51,8 @@ function clause extensionEnabled(Ext_Zalrsc) = misa[A] == 0b1 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx) -mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) - <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) +mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) + <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ size_enc_wide(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) /* We could set load-reservations on physical or virtual addresses. * However most chips (especially multi-core) will use physical addresses. @@ -106,8 +99,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd) /* ****************************************************************** */ union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx) -mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) - <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) +mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) + <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ size_enc_wide(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zalrsc) & lrsc_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { @@ -185,8 +178,8 @@ mapping encdec_amoop : amoop <-> bits(5) = { AMOMAXU <-> 0b11100 } -mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zaamo) & amo_width_valid(size) - <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zaamo) & amo_width_valid(size) +mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd) if extensionEnabled(Ext_Zaamo) & amo_width_valid(size) + <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ size_enc_wide(size) @ rd @ 0b0101111 if extensionEnabled(Ext_Zaamo) & amo_width_valid(size) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 438fa15d0..a7cd527d9 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -314,6 +314,7 @@ function is_aligned(vaddr : xlenbits, width : word_width) -> bool = HALF => vaddr[0..0] == zeros(), WORD => vaddr[1..0] == zeros(), DOUBLE => vaddr[2..0] == zeros(), + QUAD => vaddr[3..0] == zeros(), } // Return true if the address is misaligned and we don't support misaligned access. @@ -372,7 +373,7 @@ mapping clause assembly = LOAD(imm, rs1, rd, is_unsigned, size, aq, rl) union clause ast = STORE : (bits(12), regidx, regidx, word_width, bool, bool) mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) if size_bytes(size) <= sizeof(xlen_bytes) - <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes) + <-> imm7 : bits(7) @ rs2 @ rs1 @ size_enc_wide(size) @ imm5 : bits(5) @ 0b0100011 if size_bytes(size) <= sizeof(xlen_bytes) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index f366c487a..0f85ba627 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -16,9 +16,9 @@ /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ @@ -945,7 +945,7 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = { assert(sizeof(xlen) >= 64); let rs1_val_X = X(rs1); let rd_val_D = rs1_val_X [63..0]; - F(rd) = rd_val_D; + F_D(rd) = rd_val_D; RETIRE_SUCCESS } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 3a5509ea4..6797532d0 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -16,9 +16,9 @@ /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ @@ -268,7 +268,7 @@ function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | extensionEnabled(Ex /* Floating-point loads */ /* AST */ -/* FLH, FLW and FLD; H/W/D is encoded in 'word_width' */ +/* FLH, FLW, FLD and FLQ; H/W/D/Q is encoded in 'word_width' */ union clause ast = LOAD_FP : (bits(12), regidx, regidx, word_width) @@ -283,12 +283,28 @@ mapping clause encdec = LOAD_FP(imm, rs1, rd, WORD) if extensionEnabled mapping clause encdec = LOAD_FP(imm, rs1, rd, DOUBLE) if extensionEnabled(Ext_D) <-> imm @ rs1 @ 0b011 @ rd @ 0b000_0111 if extensionEnabled(Ext_D) +mapping clause encdec = LOAD_FP(imm, rs1, rd, QUAD) if extensionEnabled(Ext_Q) + <-> imm @ rs1 @ 0b100 @ rd @ 0b000_0111 if extensionEnabled(Ext_Q) + /* Execution semantics ================================ */ val process_fload64 : (regidx, xlenbits, MemoryOpResult(bits(64))) -> Retired function process_fload64(rd, addr, value) = - if sizeof(flen) == 64 + if sizeof(flen) >= 64 + then match value { + MemValue(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }, + MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } + } + else { + /* should not get here */ + RETIRE_FAIL + } + +val process_fload128 : (regidx, xlenbits, MemoryOpResult(bits(128))) + -> Retired +function process_fload128(rd, addr, value) = + if sizeof(flen) >= 128 then match value { MemValue(result) => { F(rd) = result; RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } @@ -335,6 +351,8 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = { process_fload32(rd, vaddr, mem_read(Read(Data), addr, 4, aq, rl, res)), DOUBLE if sizeof(flen) >= 64 => process_fload64(rd, vaddr, mem_read(Read(Data), addr, 8, aq, rl, res)), + QUAD if sizeof(flen) >= 128 => + process_fload128(rd, vaddr, mem_read(Read(Data), addr, 16, aq, rl, res)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point load"), } } @@ -354,7 +372,7 @@ mapping clause assembly = LOAD_FP(imm, rs1, rd, width) /* Floating-point stores */ /* AST */ -/* FSH, FSW and FSD; H/W/D is encoded in 'word_width' */ +/* FSH, FSW, FSD and FSQ; H/W/D/Q is encoded in 'word_width' */ union clause ast = STORE_FP : (bits(12), regidx, regidx, word_width) @@ -369,6 +387,10 @@ mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, WORD) mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, DOUBLE) if extensionEnabled(Ext_D) <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b011 @ imm5 : bits(5) @ 0b010_0111 if extensionEnabled(Ext_D) + +mapping clause encdec = STORE_FP(imm7 @ imm5, rs2, rs1, QUAD) if extensionEnabled(Ext_Q) + <-> imm7 : bits(7) @ rs2 @ rs1 @ 0b100 @ imm5 : bits(5) @ 0b010_0111 if extensionEnabled(Ext_Q) + /* Execution semantics ================================ */ val process_fstore : (xlenbits, MemoryOpResult(bool)) -> Retired @@ -396,7 +418,8 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { BYTE => MemValue () /* bogus placeholder for illegal size */, HALF => mem_write_ea(addr, 2, aq, rl, false), WORD => mem_write_ea(addr, 4, aq, rl, false), - DOUBLE => mem_write_ea(addr, 8, aq, rl, false) + DOUBLE => mem_write_ea(addr, 8, aq, rl, false), + QUAD => mem_write_ea(addr, 16, aq, rl, false) }; match (eares) { MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, @@ -407,7 +430,9 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = { HALF => process_fstore (vaddr, mem_write_value(addr, 2, rs2_val[15..0], aq, rl, con)), WORD => process_fstore (vaddr, mem_write_value(addr, 4, rs2_val[31..0], aq, rl, con)), DOUBLE if sizeof(flen) >= 64 => - process_fstore (vaddr, mem_write_value(addr, 8, rs2_val, aq, rl, con)), + process_fstore (vaddr, mem_write_value(addr, 8, rs2_val[63..0], aq, rl, con)), + QUAD if sizeof(flen) >= 128 => + process_fstore (vaddr, mem_write_value(addr, 16, rs2_val, aq, rl, con)), _ => report_invalid_width(__FILE__, __LINE__, width, "floating point store"), }; } diff --git a/model/riscv_insts_qext.sail b/model/riscv_insts_qext.sail new file mode 100644 index 000000000..84bbd0764 --- /dev/null +++ b/model/riscv_insts_qext.sail @@ -0,0 +1,976 @@ +/*=======================================================================================*/ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except where otherwise noted is subject the BSD */ +/* two-clause license in the LICENSE file. */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/*=======================================================================================*/ + +/* **************************************************************** */ +/* This file specifies the instructions in the Q extension */ +/* (quad precision floating point). */ + +/* RISC-V follows IEEE 754-2008 floating point arithmetic standard. */ + +/* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019 */ + +/* **************************************************************** */ +/* IMPORTANT! */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ +/* The texts follow each other very closely; please try to maintain */ +/* this correspondence as the files are maintained for bug-fixes, */ +/* improvements, and version updates. */ + +/* **************************************************************** */ +/* Note: Rounding Modes and Floating point accrued exception flags */ +/* are defined in riscv_insts_fext.sail. */ +/* In RISC-V, the Q extension requires the F extension, so that */ +/* should have been processed before this one. */ + +/* **************************************************************** */ +/* S and D value structure (sign, exponent, mantissa) */ + +/* TODO: this should be a 'mapping' */ +val fsplit_Q : bits(128) -> (bits(1), bits(15), bits(112)) +function fsplit_Q x128 = (x128[127..127], x128[126..112], x128[111..0]) + +val fmake_Q : (bits(1), bits(15), bits(112)) -> bits(128) +function fmake_Q (sign, exp, mant) = sign @ exp @ mant + +/* ---- Structure tests */ + +val f_is_neg_inf_Q : bits(128) -> bool +function f_is_neg_inf_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == 0b1) + & (exp == ones()) + & (mant == zeros())) +} + +val f_is_neg_norm_Q : bits(128) -> bool +function f_is_neg_norm_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == 0b1) + & (exp != zeros()) + & (exp != ones())) +} + +val f_is_neg_subnorm_Q : bits(128) -> bool +function f_is_neg_subnorm_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == 0b1) + & (exp == zeros()) + & (mant != zeros())) +} + +val f_is_neg_zero_Q : bits(128) -> bool +function f_is_neg_zero_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == ones()) + & (exp == zeros()) + & (mant == zeros())) +} + +val f_is_pos_zero_Q : bits(128) -> bool +function f_is_pos_zero_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == zeros()) + & (exp == zeros()) + & (mant == zeros())) +} + +val f_is_pos_subnorm_Q : bits(128) -> bool +function f_is_pos_subnorm_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == zeros()) + & (exp == zeros()) + & (mant != zeros())) +} + +val f_is_pos_norm_Q : bits(128) -> bool +function f_is_pos_norm_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == zeros()) + & (exp != zeros()) + & (exp != ones())) +} + +val f_is_pos_inf_Q : bits(128) -> bool +function f_is_pos_inf_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (sign == zeros()) + & (exp == ones()) + & (mant == zeros())) +} + +val f_is_SNaN_Q : bits(128) -> bool +function f_is_SNaN_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (exp == ones()) + & (mant [51] == bitzero) + & (mant != zeros())) +} + +val f_is_QNaN_Q : bits(128) -> bool +function f_is_QNaN_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (exp == ones()) + & (mant [51] == bitone)) +} + +/* Either QNaN or SNan */ +val f_is_NaN_Q : bits(128) -> bool +function f_is_NaN_Q x128 = { + let (sign, exp, mant) = fsplit_Q (x128); + ( (exp == ones()) + & (mant != zeros())) +} + + +/* **************************************************************** */ +/* Help functions used in the semantic functions */ + +val negate_Q : bits(128) -> bits(128) +function negate_Q (x128) = { + let (sign, exp, mant) = fsplit_Q (x128); + let new_sign = if (sign == 0b0) then 0b1 else 0b0; + fmake_Q (new_sign, exp, mant) +} + +val feq_quiet_Q : (bits(128), bits (128)) -> (bool, bits(5)) +function feq_quiet_Q (v1, v2) = { + let (s1, e1, m1) = fsplit_Q (v1); + let (s2, e2, m2) = fsplit_Q (v2); + + let v1Is0 = f_is_neg_zero_Q(v1) | f_is_pos_zero_Q(v1); + let v2Is0 = f_is_neg_zero_Q(v2) | f_is_pos_zero_Q(v2); + + let result = ((v1 == v2) | (v1Is0 & v2Is0)); + + let fflags = if (f_is_SNaN_Q(v1) | f_is_SNaN_Q(v2)) + then nvFlag() + else zeros(); + + (result, fflags) +} + +val flt_Q : (bits(128), bits (128), bool) -> (bool, bits(5)) +function flt_Q (v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit_Q (v1); + let (s2, e2, m2) = fsplit_Q (v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) + then unsigned (m1) < unsigned (m2) + else unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) then + false + else if (s1 == 0b1) & (s2 == 0b0) then + true + else + if (e1 == e2) + then unsigned (m1) > unsigned (m2) + else unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN_Q(v1) | f_is_SNaN_Q(v2)) + then nvFlag() + else zeros() + else + if (f_is_NaN_Q(v1) | f_is_NaN_Q(v2)) + then nvFlag() + else zeros(); + + (result, fflags) +} + +val fle_Q : (bits(128), bits (128), bool) -> (bool, bits(5)) +function fle_Q (v1, v2, is_quiet) = { + let (s1, e1, m1) = fsplit_Q (v1); + let (s2, e2, m2) = fsplit_Q (v2); + + let v1Is0 = f_is_neg_zero_Q(v1) | f_is_pos_zero_Q(v1); + let v2Is0 = f_is_neg_zero_Q(v2) | f_is_pos_zero_Q(v2); + + let result : bool = + if (s1 == 0b0) & (s2 == 0b0) then + if (e1 == e2) + then unsigned (m1) <= unsigned (m2) + else unsigned (e1) < unsigned (e2) + else if (s1 == 0b0) & (s2 == 0b1) then + (v1Is0 & v2Is0) /* Equal in this case (+0=-0) */ + else if (s1 == 0b1) & (s2 == 0b0) then + true + else + if (e1 == e2) + then unsigned (m1) >= unsigned (m2) + else unsigned (e1) > unsigned (e2); + + let fflags = if is_quiet then + if (f_is_SNaN_Q(v1) | f_is_SNaN_Q(v2)) + then nvFlag() + else zeros() + else + if (f_is_NaN_Q(v1) | f_is_NaN_Q(v2)) + then nvFlag() + else zeros(); + + (result, fflags) +} + +/* ****************************************************************** */ +/* Floating-point loads */ +/* These are defined in: riscv_insts_fext.sail */ + +/* ****************************************************************** */ +/* Floating-point stores */ +/* These are defined in: riscv_insts_fext.sail */ + +/* ****************************************************************** */ +/* Fused multiply-add */ + +/* AST */ + +union clause ast = F_MADD_TYPE_Q : (regidx, regidx, regidx, rounding_mode, regidx, f_madd_op_Q) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FMADD_Q) if extensionEnabled(Ext_Q) +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FMSUB_Q) if extensionEnabled(Ext_Q) +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_0111 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FNMSUB_Q) if extensionEnabled(Ext_Q) +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, FNMADD_Q) if extensionEnabled(Ext_Q) +<-> rs3 @ 0b11 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b100_1111 if extensionEnabled(Ext_Q) + +/* Execution semantics ================================ */ + +function clause execute (F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, op)) = { + let rs1_val_128b = F_Q(rs1); + let rs2_val_128b = F_Q(rs2); + let rs3_val_128b = F_Q(rs3); + + 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_128b) : (bits(5), bits(128)) = + match op { + FMADD_Q => riscv_f128MulAdd (rm_3b, rs1_val_128b, rs2_val_128b, rs3_val_128b), + FMSUB_Q => riscv_f128MulAdd (rm_3b, rs1_val_128b, rs2_val_128b, negate_Q (rs3_val_128b)), + FNMSUB_Q => riscv_f128MulAdd (rm_3b, negate_Q (rs1_val_128b), rs2_val_128b, rs3_val_128b), + FNMADD_Q => riscv_f128MulAdd (rm_3b, negate_Q (rs1_val_128b), rs2_val_128b, negate_Q (rs3_val_128b)) + }; + accrue_fflags(fflags); + F_Q(rd) = rd_val_128b; + RETIRE_SUCCESS + } + } +} + +/* AST -> Assembly notation ================================ */ + +mapping f_madd_type_mnemonic_Q : f_madd_op_Q <-> string = { + FMADD_Q <-> "fmadd.q", + FMSUB_Q <-> "fmsub.q", + FNMSUB_Q <-> "fnmsub.q", + FNMADD_Q <-> "fnmadd.q" +} + +mapping clause assembly = F_MADD_TYPE_Q(rs3, rs2, rs1, rm, rd, op) + <-> f_madd_type_mnemonic_Q(op) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + ^ sep() ^ freg_or_reg_name(rs3) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Binary ops with rounding mode */ + +/* AST */ + +union clause ast = F_BIN_RM_TYPE_Q : (regidx, regidx, rounding_mode, regidx, f_bin_rm_op_Q) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, FADD_Q) if extensionEnabled(Ext_Q) +<-> 0b000_0011 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, FSUB_Q) if extensionEnabled(Ext_Q) +<-> 0b000_0111 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, FMUL_Q) if extensionEnabled(Ext_Q) +<-> 0b000_1011 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, FDIV_Q) if extensionEnabled(Ext_Q) +<-> 0b000_1111 @ rs2 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +/* Execution semantics ================================ */ + +function clause execute (F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, op)) = { + let rs1_val_128b = F_Q(rs1); + let rs2_val_128b = F_Q(rs2); + 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_128b) : (bits(5), bits(128)) = match op { + FADD_Q => riscv_f128Add (rm_3b, rs1_val_128b, rs2_val_128b), + FSUB_Q => riscv_f128Sub (rm_3b, rs1_val_128b, rs2_val_128b), + FMUL_Q => riscv_f128Mul (rm_3b, rs1_val_128b, rs2_val_128b), + FDIV_Q => riscv_f128Div (rm_3b, rs1_val_128b, rs2_val_128b) + }; + accrue_fflags(fflags); + F_Q(rd) = rd_val_128b; + RETIRE_SUCCESS + } + } +} + +/* AST -> Assembly notation ================================ */ + +mapping f_bin_rm_type_mnemonic_Q : f_bin_rm_op_Q <-> string = { + FADD_Q <-> "fadd.q", + FSUB_Q <-> "fsub.q", + FMUL_Q <-> "fmul.q", + FDIV_Q <-> "fdiv.q" +} + +mapping clause assembly = F_BIN_RM_TYPE_Q(rs2, rs1, rm, rd, op) + <-> f_bin_rm_type_mnemonic_Q(op) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Unary with rounding mode */ + +/* AST */ + +union clause ast = F_UN_RM_TYPE_Q : (regidx, rounding_mode, regidx, f_un_rm_op_Q) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FSQRT_Q) if extensionEnabled(Ext_Q) +<-> 0b010_1111 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_W_Q) if extensionEnabled(Ext_Q) +<-> 0b110_0011 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_WU_Q) if extensionEnabled(Ext_Q) +<-> 0b110_0011 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_W) if extensionEnabled(Ext_Q) +<-> 0b110_1011 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_WU) if extensionEnabled(Ext_Q) +<-> 0b110_1011 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_S_Q) if extensionEnabled(Ext_Q) +<-> 0b010_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_S) if extensionEnabled(Ext_Q) +<-> 0b010_0011 @ 0b00000 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_D_Q) if extensionEnabled(Ext_Q) +<-> 0b010_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D) if extensionEnabled(Ext_Q) +<-> 0b010_0011 @ 0b00001 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +/* Q instructions, RV64 only */ + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_L_Q) if extensionEnabled(Ext_Q) +<-> 0b110_0011 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_LU_Q) if extensionEnabled(Ext_Q) +<-> 0b110_0011 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_L) if extensionEnabled(Ext_Q) +<-> 0b110_1011 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = + F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_LU) if extensionEnabled(Ext_Q) +<-> 0b110_1011 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +/* Execution semantics ================================ */ + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FSQRT_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_Q) = riscv_f128Sqrt (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_W_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_W) = riscv_f128ToI32 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + X(rd) = sign_extend (rd_val_W); + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_WU_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_WU) = riscv_f128ToUi32 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + X(rd) = sign_extend (rd_val_WU); + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_W)) = { + let rs1_val_W = X(rs1) [31..0]; + 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_i32ToF128 (rm_3b, rs1_val_W); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_WU)) = { + let rs1_val_WU = X(rs1) [31..0]; + 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_ui32ToF128 (rm_3b, rs1_val_WU); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_S_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_S) = riscv_f128ToF32 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + 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_S(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_f32ToF128 (rm_3b, rs1_val_S); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_D_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_D) = riscv_f128ToF64 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + 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_D(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_f64ToF128 (rm_3b, rs1_val_D); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_L_Q)) = { + assert(sizeof(xlen) >= 64); + 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_L) = riscv_f128ToI64 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + X(rd) = sign_extend(rd_val_L); + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_LU_Q)) = { + assert(sizeof(xlen) >= 64); + 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_LU) = riscv_f128ToUi64 (rm_3b, rs1_val_Q); + + accrue_fflags(fflags); + X(rd) = sign_extend(rd_val_LU); + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_L)) = { + assert(sizeof(xlen) >= 64); + let rs1_val_L = X(rs1)[63..0]; + 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_i64ToF128 (rm_3b, rs1_val_L); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +function clause execute (F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_LU)) = { + assert(sizeof(xlen) >= 64); + let rs1_val_LU = X(rs1)[63..0]; + 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_ui64ToF128 (rm_3b, rs1_val_LU); + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS + } + } +} + +/* AST -> Assembly notation ================================ */ + +mapping f_un_rm_type_mnemonic_Q : f_un_rm_op_Q <-> string = { + FSQRT_Q <-> "fsqrt.q", + FCVT_W_Q <-> "fcvt.w.q", + FCVT_WU_Q <-> "fcvt.wu.q", + FCVT_Q_W <-> "fcvt.q.w", + FCVT_Q_WU <-> "fcvt.q.wu", + + FCVT_L_Q <-> "fcvt.l.q", + FCVT_LU_Q <-> "fcvt.lu.q", + FCVT_Q_L <-> "fcvt.q.l", + FCVT_Q_LU <-> "fcvt.q.lu", + + FCVT_S_Q <-> "fcvt.s.q", + FCVT_Q_S <-> "fcvt.q.s", + FCVT_D_Q <-> "fcvt.d.q", + FCVT_Q_D <-> "fcvt.q.d" +} + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FSQRT_Q) + <-> f_un_rm_type_mnemonic_Q(FSQRT_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_W_Q) + <-> f_un_rm_type_mnemonic_Q(FCVT_W_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_WU_Q) + <-> f_un_rm_type_mnemonic_Q(FCVT_WU_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_W) + <-> f_un_rm_type_mnemonic_Q(FCVT_Q_W) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_WU) + <-> f_un_rm_type_mnemonic_Q(FCVT_Q_WU) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_L_Q) + <-> f_un_rm_type_mnemonic_Q(FCVT_L_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_LU_Q) + <-> f_un_rm_type_mnemonic_Q(FCVT_LU_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_L) + <-> f_un_rm_type_mnemonic_Q(FCVT_Q_L) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_LU) + <-> f_un_rm_type_mnemonic_Q(FCVT_Q_LU) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_S_Q) + <-> f_un_rm_type_mnemonic_Q(FCVT_S_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_S) + <-> f_un_rm_type_mnemonic_Q(FCVT_Q_S) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_D_Q) + <-> f_un_rm_type_mnemonic_Q(FCVT_D_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +mapping clause assembly = F_UN_RM_TYPE_Q(rs1, rm, rd, FCVT_Q_D) + <-> f_un_rm_type_mnemonic_Q(FCVT_Q_D) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ frm_mnemonic(rm) + +/* ****************************************************************** */ +/* Binary, no rounding mode */ + +/* AST */ + +union clause ast = F_BIN_TYPE_Q : (regidx, regidx, regidx, f_bin_op_Q) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJ_Q) if extensionEnabled(Ext_Q) + <-> 0b001_0011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJN_Q) if extensionEnabled(Ext_Q) + <-> 0b001_0011 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJX_Q) if extensionEnabled(Ext_Q) + <-> 0b001_0011 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q) if extensionEnabled(Ext_Q) + <-> 0b001_0111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q) if extensionEnabled(Ext_Q) + <-> 0b001_0111 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D) if extensionEnabled(Ext_Q) + <-> 0b101_0011 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLT_D) if extensionEnabled(Ext_Q) + <-> 0b101_0011 @ rs2 @ rs1 @ 0b001 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if extensionEnabled(Ext_Q) + <-> 0b101_0011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +/* Execution semantics ================================ */ + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJ_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (s1, e1, m1) = fsplit_Q (rs1_val_Q); + let (s2, e2, m2) = fsplit_Q (rs2_val_Q); + let rd_val_Q = fmake_Q (s2, e1, m1); + + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJN_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + let (s1, e1, m1) = fsplit_Q (rs1_val_Q); + let (s2, e2, m2) = fsplit_Q (rs2_val_Q); + let rd_val_Q = fmake_Q (0b1 ^ s2, e1, m1); + + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJX_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + let (s1, e1, m1) = fsplit_Q (rs1_val_Q); + let (s2, e2, m2) = fsplit_Q (rs2_val_Q); + let rd_val_Q = fmake_Q (s1 ^ s2, e1, m1); + + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q)) = { + 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_NaN_Q(rs1_val_Q) then rs2_val_Q + else if f_is_NaN_Q(rs2_val_Q) then rs1_val_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 /* (not rs1_lt_rs2) */ rs2_val_Q; + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q)) = { + 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_NaN_Q(rs1_val_Q) then rs2_val_Q + else if f_is_NaN_Q(rs2_val_Q) then rs1_val_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 /* (not rs2_lt_rs1) */ rs2_val_Q; + + accrue_fflags(fflags); + F_Q(rd) = rd_val_Q; + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FEQ_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Eq (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FLT_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Lt (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +function clause execute (F_BIN_TYPE_Q(rs2, rs1, rd, FLE_Q)) = { + let rs1_val_Q = F_Q(rs1); + let rs2_val_Q = F_Q(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f128Le (rs1_val_Q, rs2_val_Q); + + accrue_fflags(fflags); + X(rd) = zero_extend(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_bin_type_mnemonic_Q : f_bin_op_Q <-> string = { + FSGNJ_Q <-> "fsgnj.q", + FSGNJN_Q <-> "fsgnjn.q", + FSGNJX_Q <-> "fsgnjx.q", + FMIN_Q <-> "fmin.q", + FMAX_Q <-> "fmax.q", + FEQ_Q <-> "feq.q", + FLT_Q <-> "flt.q", + FLE_Q <-> "fle.q" +} + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJ_Q) + <-> f_bin_type_mnemonic_Q(FSGNJ_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJN_Q) + <-> f_bin_type_mnemonic_Q(FSGNJN_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FSGNJX_Q) + <-> f_bin_type_mnemonic_Q(FSGNJX_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FMIN_Q) + <-> f_bin_type_mnemonic_Q(FMIN_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FMAX_Q) + <-> f_bin_type_mnemonic_Q(FMAX_Q) + ^ spc() ^ freg_or_reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FEQ_Q) + <-> f_bin_type_mnemonic_Q(FEQ_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FLT_Q) + <-> f_bin_type_mnemonic_Q(FLT_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +mapping clause assembly = F_BIN_TYPE_Q(rs2, rs1, rd, FLE_Q) + <-> f_bin_type_mnemonic_Q(FLE_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + ^ sep() ^ freg_or_reg_name(rs2) + +/* ****************************************************************** */ +/* Unary, no rounding mode */ + +union clause ast = F_UN_TYPE_Q : (regidx, regidx, f_un_op_Q) + +/* AST <-> Binary encoding ================================ */ + +mapping clause encdec = F_UN_TYPE_Q(rs1, rd, FCLASS_Q) if extensionEnabled(Ext_Q) + <-> 0b111_0011 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) + +/* FMV Q instructions are RV128 only */ + +/* Execution semantics ================================ */ + +function clause execute (F_UN_TYPE_Q(rs1, rd, FCLASS_Q)) = { + let rs1_val_Q = F_Q(rs1); + + let rd_val_10b : bits (10) = + if f_is_neg_inf_Q (rs1_val_Q) then 0b_00_0000_0001 + else if f_is_neg_norm_Q (rs1_val_Q) then 0b_00_0000_0010 + else if f_is_neg_subnorm_Q (rs1_val_Q) then 0b_00_0000_0100 + else if f_is_neg_zero_Q (rs1_val_Q) then 0b_00_0000_1000 + else if f_is_pos_zero_Q (rs1_val_Q) then 0b_00_0001_0000 + else if f_is_pos_subnorm_Q (rs1_val_Q) then 0b_00_0010_0000 + else if f_is_pos_norm_Q (rs1_val_Q) then 0b_00_0100_0000 + else if f_is_pos_inf_Q (rs1_val_Q) then 0b_00_1000_0000 + else if f_is_SNaN_Q (rs1_val_Q) then 0b_01_0000_0000 + else if f_is_QNaN_Q (rs1_val_Q) then 0b_10_0000_0000 + else zeros(); + + X(rd) = zero_extend (rd_val_10b); + RETIRE_SUCCESS +} + +/* AST -> Assembly notation ================================ */ + +mapping f_un_type_mnemonic_Q : f_un_op_Q <-> string = { + FCLASS_Q <-> "fclass.d" + } + +mapping clause assembly = F_UN_TYPE_Q(rs1, rd, FCLASS_Q) + <-> f_un_type_mnemonic_Q(FCLASS_Q) + ^ spc() ^ reg_name(rd) + ^ sep() ^ freg_or_reg_name(rs1) + +/* ****************************************************************** */ diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 2b1f7c50f..d3c5b74a2 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -156,6 +156,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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b111_1011 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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) @@ -336,6 +385,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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b001_0111 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b001_0111 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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) @@ -504,6 +613,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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b010_0011 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b010_0011 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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) @@ -549,6 +714,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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) & in64BitMode() + <-> 0b111_0011 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) & 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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) & in64BitMode() + <-> 0b101_1011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) & 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) @@ -694,6 +906,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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b101_0011 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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 extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + <-> 0b101_0011 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if extensionEnabled(Ext_Q) & extensionEnabled(Ext_Zfa) + +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 5e55fb8a2..cb0abc221 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -19,9 +19,9 @@ function clause extensionEnabled(Ext_Zhinx) = sys_enable_zfinx() /* **************************************************************** */ /* IMPORTANT! */ -/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail' and */ -/* 'riscv_insts_zfh.sail' define the F, D and Zfh extensions, */ -/* respectively. */ +/* The files 'riscv_insts_fext.sail', 'riscv_insts_dext.sail', */ +/* 'riscv_insts_qext.sail' and 'riscv_insts_zfh.sail' define the */ +/* F, D, Q and Zfh extensions, respectively. */ /* The texts follow each other very closely; please try to maintain */ /* this correspondence as the files are maintained for bug-fixes, */ /* improvements, and version updates. */ @@ -545,6 +545,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() @@ -553,8 +557,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 */ @@ -681,6 +686,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)) { @@ -696,7 +716,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)) { @@ -712,6 +731,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); @@ -787,8 +821,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", @@ -862,6 +898,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) @@ -874,6 +916,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 fdf84dbf3..413b99d6d 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -8,7 +8,7 @@ /* **************************************************************** */ /* This file lists all the external Berkeley softfloat functions */ -/* invoked from the SAIL spec for RISC-V F and D extensions */ +/* invoked from the SAIL spec for RISC-V F, D and Q extensions */ /* (in: riscv_insts_fdext.sail) */ /* */ /* Each of these functions corresponds to one in 'SoftFloat.hs' */ @@ -30,6 +30,9 @@ type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */ 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,6 +45,7 @@ type bits_LU = bits(64) /* Unsigned integer */ * to avoid return types involving structures. */ register float_result : bits(64) +register float_result_high : bits(64) register float_fflags : bits(64) /* **************************************************************** */ @@ -131,6 +135,33 @@ function riscv_f64Div (rm, v1, v2) = { (float_fflags[4 .. 0], float_result) } +val extern_f128Add = pure {c: "softfloat_f128add", 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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) +} + +val extern_f128Sub = pure {c: "softfloat_f128sub", 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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) +} + +val extern_f128Mul = pure {c: "softfloat_f128mul", 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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) +} + +val extern_f128Div = pure {c: "softfloat_f128div", 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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) +} /* **************************************************************** */ /* MULTIPLY-ADD */ @@ -155,6 +186,14 @@ function riscv_f64MulAdd (rm, v1, v2, v3) = { (float_fflags[4 .. 0], float_result) } +val extern_f128MulAdd = pure {c: "softfloat_f128muladd", 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[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) +} + + /* **************************************************************** */ /* SQUARE ROOT */ @@ -179,6 +218,14 @@ function riscv_f64Sqrt (rm, v) = { (float_fflags[4 .. 0], float_result) } +val extern_f128Sqrt = pure {c: "softfloat_f128sqrt", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result_high @ float_result) + +} + /* **************************************************************** */ /* CONVERSIONS */ @@ -351,6 +398,62 @@ function riscv_ui64ToF64 (rm, v) = { (float_fflags[4 .. 0], float_result) } +val extern_f128ToI32 = pure {c: "softfloat_f128toi32", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result[31..0]) +} + +val extern_f128ToUi32 = pure {c: "softfloat_f128toui32", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result[31..0]) +} + +val extern_i32ToF128 = pure {c: "softfloat_i32tof128", lem: "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_high @ float_result) +} + +val extern_ui32ToF128 = pure {c: "softfloat_ui32tof128", 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_high @ float_result) +} + +val extern_f128ToI64 = pure {c: "softfloat_f128toi64", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result) +} + +val extern_f128ToUi64 = pure {c: "softfloat_f128toui64", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result) +} + +val extern_i64ToF128 = pure {c: "softfloat_i64tof128", 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_high @ float_result) +} + +val extern_ui64ToF128 = pure {c: "softfloat_ui64tof128", 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_high @ float_result) +} + val extern_f16ToF32 = pure {c: "softfloat_f16tof32", 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) = { @@ -365,11 +468,11 @@ function riscv_f16ToF64 (rm, v) = { (float_fflags[4 .. 0], float_result) } -val extern_f32ToF64 = pure {c: "softfloat_f32tof64", 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) +val extern_f16ToF128 = pure {c: "softfloat_f16tof128", 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_high @ float_result) } val extern_f32ToF16 = pure {c: "softfloat_f32tof16", lem: "softfloat_f32_to_f16"} : (bits_rm, bits_S) -> unit @@ -379,6 +482,20 @@ function riscv_f32ToF16 (rm, v) = { (float_fflags[4 .. 0], float_result[15 .. 0]) } +val extern_f32ToF64 = pure {c: "softfloat_f32tof64", 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) +} + +val extern_f32ToF128 = pure {c: "softfloat_f32tof128", 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_high @ float_result) +} + val extern_f64ToF16 = pure {c: "softfloat_f64tof16", 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) = { @@ -393,6 +510,34 @@ function riscv_f64ToF32 (rm, v) = { (float_fflags[4 .. 0], float_result[31 .. 0]) } +val extern_f64ToF128 = pure {c: "softfloat_f64tof128", lem: "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_high @ float_result) +} + +val extern_f128ToF16 = pure {c: "softfloat_f128tof16", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result[15..0]) +} + +val extern_f128ToF32 = pure {c: "softfloat_f128tof32", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result[31..0]) +} + +val extern_f128ToF64 = pure {c: "softfloat_f128tof64", 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[63..0], v[127..64]); + (float_fflags[4 .. 0], float_result) +} + /* **************************************************************** */ /* COMPARISONS */ @@ -501,6 +646,41 @@ function riscv_f64Eq (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f128Lt = pure {c: "softfloat_f128lt", 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[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 = pure {c: "softfloat_f128lt_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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + +val extern_f128Le = pure {c: "softfloat_f128le", 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[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 = pure {c: "softfloat_f128le_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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + +val extern_f128Eq = pure {c: "softfloat_f128eq", 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[63..0], v1[127..64], v2[63..0], v2[127..64]); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f16roundToInt = pure {c: "softfloat_f16roundToInt", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) function riscv_f16roundToInt (rm, v, exact) = { @@ -519,6 +699,13 @@ val extern_f64roundToInt = pure {c: "softfloat_f64roundToInt", lem: "softflo val riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) function riscv_f64roundToInt (rm, v, exact) = { extern_f64roundToInt(rm, v, exact); - (float_fflags[4 .. 0], float_result) + (float_fflags[4 .. 0], float_result[63 .. 0]) +} + +val extern_f128roundToInt = pure {c: "softfloat_f128roundToInt", 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[63..0], v[127..64], exact); + (float_fflags[4 .. 0], float_result_high @ float_result) } /* **************************************************************** */ diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6e8832738..7b23161ca 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -506,11 +506,10 @@ function init_sys() -> unit = { if sys_enable_fdext() & sys_enable_zfinx() then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!"); - /* We currently support both F and D */ - misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */ - misa[D] = if sizeof(flen) >= 64 - then bool_to_bits(sys_enable_fdext()) /* double-precision */ - else 0b0; + /* We currently support F, D and Q */ + misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */ + misa[D] = bool_to_bits(sys_enable_fdext() & sizeof(flen) >= 64); /* double-precision */ + misa[Q] = bool_to_bits(sys_enable_fdext() & sizeof(flen) >= 128); /* quad-precision */ mstatus = set_mstatus_SXL(mstatus, misa[MXL]); mstatus = set_mstatus_UXL(mstatus, misa[MXL]); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 1f34d2d3a..509d3d0c1 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -302,6 +302,10 @@ function in32BitMode() -> bool = { cur_Architecture() == RV32 } +function in64BitMode() -> bool = { + cur_Architecture() == RV64 +} + /* interrupt processing state */ bitfield Minterrupts : xlenbits = { diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 94c57a34e..9da68a0c9 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -144,7 +144,7 @@ union AccessType ('a : Type) = { Execute : unit } -enum word_width = {BYTE, HALF, WORD, DOUBLE} +enum word_width = {BYTE, HALF, WORD, DOUBLE, QUAD} /* architectural interrupt definitions */ @@ -369,26 +369,37 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH} enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ} -// Get the bit encoding of word_width. +// Get the short bit encoding of word_width for use with signed expressions. mapping size_enc : word_width <-> bits(2) = { BYTE <-> 0b00, HALF <-> 0b01, WORD <-> 0b10, - DOUBLE <-> 0b11 + DOUBLE <-> 0b11, +} + +// Get the full bit encoding of word_width. +mapping size_enc_wide : word_width <-> bits(3) = { + QUAD <-> 0b100, + BYTE <-> 0b0 @ size_enc(BYTE), + HALF <-> 0b0 @ size_enc(HALF), + WORD <-> 0b0 @ size_enc(WORD), + DOUBLE <-> 0b0 @ size_enc(DOUBLE), } mapping size_mnemonic : word_width <-> string = { BYTE <-> "b", HALF <-> "h", WORD <-> "w", - DOUBLE <-> "d" + DOUBLE <-> "d", + QUAD <-> "q", } -mapping size_bytes : word_width <-> {1, 2, 4, 8} = { +mapping size_bytes : word_width <-> {1, 2, 4, 8, 16} = { BYTE <-> 1, HALF <-> 2, WORD <-> 4, DOUBLE <-> 8, + QUAD <-> 16, } struct mul_op = {