Add Zfa extension support (excl. quad-precision)

This commit adds the following:
- infrastructure for Zfa (e.g., existence macro)
- support for the following instructions:
  + FLI.[HSD]
  + FMINM.[HSD] and FMAXM.[HSD]
  + FROUND.[HSD] and FROUNDNX.[HSD]
  + FMVH.X.D and FMVP.D.X
  + FLEQ.[HSD] and FLTQ.[HSD]
  + FCVTMOD.W.D

Note the following implementation details:

FMINM and FMAXM provide similar functionality to FMIN and FMAX,
differing only in their NaN-handling:
 * FMIN/FMAX return a canonical NaN only if both operands are a NaN
 * FMINM/FMAXM return a canonical Nan if any operand is a NaN
Consequently, the implementation is identical to FMIN/FMAX with only
the NaN-related tests changed.

FROUND instruction rounds a floating-point number in floating-point
register rs1 and writes that integer, represented as a floating-point
number to floating-point register rd while:
* Zero and infinite inputs are copied to rd unmodified.
* NaN inputs cause the invalid operation exception flag to be set.
FROUNDNX instruction is defined similarly, but also sets the inexact
exception flag if the input differs from the rounded result and is not
NaN.

FMVH.X.D instruction is available for RV32 only and moves bits 63:32
of floating-point register rs1 into integer register rd.

FMVP.D.X instruction is available for RV32 only and moves a
double-precision number from a pair of integer registers into a
floating-point register. Integer registers rs1 and rs2 supply bits
31:0 and 63:32, respectively.

FLEQ and FLTQ instructions are defined like the FLE and FLT
instructions, except that quiet NaN inputs do not cause the invalid
operation exception flag to be set.

The FCVTMOD.W.D instruction is defined similarly to the FCVT.W.D
instruction, with the following differences:
 * FCVTMOD.W.D always rounds towards zero.
 * Bits 31:0 are taken from the rounded, unbounded two's complement
   result, then sign-extended to XLEN bits and written to integer
   register rd.
 * Positive infinity, negative infinity and NaN are converted to zero.

Signed-off-by: Charalampos Mitrodimas <[email protected]>
Signed-off-by: Philipp Tomsich <[email protected]>

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

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;
+}

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

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

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 {