Skip to content

Commit

Permalink
Use {f16,f32,f64}roundToInt for FROUND & FROUNDNX instructions
Browse files Browse the repository at this point in the history 
This commits also adds the following functions from
Softfloat C library into SAIL interface, for using
them in the FROUND.[H,S,D] & FROUNDNX.[H,S,D]
instructions:
 * f16_roundToInt
 * f32_roundToInt
 * f64_roundToInt

Signed-off-by: Charalampos Mitrodimas <[email protected]>
  • Loading branch information
@ptomsich
Charalampos Mitrodimas authored and ptomsich committed Apr 10, 2023
1 parent 213d048 commit 9d5a65f
Show file tree
Hide file tree
Showing 5 changed files with 104 additions and 79 deletions.
39 changes: 39 additions & 0 deletions c_emulator/riscv_softfloat.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
4 changes: 4 additions & 0 deletions c_emulator/riscv_softfloat.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
108 changes: 30 additions & 78 deletions model/riscv_insts_zfa.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}
Expand All @@ -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
}
}
Expand All @@ -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
}
}
Expand All @@ -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
}
}
Expand All @@ -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
}
}
Expand All @@ -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
}
}
Expand Down
23 changes: 22 additions & 1 deletion model/riscv_softfloat_interface.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 */

Expand Down Expand Up @@ -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)
}
/* **************************************************************** */
9 changes: 9 additions & 0 deletions ocaml_emulator/softfloat.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
()

0 comments on commit 9d5a65f

Please sign in to comment.