Merge pull request #251 from riscv/vrull/zfa

Add Zfa support (excl. quad-precision instructions)
riscv · May 29, 2023 · 917e6c0 · 917e6c0
2 parents c57aebc + 2cd4a17
commit 917e6c0
Show file tree

Hide file tree

Showing 9 changed files with 1,067 additions and 6 deletions.
diff --git a/Makefile b/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

diff --git a/c_emulator/riscv_softfloat.c b/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;
+}
diff --git a/c_emulator/riscv_softfloat.h b/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);
diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/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 _ _ _ = ()
diff --git a/model/riscv_fdext_regs.sail b/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 {