diff --git a/c_emulator/riscv_softfloat.c b/c_emulator/riscv_softfloat.c index b3819b6a3..ee30f0b7c 100644 --- a/c_emulator/riscv_softfloat.c +++ b/c_emulator/riscv_softfloat.c @@ -744,3 +744,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..8fab64078 100644 --- a/c_emulator/riscv_softfloat.h +++ b/c_emulator/riscv_softfloat.h @@ -70,3 +70,7 @@ unit softfloat_f32eq(mach_bits v1, mach_bits v2); unit softfloat_f64lt(mach_bits v1, mach_bits v2); unit softfloat_f64le(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/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index a0fb82fc0..56aeaec12 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -342,24 +342,17 @@ mapping clause assembly = RISCV_FROUND_H(rs1, rm, rd) function clause execute (RISCV_FROUND_H(rs1, rm, rd)) = { let rs1_val_H = nan_unbox_H(F(rs1)); - let fflags = fcsr.FFLAGS(); + fflags = fcsr.FFLAGS(); match (select_instr_or_fcsr_rm(rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); + let (round_fflags, rd_val_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, true); + fflags = fflags | round_fflags; - let (result_fflags, result_F) = if (f_is_NaN_H(rs1_val_H)) then (nvFlag(), rs1_val_H) - else if (f_is_pos_inf_H(rs1_val_H) | f_is_neg_inf_H(rs1_val_H)) then (fflags, rs1_val_H) - else if (f_is_pos_zero_H(rs1_val_H) | f_is_neg_zero_H(rs1_val_H)) then (fflags, rs1_val_H) - else { - let (_, rd_val_H) = riscv_f16ToI32(rm_3b, rs1_val_H); - let (_, rd_val_H) = riscv_i32ToF16(rm_3b, rd_val_H); - (fflags, rd_val_H) - }; - - write_fflags(result_fflags); - F(rd) = nan_box_H(result_F); + write_fflags(fflags); + F(rd) = nan_box_H(rd_val_H); RETIRE_SUCCESS } } @@ -379,26 +372,17 @@ mapping clause assembly = RISCV_FROUNDNX_H(rs1, rm, rd) function clause execute (RISCV_FROUNDNX_H(rs1, rm, rd)) = { let rs1_val_H = nan_unbox_H(F(rs1)); - let fflags = fcsr.FFLAGS(); + fflags = fcsr.FFLAGS(); match (select_instr_or_fcsr_rm(rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); + let (round_fflags, rd_val_H) = riscv_f16roundToInt(rm_3b, rs1_val_H, false); + fflags = fflags | round_fflags; - let (result_fflags, result_F) = if (f_is_NaN_H(rs1_val_H)) then (nvFlag(), rs1_val_H) - else if (f_is_pos_inf_H(rs1_val_H) | f_is_neg_inf_H(rs1_val_H)) then (fflags, rs1_val_H) - else if (f_is_pos_zero_H(rs1_val_H) | f_is_neg_zero_H(rs1_val_H)) then (fflags, rs1_val_H) - else { - let (_, rd_val_H) = riscv_f16ToI32(rm_3b, rs1_val_H); - let (_, rd_val_H) = riscv_i32ToF16(rm_3b, rd_val_H); - - if (rs1_val_H != rd_val_H) then (nxFlag(), rd_val_H) - else (fflags, rd_val_H) - }; - - write_fflags(result_fflags); - F(rd) = nan_box_H(result_F); + write_fflags(fflags); + F(rd) = nan_box_H(rd_val_H); RETIRE_SUCCESS } } @@ -418,24 +402,17 @@ mapping clause assembly = RISCV_FROUND_S(rs1, rm, rd) function clause execute (RISCV_FROUND_S(rs1, rm, rd)) = { let rs1_val_S = nan_unbox_S(F(rs1)); - let fflags = fcsr.FFLAGS(); + fflags = fcsr.FFLAGS(); match (select_instr_or_fcsr_rm(rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); + let (round_fflags, rd_val_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, true); + fflags = fflags | round_fflags; - let (result_fflags, result_F) = if (f_is_NaN_S(rs1_val_S)) then (nvFlag(), rs1_val_S) - else if (f_is_pos_inf_S(rs1_val_S) | f_is_neg_inf_S(rs1_val_S)) then (fflags, rs1_val_S) - else if (f_is_pos_zero_S(rs1_val_S) | f_is_neg_zero_S(rs1_val_S)) then (fflags, rs1_val_S) - else { - let (_, rd_val_S) = riscv_f32ToI32(rm_3b, rs1_val_S); - let (_, rd_val_S) = riscv_i32ToF32(rm_3b, rd_val_S); - (fflags, rd_val_S) - }; - - write_fflags(result_fflags); - F(rd) = nan_box_S(result_F); + write_fflags(fflags); + F(rd) = nan_box_S(rd_val_S); RETIRE_SUCCESS } } @@ -455,26 +432,17 @@ mapping clause assembly = RISCV_FROUNDNX_S(rs1, rm, rd) function clause execute (RISCV_FROUNDNX_S(rs1, rm, rd)) = { let rs1_val_S = nan_unbox_S(F(rs1)); - let fflags = fcsr.FFLAGS(); + fflags = fcsr.FFLAGS(); match (select_instr_or_fcsr_rm(rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); + let (round_fflags, rd_val_S) = riscv_f32roundToInt(rm_3b, rs1_val_S, false); + fflags = fflags | round_fflags; - let (result_fflags, result_F) = if (f_is_NaN_S(rs1_val_S)) then (nvFlag(), rs1_val_S) - else if (f_is_pos_inf_S(rs1_val_S) | f_is_neg_inf_S(rs1_val_S)) then (fflags, rs1_val_S) - else if (f_is_pos_zero_S(rs1_val_S) | f_is_neg_zero_S(rs1_val_S)) then (fflags, rs1_val_S) - else { - let (_, rd_val_S) = riscv_f32ToI32(rm_3b, rs1_val_S); - let (_, rd_val_S) = riscv_i32ToF32(rm_3b, rd_val_S); - - if (rs1_val_S != rd_val_S) then (nxFlag(), rd_val_S) - else (fflags, rd_val_S) - }; - - write_fflags(result_fflags); - F(rd) = nan_box_S(result_F); + write_fflags(fflags); + F(rd) = nan_box_S(rd_val_S); RETIRE_SUCCESS } } @@ -494,24 +462,17 @@ mapping clause assembly = RISCV_FROUND_D(rs1, rm, rd) function clause execute (RISCV_FROUND_D(rs1, rm, rd)) = { let rs1_val_D = F(rs1); - let fflags = fcsr.FFLAGS(); + fflags = fcsr.FFLAGS(); match (select_instr_or_fcsr_rm(rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); + let (round_fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, true); + fflags = fflags | round_fflags; - let (result_fflags, result_F) = if (f_is_NaN_D(rs1_val_D)) then (nvFlag(), rs1_val_D) - else if (f_is_pos_inf_D(rs1_val_D) | f_is_neg_inf_D(rs1_val_D)) then (fflags, rs1_val_D) - else if (f_is_pos_zero_D(rs1_val_D) | f_is_neg_zero_D(rs1_val_D)) then (fflags, rs1_val_D) - else { - let (_, rd_val_D) = riscv_f64ToI64(rm_3b, rs1_val_D); - let (_, rd_val_D) = riscv_i64ToF64(rm_3b, rd_val_D); - (fflags, rd_val_D) - }; - - write_fflags(result_fflags); - F(rd) = result_F; + write_fflags(fflags); + F(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -531,26 +492,17 @@ mapping clause assembly = RISCV_FROUNDNX_D(rs1, rm, rd) function clause execute (RISCV_FROUNDNX_D(rs1, rm, rd)) = { let rs1_val_D = F(rs1); - let fflags = fcsr.FFLAGS(); + fflags = fcsr.FFLAGS(); match (select_instr_or_fcsr_rm(rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { let rm_3b = encdec_rounding_mode(rm'); + let (round_fflags, rd_val_D) = riscv_f64roundToInt(rm_3b, rs1_val_D, false); + fflags = fflags | round_fflags; - let (result_fflags, result_F) = if (f_is_NaN_D(rs1_val_D)) then (nvFlag(), rs1_val_D) - else if (f_is_pos_inf_D(rs1_val_D) | f_is_neg_inf_D(rs1_val_D)) then (fflags, rs1_val_D) - else if (f_is_pos_zero_D(rs1_val_D) | f_is_neg_zero_D(rs1_val_D)) then (fflags, rs1_val_D) - else { - let (_, rd_val_D) = riscv_f64ToI64(rm_3b, rs1_val_D); - let (_, rd_val_D) = riscv_i64ToF64(rm_3b, rd_val_D); - - if (rs1_val_D != rd_val_D) then (nxFlag(), rd_val_D) - else (fflags, rd_val_D) - }; - - write_fflags(result_fflags); - F(rd) = result_F; + write_fflags(fflags); + F(rd) = rd_val_D; RETIRE_SUCCESS } } diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 4706e92b8..d601f81b6 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -87,7 +87,7 @@ type bits_rm = bits(3) /* Rounding mode */ type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */ -type bits_H = bits(16) /* Half-precision float value */ +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 */ @@ -523,4 +523,25 @@ 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/ocaml_emulator/softfloat.ml b/ocaml_emulator/softfloat.ml index 01aaa2a4f..1fd3f7fbb 100644 --- a/ocaml_emulator/softfloat.ml +++ b/ocaml_emulator/softfloat.ml @@ -169,3 +169,12 @@ let f64_le 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 = + ()