From f2d8e1b959def0f08af45a39c9c675f62f35db85 Mon Sep 17 00:00:00 2001 From: Philipp Tomsich Date: Thu, 16 Feb 2023 12:49:01 +0100 Subject: [PATCH] Add Zfa extension support (excl. quad-precision) This commit adds the following: - infrastructure for Zfa (e.g., existence macro) - support for the following instructions: + FLI.[HSD] + FMINM.[HSD] and FMAXM.[HSD] + FROUND.[HSD] and FROUNDNX.[HSD] + FMVH.X.D and FMVP.D.X + FLEQ.[HSD] and FLTQ.[HSD] + FCVTMOD.W.D Note the following implementation details: FMINM and FMAXM provide similar functionality to FMIN and FMAX, differing only in their NaN-handling: * FMIN/FMAX return a canonical NaN only if both operands are a NaN * FMINM/FMAXM return a canonical Nan if any operand is a NaN Consequently, the implementation is identical to FMIN/FMAX with only the NaN-related tests changed. FROUND instruction rounds a floating-point number in floating-point register rs1 and writes that integer, represented as a floating-point number to floating-point register rd while: * Zero and infinite inputs are copied to rd unmodified. * NaN inputs cause the invalid operation exception flag to be set. FROUNDNX instruction is defined similarly, but also sets the inexact exception flag if the input differs from the rounded result and is not NaN. FMVH.X.D instruction is available for RV32 only and moves bits 63:32 of floating-point register rs1 into integer register rd. FMVP.D.X instruction is available for RV32 only and moves a double-precision number from a pair of integer registers into a floating-point register. Integer registers rs1 and rs2 supply bits 31:0 and 63:32, respectively. FLEQ and FLTQ instructions are defined like the FLE and FLT instructions, except that quiet NaN inputs do not cause the invalid operation exception flag to be set. The FCVTMOD.W.D instruction is defined similarly to the FCVT.W.D instruction, with the following differences: * FCVTMOD.W.D always rounds towards zero. * Bits 31:0 are taken from the rounded, unbounded two's complement result, then sign-extended to XLEN bits and written to integer register rd. * Positive infinity, negative infinity and NaN are converted to zero. Signed-off-by: Charalampos Mitrodimas Signed-off-by: Philipp Tomsich --- Makefile | 3 + c_emulator/riscv_softfloat.c | 118 +++ c_emulator/riscv_softfloat.h | 10 + .../0.11/riscv_extras_fdext.lem | 27 + model/riscv_fdext_regs.sail | 58 +- model/riscv_insts_zfa.sail | 764 ++++++++++++++++++ model/riscv_softfloat_interface.sail | 63 ++ model/riscv_sys_regs.sail | 3 + ocaml_emulator/softfloat.ml | 27 + 9 files changed, 1067 insertions(+), 6 deletions(-) create mode 100644 model/riscv_insts_zfa.sail diff --git a/Makefile b/Makefile index 5365f046e..17b8a0a62 100644 --- a/Makefile +++ b/Makefile @@ -29,6 +29,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbc.sail SAIL_DEFAULT_INST += riscv_insts_zbs.sail SAIL_DEFAULT_INST += riscv_insts_zfh.sail +# Zfa needs to be added after fext, dext and Zfh (as it needs +# definitions from those) +SAIL_DEFAULT_INST += riscv_insts_zfa.sail SAIL_DEFAULT_INST += riscv_insts_zkn.sail SAIL_DEFAULT_INST += riscv_insts_zks.sail diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c index b3819b6a3..5fc178716 100644 --- a/c_emulator/riscv_softfloat.c +++ b/c_emulator/riscv_softfloat.c @@ -641,6 +641,19 @@ unit softfloat_f16lt(mach_bits v1, mach_bits v2) { return UNIT; } +unit softfloat_f16lt_quiet(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float16_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f16_lt_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f16le(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -654,6 +667,19 @@ unit softfloat_f16le(mach_bits v1, mach_bits v2) { return UNIT; } +unit softfloat_f16le_quiet(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float16_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f16_le_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f16eq(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -680,6 +706,19 @@ unit softfloat_f32lt(mach_bits v1, mach_bits v2) { return UNIT; } +unit softfloat_f32lt_quiet(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f32_lt_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f32le(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -693,6 +732,20 @@ unit softfloat_f32le(mach_bits v1, mach_bits v2) { return UNIT; } + +unit softfloat_f32le_quiet(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float32_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f32_le_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f32eq(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -719,6 +772,19 @@ unit softfloat_f64lt(mach_bits v1, mach_bits v2) { return UNIT; } +unit softfloat_f64lt_quiet(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f64_lt_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f64le(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -732,6 +798,19 @@ unit softfloat_f64le(mach_bits v1, mach_bits v2) { return UNIT; } +unit softfloat_f64le_quiet(mach_bits v1, mach_bits v2) { + SOFTFLOAT_PRELUDE(0); + + float64_t a, b, res; + a.v = v1; + b.v = v2; + res.v = f64_le_quiet(a, b); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + unit softfloat_f64eq(mach_bits v1, mach_bits v2) { SOFTFLOAT_PRELUDE(0); @@ -744,3 +823,42 @@ unit softfloat_f64eq(mach_bits v1, mach_bits v2) { return UNIT; } + +unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact) { + SOFTFLOAT_PRELUDE(rm); + + float16_t a, res; + uint_fast8_t rm8 = uint8_of_rm(rm); + a.v = v; + res = f16_roundToInt(a, rm8, exact); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact) { + SOFTFLOAT_PRELUDE(rm); + + float32_t a, res; + uint_fast8_t rm8 = uint8_of_rm(rm); + a.v = v; + res = f32_roundToInt(a, rm8, exact); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} + +unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact) { + SOFTFLOAT_PRELUDE(rm); + + float64_t a, res; + uint_fast8_t rm8 = uint8_of_rm(rm); + a.v = v; + res = f64_roundToInt(a, rm8, exact); + + SOFTFLOAT_POSTLUDE(res); + + return UNIT; +} diff --git a/c_emulator/riscv_softfloat.h b/c_emulator/riscv_softfloat.h index bd29d7f76..745a13a47 100644 --- a/c_emulator/riscv_softfloat.h +++ b/c_emulator/riscv_softfloat.h @@ -62,11 +62,21 @@ unit softfloat_f64tof16(mach_bits rm, mach_bits v); unit softfloat_f64tof32(mach_bits rm, mach_bits v); unit softfloat_f16lt(mach_bits v1, mach_bits v2); +unit softfloat_f16lt_quiet(mach_bits v1, mach_bits v2); unit softfloat_f16le(mach_bits v1, mach_bits v2); +unit softfloat_f16le_quiet(mach_bits v1, mach_bits v2); unit softfloat_f16eq(mach_bits v1, mach_bits v2); unit softfloat_f32lt(mach_bits v1, mach_bits v2); +unit softfloat_f32lt_quiet(mach_bits v1, mach_bits v2); unit softfloat_f32le(mach_bits v1, mach_bits v2); +unit softfloat_f32le_quiet(mach_bits v1, mach_bits v2); unit softfloat_f32eq(mach_bits v1, mach_bits v2); unit softfloat_f64lt(mach_bits v1, mach_bits v2); +unit softfloat_f64lt_quiet(mach_bits v1, mach_bits v2); unit softfloat_f64le(mach_bits v1, mach_bits v2); +unit softfloat_f64le_quiet(mach_bits v1, mach_bits v2); unit softfloat_f64eq(mach_bits v1, mach_bits v2); + +unit softfloat_f16roundToInt(mach_bits rm, mach_bits v, bool exact); +unit softfloat_f32roundToInt(mach_bits rm, mach_bits v, bool exact); +unit softfloat_f64roundToInt(mach_bits rm, mach_bits v, bool exact); diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem index 04b4d7e54..e24a63d6a 100644 --- a/handwritten_support/0.11/riscv_extras_fdext.lem +++ b/handwritten_support/0.11/riscv_extras_fdext.lem @@ -164,26 +164,53 @@ let softfloat_f64_to_f32 _ _ = () val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f16_lt _ _ = () +val softfloat_f16_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f16_lt_quiet _ _ = () + val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f16_le _ _ = () +val softfloat_f16_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f16_le_quiet _ _ = () + val softfloat_f16_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f16_eq _ _ = () val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f32_lt _ _ = () +val softfloat_f32_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_lt_quiet _ _ = () + val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f32_le _ _ = () +val softfloat_f32_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f32_le_quiet _ _ = () + val softfloat_f32_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f32_eq _ _ = () val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f64_lt _ _ = () +val softfloat_f64_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_lt_quiet _ _ = () + val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f64_le _ _ = () +val softfloat_f64_le_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit +let softfloat_f64_le_quiet _ _ = () + val softfloat_f64_eq : forall 's. Size 's => bitvector 's -> bitvector 's -> unit let softfloat_f64_eq _ _ = () + +val softfloat_f16_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit +let softfloat_f16_round_to_int _ _ _ = () + +val softfloat_f32_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit +let softfloat_f32_round_to_int _ _ _ = () + +val softfloat_f64_round_to_int : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bool -> unit +let softfloat_f64_round_to_int _ _ _ = () diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index e01a8053e..a5377b109 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -270,12 +270,58 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = { overload F = {rF_bits, wF_bits, rF, wF} +val rF_H : bits(5) -> bits(16) effect {escape, rreg} +function rF_H(i) = { + assert(sizeof(flen) >= 16); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + nan_unbox(F(i)) +} + +val wF_H : (bits(5), bits(16)) -> unit effect {escape, wreg} +function wF_H(i, data) = { + assert(sizeof(flen) >= 16); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) = nan_box(data) +} + +val rF_S : bits(5) -> bits(32) effect {escape, rreg} +function rF_S(i) = { + assert(sizeof(flen) >= 32); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + nan_unbox(F(i)) +} + +val wF_S : (bits(5), bits(32)) -> unit effect {escape, wreg} +function wF_S(i, data) = { + assert(sizeof(flen) >= 32); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) = nan_box(data) +} + +val rF_D : bits(5) -> bits(64) effect {escape, rreg} +function rF_D(i) = { + assert(sizeof(flen) >= 64); + assert(sys_enable_fdext() & not(sys_enable_zfinx())); + F(i) +} + +val wF_D : (bits(5), bits(64)) -> unit effect {escape, wreg} +function wF_D(i, data) = { + assert(sizeof(flen) >= 64); + 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 } + val rF_or_X_H : bits(5) -> bits(16) effect {escape, rreg} function rF_or_X_H(i) = { assert(sizeof(flen) >= 16); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() - then nan_unbox(F(i)) + then F_H(i) else X(i)[15..0] } @@ -284,7 +330,7 @@ function rF_or_X_S(i) = { assert(sizeof(flen) >= 32); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() - then nan_unbox(F(i)) + then F_S(i) else X(i)[31..0] } @@ -293,7 +339,7 @@ function rF_or_X_D(i) = { assert(sizeof(flen) >= 64); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() - then F(unsigned(i)) + then F_D(i) else if sizeof(xlen) >= 64 then X(i)[63..0] else { @@ -307,7 +353,7 @@ function wF_or_X_H(i, data) = { assert(sizeof(flen) >= 16); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() - then F(i) = nan_box(data) + then F_H(i) = data else X(i) = EXTS(data) } @@ -316,7 +362,7 @@ function wF_or_X_S(i, data) = { assert(sizeof(flen) >= 32); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() - then F(i) = nan_box(data) + then F_S(i) = data else X(i) = EXTS(data) } @@ -325,7 +371,7 @@ function wF_or_X_D(i, data) = { assert (sizeof(flen) >= 64); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() - then F(i) = data + then F_D(i) = data else if sizeof(xlen) >= 64 then X(i) = EXTS(data) else { diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail new file mode 100644 index 000000000..2b425dc8c --- /dev/null +++ b/model/riscv_insts_zfa.sail @@ -0,0 +1,764 @@ +/* FLI.H */ + +union clause ast = RISCV_FLI_H : (bits(5), regidx) + +mapping clause encdec = RISCV_FLI_H(rs1, rd) if haveZfh() & haveZfa() + <-> 0b111_1010 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FLI_H(constantidx, rd) + <-> "fli.h" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) + +function clause execute (RISCV_FLI_H(constantidx, rd)) = { + let bits : bits(16) = match constantidx { + 0b00000 => { 0xbc00 }, /* -1.0 */ + 0b00001 => { 0x0400 }, /* minimum positive normal */ + 0b00010 => { 0x0100 }, /* 1.0 * 2^-16 */ + 0b00011 => { 0x0200 }, /* 1.0 * 2^-15 */ + 0b00100 => { 0x1c00 }, /* 1.0 * 2^-8 */ + 0b00101 => { 0x2000 }, /* 1.0 * 2^-7 */ + 0b00110 => { 0x2c00 }, /* 1.0 * 2^-4 */ + 0b00111 => { 0x3000 }, /* 1.0 * 2^-3 */ + 0b01000 => { 0x3400 }, /* 0.25 */ + 0b01001 => { 0x3500 }, /* 0.3125 */ + 0b01010 => { 0x3600 }, /* 0.375 */ + 0b01011 => { 0x3700 }, /* 0.4375 */ + 0b01100 => { 0x3800 }, /* 0.5 */ + 0b01101 => { 0x3900 }, /* 0.625 */ + 0b01110 => { 0x3a00 }, /* 0.75 */ + 0b01111 => { 0x3b00 }, /* 0.875 */ + 0b10000 => { 0x3c00 }, /* 1.0 */ + 0b10001 => { 0x3d00 }, /* 1.25 */ + 0b10010 => { 0x3e00 }, /* 1.5 */ + 0b10011 => { 0x3f00 }, /* 1.75 */ + 0b10100 => { 0x4000 }, /* 2.0 */ + 0b10101 => { 0x4100 }, /* 2.5 */ + 0b10110 => { 0x4200 }, /* 3 */ + 0b10111 => { 0x4400 }, /* 4 */ + 0b11000 => { 0x4800 }, /* 8 */ + 0b11001 => { 0x4c00 }, /* 16 */ + 0b11010 => { 0x5800 }, /* 2^7 */ + 0b11011 => { 0x5c00 }, /* 2^8 */ + 0b11100 => { 0x7800 }, /* 2^15 */ + 0b11101 => { 0x7c00 }, /* 2^16 */ + 0b11110 => { 0x7c00 }, /* +inf */ + 0b11111 => { canonical_NaN_H() }, + }; + F_H(rd) = bits; + RETIRE_SUCCESS +} + +/* FLI.S */ + +union clause ast = RISCV_FLI_S : (bits(5), regidx) + +mapping clause encdec = RISCV_FLI_S(rs1, rd) if haveZfa() + <-> 0b111_1000 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FLI_S(constantidx, rd) + <-> "fli.s" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) + +function clause execute (RISCV_FLI_S(constantidx, rd)) = { + let bits : bits(32) = match constantidx { + 0b00000 => { 0xbf800000 }, /* -1.0 */ + 0b00001 => { 0x00800000 }, /* minimum positive normal */ + 0b00010 => { 0x37800000 }, /* 1.0 * 2^-16 */ + 0b00011 => { 0x38000000 }, /* 1.0 * 2^-15 */ + 0b00100 => { 0x3b800000 }, /* 1.0 * 2^-8 */ + 0b00101 => { 0x3c000000 }, /* 1.0 * 2^-7 */ + 0b00110 => { 0x3d800000 }, /* 1.0 * 2^-4 */ + 0b00111 => { 0x3e000000 }, /* 1.0 * 2^-3 */ + 0b01000 => { 0x3e800000 }, /* 0.25 */ + 0b01001 => { 0x3ea00000 }, /* 0.3125 */ + 0b01010 => { 0x3ec00000 }, /* 0.375 */ + 0b01011 => { 0x3ee00000 }, /* 0.4375 */ + 0b01100 => { 0x3f000000 }, /* 0.5 */ + 0b01101 => { 0x3f200000 }, /* 0.625 */ + 0b01110 => { 0x3f400000 }, /* 0.75 */ + 0b01111 => { 0x3f600000 }, /* 0.875 */ + 0b10000 => { 0x3f800000 }, /* 1.0 */ + 0b10001 => { 0x3fa00000 }, /* 1.25 */ + 0b10010 => { 0x3fc00000 }, /* 1.5 */ + 0b10011 => { 0x3fe00000 }, /* 1.75 */ + 0b10100 => { 0x40000000 }, /* 2.0 */ + 0b10101 => { 0x40200000 }, /* 2.5 */ + 0b10110 => { 0x40400000 }, /* 3 */ + 0b10111 => { 0x40800000 }, /* 4 */ + 0b11000 => { 0x41000000 }, /* 8 */ + 0b11001 => { 0x41800000 }, /* 16 */ + 0b11010 => { 0x43000000 }, /* 2^7 */ + 0b11011 => { 0x43800000 }, /* 2^8 */ + 0b11100 => { 0x47000000 }, /* 2^15 */ + 0b11101 => { 0x47800000 }, /* 2^16 */ + 0b11110 => { 0x7f800000 }, /* +inf */ + 0b11111 => { canonical_NaN_S() }, + }; + F_S(rd) = bits; + RETIRE_SUCCESS +} + +/* FLI.D */ + +union clause ast = RISCV_FLI_D : (bits(5), regidx) + +mapping clause encdec = RISCV_FLI_D(rs1, rd) if haveDExt() & haveZfa() + <-> 0b111_1001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FLI_D(constantidx, rd) + <-> "fli.d" ^ spc() ^ freg_name(rd) ^ sep() ^ hex_bits_5(constantidx) + +function clause execute (RISCV_FLI_D(constantidx, rd)) = { + let bits : bits(64) = match constantidx { + 0b00000 => { 0xbff0000000000000 }, /* -1.0 */ + 0b00001 => { 0x0010000000000000 }, /* minimum positive normal */ + 0b00010 => { 0x3Ef0000000000000 }, /* 1.0 * 2^-16 */ + 0b00011 => { 0x3f00000000000000 }, /* 1.0 * 2^-15 */ + 0b00100 => { 0x3f70000000000000 }, /* 1.0 * 2^-8 */ + 0b00101 => { 0x3f80000000000000 }, /* 1.0 * 2^-7 */ + 0b00110 => { 0x3fb0000000000000 }, /* 1.0 * 2^-4 */ + 0b00111 => { 0x3fc0000000000000 }, /* 1.0 * 2^-3 */ + 0b01000 => { 0x3fd0000000000000 }, /* 0.25 */ + 0b01001 => { 0x3fd4000000000000 }, /* 0.3125 */ + 0b01010 => { 0x3fd8000000000000 }, /* 0.375 */ + 0b01011 => { 0x3fdc000000000000 }, /* 0.4375 */ + 0b01100 => { 0x3fe0000000000000 }, /* 0.5 */ + 0b01101 => { 0x3fe4000000000000 }, /* 0.625 */ + 0b01110 => { 0x3fe8000000000000 }, /* 0.75 */ + 0b01111 => { 0x3fec000000000000 }, /* 0.875 */ + 0b10000 => { 0x3ff0000000000000 }, /* 1.0 */ + 0b10001 => { 0x3ff4000000000000 }, /* 1.25 */ + 0b10010 => { 0x3ff8000000000000 }, /* 1.5 */ + 0b10011 => { 0x3ffc000000000000 }, /* 1.75 */ + 0b10100 => { 0x4000000000000000 }, /* 2.0 */ + 0b10101 => { 0x4004000000000000 }, /* 2.5 */ + 0b10110 => { 0x4008000000000000 }, /* 3 */ + 0b10111 => { 0x4010000000000000 }, /* 4 */ + 0b11000 => { 0x4020000000000000 }, /* 8 */ + 0b11001 => { 0x4030000000000000 }, /* 16 */ + 0b11010 => { 0x4060000000000000 }, /* 2^7 */ + 0b11011 => { 0x4070000000000000 }, /* 2^8 */ + 0b11100 => { 0x40e0000000000000 }, /* 2^15 */ + 0b11101 => { 0x40f0000000000000 }, /* 2^16 */ + 0b11110 => { 0x7ff0000000000000 }, /* +inf */ + 0b11111 => { canonical_NaN_D() }, + }; + F_D(rd) = bits; + RETIRE_SUCCESS +} + +/* FMINM.H */ + +union clause ast = RISCV_FMINM_H : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMINM_H(rs2, rs1, rd) if haveZfh() & haveZfa() + <-> 0b001_0110 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FMINM_H(rs2, rs1, rd) + <-> "fminm.h" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute (RISCV_FMINM_H(rs2, rs1, rd)) = { + let rs1_val_H = F_H(rs1); + let rs2_val_H = F_H(rs2); + + let is_quiet = true; + let (rs1_lt_rs2, fflags) = fle_H (rs1_val_H, rs2_val_H, is_quiet); + + let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN_H() + else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs1_val_H + else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs2_val_H + else if rs1_lt_rs2 then rs1_val_H + else /* (not rs1_lt_rs2) */ rs2_val_H; + + accrue_fflags(fflags); + F_H(rd) = rd_val_H; + RETIRE_SUCCESS +} + +/* FMAXM.H */ + +union clause ast = RISCV_FMAXM_H : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMAXM_H(rs2, rs1, rd) if haveZfh() & haveZfa() + <-> 0b001_0110 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FMAXM_H(rs2, rs1, rd) + <-> "fmaxm.h" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute (RISCV_FMAXM_H(rs2, rs1, rd)) = { + let rs1_val_H = F_H(rs1); + let rs2_val_H = F_H(rs2); + + let is_quiet = true; + let (rs2_lt_rs1, fflags) = fle_H (rs2_val_H, rs1_val_H, is_quiet); + + let rd_val_H = if (f_is_NaN_H(rs1_val_H) | f_is_NaN_H(rs2_val_H)) then canonical_NaN_H() + else if (f_is_neg_zero_H(rs1_val_H) & f_is_pos_zero_H(rs2_val_H)) then rs2_val_H + else if (f_is_neg_zero_H(rs2_val_H) & f_is_pos_zero_H(rs1_val_H)) then rs1_val_H + else if rs2_lt_rs1 then rs1_val_H + else /* (not rs2_lt_rs1) */ rs2_val_H; + + accrue_fflags(fflags); + F_H(rd) = rd_val_H; + RETIRE_SUCCESS +} + +/* FMINM.S */ + +union clause ast = RISCV_FMINM_S : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMINM_S(rs2, rs1, rd) if haveZfa() + <-> 0b001_0100 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FMINM_S(rs2, rs1, rd) + <-> "fminm.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute (RISCV_FMINM_S(rs2, rs1, rd)) = { + let rs1_val_S = F_S(rs1); + let rs2_val_S = F_S(rs2); + + let is_quiet = true; + let (rs1_lt_rs2, fflags) = fle_S (rs1_val_S, rs2_val_S, is_quiet); + + let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() + else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs1_val_S + else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs2_val_S + else if rs1_lt_rs2 then rs1_val_S + else /* (not rs1_lt_rs2) */ rs2_val_S; + + accrue_fflags(fflags); + F_S(rd) = rd_val_S; + RETIRE_SUCCESS +} + +/* FMAXM.S */ + +union clause ast = RISCV_FMAXM_S : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMAXM_S(rs2, rs1, rd) if haveZfa() + <-> 0b001_0100 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FMAXM_S(rs2, rs1, rd) + <-> "fmaxm.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute (RISCV_FMAXM_S(rs2, rs1, rd)) = { + let rs1_val_S = F_S(rs1); + let rs2_val_S = F_S(rs2); + + let is_quiet = true; + let (rs2_lt_rs1, fflags) = fle_S (rs2_val_S, rs1_val_S, is_quiet); + + let rd_val_S = if (f_is_NaN_S(rs1_val_S) | f_is_NaN_S(rs2_val_S)) then canonical_NaN_S() + else if (f_is_neg_zero_S(rs1_val_S) & f_is_pos_zero_S(rs2_val_S)) then rs2_val_S + else if (f_is_neg_zero_S(rs2_val_S) & f_is_pos_zero_S(rs1_val_S)) then rs1_val_S + else if rs2_lt_rs1 then rs1_val_S + else /* (not rs2_lt_rs1) */ rs2_val_S; + + accrue_fflags(fflags); + F_S(rd) = rd_val_S; + RETIRE_SUCCESS +} + +/* FMINM.D */ + +union clause ast = RISCV_FMINM_D : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMINM_D(rs2, rs1, rd) if haveDExt() & haveZfa() + <-> 0b001_0101 @ rs2 @ rs1 @ 0b010 @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FMINM_D(rs2, rs1, rd) + <-> "fminm.d" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute (RISCV_FMINM_D(rs2, rs1, rd)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let is_quiet = true; + let (rs1_lt_rs2, fflags) = fle_D (rs1_val_D, rs2_val_D, is_quiet); + + let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN_D() + else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs1_val_D + else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs2_val_D + else if rs1_lt_rs2 then rs1_val_D + else rs2_val_D; + + accrue_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +/* FMAXM.D */ + +union clause ast = RISCV_FMAXM_D : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMAXM_D(rs2, rs1, rd) if haveDExt() & haveZfa() + <-> 0b001_0101 @ rs2 @ rs1 @ 0b011 @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FMAXM_D(rs2, rs1, rd) + <-> "fmaxm.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute (RISCV_FMAXM_D(rs2, rs1, rd)) = { + let rs1_val_D = F(rs1); + let rs2_val_D = F(rs2); + + let is_quiet = true; + let (rs2_lt_rs1, fflags) = fle_D (rs2_val_D, rs1_val_D, is_quiet); + + let rd_val_D = if (f_is_NaN_D(rs1_val_D) | f_is_NaN_D(rs2_val_D)) then canonical_NaN_D() + else if (f_is_neg_zero_D(rs1_val_D) & f_is_pos_zero_D(rs2_val_D)) then rs2_val_D + else if (f_is_neg_zero_D(rs2_val_D) & f_is_pos_zero_D(rs1_val_D)) then rs1_val_D + else if rs2_lt_rs1 then rs1_val_D + else rs2_val_D; + + accrue_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS +} + +/* FROUND.H */ + +union clause ast = RISCV_FROUND_H : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUND_H(rs1, rm, rd) if haveZfh() & haveZfa() + <-> 0b010_0010 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FROUND_H(rs1, rm, rd) + <-> "fround.h" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUND_H(rs1, rm, rd)) = { + let rs1_val_H = F_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_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, false); + + write_fflags(fflags); + F_H(rd) = rd_val_H; + RETIRE_SUCCESS + } + } +} + +/* FROUNDNX.H */ + +union clause ast = RISCV_FROUNDNX_H : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUNDNX_H(rs1, rm, rd) if haveZfh() & haveZfa() + <-> 0b010_0010 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FROUNDNX_H(rs1, rm, rd) + <-> "froundnx.h" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUNDNX_H(rs1, rm, rd)) = { + let rs1_val_H = F_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_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, true); + + write_fflags(fflags); + F_H(rd) = rd_val_H; + RETIRE_SUCCESS + } + } +} + +/* FROUND.S */ + +union clause ast = RISCV_FROUND_S : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUND_S(rs1, rm, rd) if haveZfa() + <-> 0b010_0000 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FROUND_S(rs1, rm, rd) + <-> "fround.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUND_S(rs1, rm, rd)) = { + 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_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, false); + + write_fflags(fflags); + F_S(rd) = rd_val_S; + RETIRE_SUCCESS + } + } +} + +/* FROUNDNX.S */ + +union clause ast = RISCV_FROUNDNX_S : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUNDNX_S(rs1, rm, rd) if haveZfa() + <-> 0b010_0000 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FROUNDNX_S(rs1, rm, rd) + <-> "froundnx.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUNDNX_S(rs1, rm, rd)) = { + 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_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, true); + + write_fflags(fflags); + F_S(rd) = rd_val_S; + RETIRE_SUCCESS + } + } +} + +/* FROUND.D */ + +union clause ast = RISCV_FROUND_D : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUND_D(rs1, rm, rd) if haveDExt() & haveZfa() + <-> 0b010_0001 @ 0b00100 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FROUND_D(rs1, rm, rd) + <-> "fround.d" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = { + let rs1_val_D = F(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_f64roundToInt(rm_3b, rs1_val_D, false); + + write_fflags(fflags); + F(rd) = rd_val_D; + RETIRE_SUCCESS + } + } +} + +/* FROUNDNX.D */ + +union clause ast = RISCV_FROUNDNX_D : (regidx, rounding_mode, regidx) + +mapping clause encdec = RISCV_FROUNDNX_D(rs1, rm, rd) if haveDExt() & haveZfa() + <-> 0b010_0001 @ 0b00101 @ rs1 @ encdec_rounding_mode(rm) @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FROUNDNX_D(rs1, rm, rd) + <-> "froundnx.d" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ frm_mnemonic(rm) + +function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = { + 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_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, true); + + write_fflags(fflags); + F_D(rd) = rd_val_D; + RETIRE_SUCCESS + } + } +} + +/* FMVH.X.D */ + +union clause ast = RISCV_FMVH_X_D : (regidx, regidx) + +mapping clause encdec = RISCV_FMVH_X_D(rs1, rd) if haveDExt() & haveZfa() & in32BitMode() + <-> 0b111_0001 @ 0b00001 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & haveZfa() & in32BitMode() + +mapping clause assembly = RISCV_FMVH_X_D(rs1, rd) + <-> "fmvh.x.d" ^ spc() ^ reg_name(rd) + ^ spc() ^ freg_name(rs1) + +function clause execute (RISCV_FMVH_X_D(rs1, rd)) = { + let rs1_val_D = F_D(rs1)[63..32]; + let rd_val_X : xlenbits = EXTS(rs1_val_D); + X(rd) = rd_val_X; + RETIRE_SUCCESS +} + +/* FMVP.X.D */ + +union clause ast = RISCV_FMVP_D_X : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FMVP_D_X(rs2, rs1, rd) if haveDExt() & haveZfa() & in32BitMode() + <-> 0b101_1001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b101_0011 if haveDExt() & haveZfa() & in32BitMode() + +mapping clause assembly = RISCV_FMVP_D_X(rs2, rs1, rd) + <-> "fmvp.d.x" ^ spc() ^ freg_name(rd) + ^ spc() ^ reg_name(rs1) + ^ spc() ^ reg_name(rs2) + +function clause execute (RISCV_FMVP_D_X(rs2, rs1, rd)) = { + let rs1_val_X = X(rs1)[31..0]; + let rs2_val_X = X(rs2)[31..0]; + + /* Concatenate the two values using '@' operator */ + /* e.g. */ + /* rs1 = 0x01234567 */ + /* rs2 = 0x89abcdef */ + /* rd = rs1 @ rs2 => 0x89abcdef01234567 */ + let rd_val_D = rs2_val_X @ rs1_val_X; + + F_D(rd) = rd_val_D; + RETIRE_SUCCESS +} + +/* FLEQ.H */ + +union clause ast = RISCV_FLEQ_H : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLEQ_H(rs2, rs1, rd) if haveZfh() & haveZfa() + <-> 0b101_0010 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FLEQ_H(rs2, rs1, rd) + <-> "fleq.h" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = { + let rs1_val_H = F_H(rs1); + let rs2_val_H = F_H(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f16Le_quiet (rs1_val_H, rs2_val_H); + + write_fflags(fflags); + X(rd) = EXTZ(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* FLTQ.H */ + +union clause ast = RISCV_FLTQ_H : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLTQ_H(rs2, rs1, rd) if haveZfh() & haveZfa() + <-> 0b101_0010 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveZfh() & haveZfa() + +mapping clause assembly = RISCV_FLTQ_H(rs2, rs1, rd) + <-> "fltq.h" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = { + let rs1_val_H = F_H(rs1); + let rs2_val_H = F_H(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f16Lt_quiet (rs1_val_H, rs2_val_H); + + write_fflags(fflags); + X(rd) = EXTZ(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* FLEQ.S */ + +union clause ast = RISCV_FLEQ_S : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLEQ_S(rs2, rs1, rd) if haveZfa() + <-> 0b101_0000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FLEQ_S(rs2, rs1, rd) + <-> "fleq.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = { + let rs1_val_S = F_S(rs1); + let rs2_val_S = F_S(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f32Le_quiet (rs1_val_S, rs2_val_S); + + write_fflags(fflags); + X(rd) = EXTZ(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* FLTQ.S */ + +union clause ast = RISCV_FLTQ_S : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLTQ_S(rs2, rs1, rd) if haveZfa() + <-> 0b101_0000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveZfa() + +mapping clause assembly = RISCV_FLTQ_S(rs2, rs1, rd) + <-> "fltq.s" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = { + let rs1_val_S = F_S(rs1); + let rs2_val_S = F_S(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f32Lt_quiet (rs1_val_S, rs2_val_S); + + write_fflags(fflags); + X(rd) = EXTZ(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + + +/* FLEQ.D */ + +union clause ast = RISCV_FLEQ_D : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLEQ_D(rs2, rs1, rd) if haveDExt() & haveZfa() + <-> 0b101_0001 @ rs2 @ rs1 @ 0b100 @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FLEQ_D(rs2, rs1, rd) + <-> "fleq.d" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = { + let rs1_val_D = F_D(rs1); + let rs2_val_D = F_D(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f64Le_quiet (rs1_val_D, rs2_val_D); + + write_fflags(fflags); + X(rd) = EXTZ(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* FLTQ.D */ + +union clause ast = RISCV_FLTQ_D : (regidx, regidx, regidx) + +mapping clause encdec = RISCV_FLTQ_D(rs2, rs1, rd) if haveDExt() & haveZfa() + <-> 0b101_0001 @ rs2 @ rs1 @ 0b101 @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FLTQ_D(rs2, rs1, rd) + <-> "fltq.d" ^ spc() ^ freg_name(rd) + ^ spc() ^ freg_name(rs1) + ^ spc() ^ freg_name(rs2) + +function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = { + let rs1_val_D = F_D(rs1); + let rs2_val_D = F_D(rs2); + + let (fflags, rd_val) : (bits_fflags, bool) = + riscv_f64Lt_quiet (rs1_val_D, rs2_val_D); + + write_fflags(fflags); + X(rd) = EXTZ(bool_to_bits(rd_val)); + RETIRE_SUCCESS +} + +/* FCVTMOD.W.D */ + +/* + * Implement float64 to int32 conversion without saturation, the + * result is supplied modulo 2^32. + */ +val fcvtmod_helper : bits(64) -> (bits(5), bits(32)) +function fcvtmod_helper(x64) = { + let (sign, exp, mant) = fsplit_D(x64); + + /* Detect the non-normal cases */ + let is_subnorm = exp == zeros() & mant != zeros(); + let is_zero = exp == zeros() & mant == zeros(); + let is_nan_or_inf = exp == ones(); + + /* For normal numbers, the mantissa and exponent use special encoding */ + let true_mant = 0b1 @ mant; /* concatenate with the implicit bit */ + let true_exp = unsigned(exp) - 1023; /* undo the offset-binary */ + + /* + * Detect the trivial cases for normal numbers. + * + * While is_too_large could subsume is_nan_or_inf, and is_too_small + * cound subsume is_subnorm, we deliberately enumerate these + * separately as is_too_large/is_too_small operate on normal + * numbers. + */ + let is_too_large = true_exp >= 84; /* bits will be 'multiplied' out */ + let is_too_small = true_exp < 0; /* bits will be 'divided' out */ + + if is_zero then (zeros(), zeros()) + else if is_subnorm then (nxFlag(), zeros()) + else if is_nan_or_inf then (nvFlag(), zeros()) + else if is_too_large then (nvFlag(), zeros()) + else if is_too_small then (nxFlag(), zeros()) + else { + /* + * Calculate the low 32 bits of the integer value from the + * binary64 floating-point number and return them together with an + * indicator whether a NV (overflow) or NX (inexact) exceptions is + * to be raised. + */ + + /* Perform the exponentation on the fixed-point mantissa and + extract the integer part */ + let fixedpoint : bits(84) = EXTZ(true_mant) << true_exp; + let integer = fixedpoint[83..52]; + let fractional = fixedpoint[51..0]; + + /* Apply the sign bit */ + let result = if sign == 0b1 then ~(integer) + 1 + else integer; + + /* Raise FP exception flags, honoring the precedence of nV > nX */ + let flags : bits(5) = if (true_exp > 31) then nvFlag() + else if (fractional != zeros()) then nxFlag() + else zeros(); + + (flags, result) + } +} + +union clause ast = RISCV_FCVTMOD_W_D : (regidx, regidx) + +/* We need rounding mode to be explicitly specified to RTZ(0b001) */ +mapping clause encdec = RISCV_FCVTMOD_W_D(rs1, rd) if haveDExt() & haveZfa() + <-> 0b110_0001 @ 0b01000 @ rs1 @ 0b001 @ rd @ 0b101_0011 if haveDExt() & haveZfa() + +mapping clause assembly = RISCV_FCVTMOD_W_D(rs1, rd) + <-> "fcvtmod.w.d" ^ spc() ^ reg_name(rd) + ^ spc() ^ freg_name(rs1) + +function clause execute(RISCV_FCVTMOD_W_D(rs1, rd)) = { + let rs1_val_D = F_D(rs1); + let (fflags, rd_val) = fcvtmod_helper(rs1_val_D); + write_fflags(fflags); + X(rd) = EXTS(rd_val); + RETIRE_SUCCESS +} diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 4706e92b8..5daddcb11 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -468,6 +468,13 @@ function riscv_f16Lt (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit +val riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +function riscv_f16Lt_quiet (v1, v2) = { + extern_f16Lt_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit val riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} function riscv_f16Le (v1, v2) = { @@ -475,6 +482,13 @@ function riscv_f16Le (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit +val riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} +function riscv_f16Le_quiet (v1, v2) = { + extern_f16Le_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) effect {rreg} function riscv_f16Eq (v1, v2) = { @@ -489,6 +503,13 @@ function riscv_f32Lt (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit +val riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +function riscv_f32Lt_quiet (v1, v2) = { + extern_f32Lt_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} function riscv_f32Le (v1, v2) = { @@ -496,6 +517,13 @@ function riscv_f32Le (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit +val riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} +function riscv_f32Le_quiet (v1, v2) = { + extern_f32Le_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) effect {rreg} function riscv_f32Eq (v1, v2) = { @@ -510,6 +538,13 @@ function riscv_f64Lt (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit +val riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +function riscv_f64Lt_quiet (v1, v2) = { + extern_f64Lt_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} function riscv_f64Le (v1, v2) = { @@ -517,10 +552,38 @@ function riscv_f64Le (v1, v2) = { (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } +val extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit +val riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} +function riscv_f64Le_quiet (v1, v2) = { + extern_f64Le_quiet(v1, v2); + (float_fflags[4 .. 0], bit_to_bool(float_result[0])) +} + val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) effect {rreg} function riscv_f64Eq (v1, v2) = { extern_f64Eq(v1, v2); (float_fflags[4 .. 0], bit_to_bool(float_result[0])) } + +val extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit +val riscv_f16roundToInt : (bits_rm, bits_H, bool) -> (bits_fflags, bits_H) effect {rreg} +function riscv_f16roundToInt (rm, v, exact) = { + extern_f16roundToInt(rm, v, exact); + (float_fflags[4 .. 0], float_result[15 .. 0]) +} + +val extern_f32roundToInt = {c: "softfloat_f32roundToInt", ocaml: "Softfloat.f32_round_to_int", lem: "softfloat_f32_round_to_int"} : (bits_rm, bits_S, bool) -> unit +val riscv_f32roundToInt : (bits_rm, bits_S, bool) -> (bits_fflags, bits_S) effect {rreg} +function riscv_f32roundToInt (rm, v, exact) = { + extern_f32roundToInt(rm, v, exact); + (float_fflags[4 .. 0], float_result[31 .. 0]) +} + +val extern_f64roundToInt = {c: "softfloat_f64roundToInt", ocaml: "Softfloat.f64_round_to_int", lem: "softfloat_f64_round_to_int"} : (bits_rm, bits_D, bool) -> unit +val riscv_f64roundToInt : (bits_rm, bits_D, bool) -> (bits_fflags, bits_D) effect {rreg} +function riscv_f64roundToInt (rm, v, exact) = { + extern_f64roundToInt(rm, v, exact); + (float_fflags[4 .. 0], float_result) +} /* **************************************************************** */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index aed6eac3e..fe1b5dcf6 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -189,6 +189,9 @@ function haveZbb() -> bool = true function haveZbc() -> bool = true function haveZbs() -> bool = true +/* Zfa (additional FP) extension */ +function haveZfa() -> bool = true + /* Scalar Cryptography extensions support. */ function haveZbkb() -> bool = true function haveZbkc() -> bool = true diff --git a/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml index 01aaa2a4f..2b98751a4 100644 --- a/ocaml_emulator/softfloat.ml +++ b/ocaml_emulator/softfloat.ml @@ -146,26 +146,53 @@ let f64_to_f32 rm v = let f16_lt v1 v2 = () +let f16_lt_quiet v1 v2 = + () + let f16_le v1 v2 = () +let f16_le_quiet v1 v2 = + () + let f16_eq v1 v2 = () let f32_lt v1 v2 = () +let f32_lt_quiet v1 v2 = + () + let f32_le v1 v2 = () +let f32_le_quiet v1 v2 = + () + let f32_eq v1 v2 = () let f64_lt v1 v2 = () +let f64_lt_quiet v1 v2 = + () + let f64_le v1 v2 = () +let f64_le_quiet v1 v2 = + () + let f64_eq v1 v2 = () + +let f16_round_to_int exact rm v = + () + +let f32_round_to_int exact rm v = + () + +let f64_round_to_int exact rm v = + ()