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 = + ()