Float: Add floating-point equals API in sail model

Makefile

@@ -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

model/float/riscv_float_common.sail

@@ -0,0 +1,18 @@
+/*=======================================================================================*/
+/* 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

model/float/riscv_float_eq.sail

@@ -0,0 +1,41 @@
+/*=======================================================================================*/
+/* 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_snan
+ then float_flag_invalid
+ else zeros();
+ let is_equal = not(is_nan) & (op1 == op2) | ((op1 | op2) << 1) == zeros();
+
+ (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
+}

model/riscv_insts_dext.sail

@@ -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));

model/riscv_insts_fext.sail

@@ -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));

model/riscv_insts_vext_utils.sail

@@ -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 {

model/riscv_insts_vext_vm.sail

@@ -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])
  };
@@ -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),

model/riscv_insts_zfh.sail

@@ -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));

model/riscv_softfloat_interface.sail

@@ -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 */
 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 */
@@ -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) = {
@@ -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) = {
@@ -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) = {