Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Float: Add floating-point equals API in sail model #403

Closed
wants to merge 13 commits into from
Closed
2 changes: 2 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,8 @@ SAIL_SYS_SRCS += riscv_next_regs.sail
SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling
SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model
SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension
SAIL_SYS_SRCS += float/riscv_float_common.sail
SAIL_SYS_SRCS += float/riscv_float_eq.sail
SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail
SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions
SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling
Expand Down
18 changes: 18 additions & 0 deletions model/float/riscv_float_common.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
/*=======================================================================================*/
Incarnation-p-lee marked this conversation as resolved.
Show resolved Hide resolved
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

/* **************************************************************** */
/* This file implements the floating-point for some common helper */
/* functions. They will be leveraged by other float sail implement. */
/* */
/* **************************************************************** */

type bits_rm = bits(3) /* Rounding mode */
type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */

let float_flag_invalid : bits_fflags = 0b10000
43 changes: 43 additions & 0 deletions model/float/riscv_float_eq.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

/* **************************************************************** */
/* This file implements the floating-point for equal. The below */
/* floating-point types are supported. */
/* */
/* 1. Double-precision, aka 64 bits floating-point. */
/* 2. Single-precision, aka 32 bits floating-point. */
/* 3. Half-precision, aka 16 bits floating-point. */
/* **************************************************************** */

val f_is_NaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool
val f_is_SNaN : forall 'm, 'm in {16, 32, 64}. bits('m) -> bool
val accrue_fflags : (bits_fflags) -> unit

val float_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> (bits_fflags, bool)
function float_eq (op1, op2) = {
let is_nan = f_is_NaN(op1) | f_is_NaN(op2);
let is_snan = f_is_SNaN(op1) | f_is_SNaN(op2);
let fflags = if is_nan & is_snan
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is_nan & can be removed here because is_snan is a subset of is_nan.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated.

then float_flag_invalid
else zeros();
let is_equal : bool = if not(is_nan)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This can be simplified to the following:

let is_equal = not(is_nan) & (op1 == op2 | ((op1 | op2) << 1) == zeros());

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated and removed the bool declaration.

then op1 == op2 | ((op1 | op2) << 1) == zeros()
else false;

(fflags, is_equal)
}

val float_raise_flags_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function float_raise_flags_eq (op1, op2) = {
let (fflags, is_equal) = float_eq(op1, op2);

accrue_fflags(fflags);

is_equal
}
3 changes: 1 addition & 2 deletions model/riscv_insts_dext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -797,8 +797,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
let rs1_val_D = F_or_X_D(rs1);
let rs2_val_D = F_or_X_D(rs2);

let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f64Eq (rs1_val_D, rs2_val_D);
let (fflags, rd_val) = float_eq(rs1_val_D, rs2_val_D);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
Expand Down
3 changes: 1 addition & 2 deletions model/riscv_insts_fext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -921,8 +921,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
let rs1_val_S = F_or_X_S(rs1);
let rs2_val_S = F_or_X_S(rs2);

let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f32Eq (rs1_val_S, rs2_val_S);
let (fflags, rd_val) = float_eq(rs1_val_S, rs2_val_S);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
Expand Down
11 changes: 0 additions & 11 deletions model/riscv_insts_vext_utils.sail
Original file line number Diff line number Diff line change
Expand Up @@ -685,17 +685,6 @@ function fp_max(op1, op2) = {
result_val
}

val fp_eq : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function fp_eq(op1, op2) = {
let (fflags, result_val) : (bits_fflags, bool) = match 'm {
16 => riscv_f16Eq(op1, op2),
32 => riscv_f32Eq(op1, op2),
64 => riscv_f64Eq(op1, op2)
};
accrue_fflags(fflags);
result_val
}

val fp_gt : forall 'm, 'm in {16, 32, 64}. (bits('m), bits('m)) -> bool
function fp_gt(op1, op2) = {
let (fflags, temp_val) : (bits_fflags, bool) = match 'm {
Expand Down
8 changes: 4 additions & 4 deletions model/riscv_insts_vext_vm.sail
Original file line number Diff line number Diff line change
Expand Up @@ -760,8 +760,8 @@ function clause execute(FVVMTYPE(funct6, vm, vs2, vs1, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
let res : bool = match funct6 {
FVVM_VMFEQ => fp_eq(vs2_val[i], vs1_val[i]),
FVVM_VMFNE => ~(fp_eq(vs2_val[i], vs1_val[i])),
FVVM_VMFEQ => float_raise_flags_eq(vs2_val[i], vs1_val[i]),
FVVM_VMFNE => ~(float_raise_flags_eq(vs2_val[i], vs1_val[i])),
FVVM_VMFLE => fp_le(vs2_val[i], vs1_val[i]),
FVVM_VMFLT => fp_lt(vs2_val[i], vs1_val[i])
};
Expand Down Expand Up @@ -824,8 +824,8 @@ function clause execute(FVFMTYPE(funct6, vm, vs2, rs1, vd)) = {
foreach (i from 0 to (num_elem - 1)) {
if mask[i] then {
let res : bool = match funct6 {
VFM_VMFEQ => fp_eq(vs2_val[i], rs1_val),
VFM_VMFNE => ~(fp_eq(vs2_val[i], rs1_val)),
VFM_VMFEQ => float_raise_flags_eq(vs2_val[i], rs1_val),
VFM_VMFNE => ~(float_raise_flags_eq(vs2_val[i], rs1_val)),
VFM_VMFLE => fp_le(vs2_val[i], rs1_val),
VFM_VMFLT => fp_lt(vs2_val[i], rs1_val),
VFM_VMFGE => fp_ge(vs2_val[i], rs1_val),
Expand Down
3 changes: 1 addition & 2 deletions model/riscv_insts_zfh.sail
Original file line number Diff line number Diff line change
Expand Up @@ -412,8 +412,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = {
let rs1_val_H = F_or_X_H(rs1);
let rs2_val_H = F_or_X_H(rs2);

let (fflags, rd_val) : (bits_fflags, bool) =
riscv_f16Eq (rs1_val_H, rs2_val_H);
let (fflags, rd_val) = float_eq(rs1_val_H, rs2_val_H);

accrue_fflags(fflags);
X(rd) = zero_extend(bool_to_bits(rd_val));
Expand Down
23 changes: 0 additions & 23 deletions model/riscv_softfloat_interface.sail
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,6 @@
/* **************************************************************** */
/* All arguments and results have one of these types */

type bits_rm = bits(3) /* Rounding mode */
type bits_fflags = bits(5) /* Accrued exceptions: NV,DZ,OF,UF,NX */
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't see how this builds if you delete the type used by the unconverted functions...

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I see, you moved that but nothing else to a new file. That seems like a strange design choice; I would expect fflags and frm to be defined next to each other given they both constitute fcsr.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This type moved to the riscv_float_common.sail, which will be leveraged by the floating-point implementation (like float_eq) in sail.

Given the softfloat_interface will be retired soon, it is better to let the softfloat_interface
depends on riscv_float_common.sail. Of course, you are right, the related types like frm/fflags will be removed to the riscv_float_common.sail soon. I didn't perform this change because they are not referenced by the float_eq.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Updated, please help to review when you free.

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 @@ -424,13 +422,6 @@ function riscv_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)
function riscv_f16Eq (v1, v2) = {
extern_f16Eq(v1, v2);
(float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit
val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool)
function riscv_f32Lt (v1, v2) = {
Expand Down Expand Up @@ -459,13 +450,6 @@ function riscv_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)
function riscv_f32Eq (v1, v2) = {
extern_f32Eq(v1, v2);
(float_fflags[4 .. 0], bit_to_bool(float_result[0]))
}

val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit
val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool)
function riscv_f64Lt (v1, v2) = {
Expand Down Expand Up @@ -494,13 +478,6 @@ function riscv_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)
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)
function riscv_f16roundToInt (rm, v, exact) = {
Expand Down
2 changes: 1 addition & 1 deletion sail-riscv.install

Large diffs are not rendered by default.