Revert "Initial introduction of zfinx (#75)"

This reverts commit c5e62ea.

c_emulator/riscv_platform.c

@@ -18,9 +18,6 @@ bool sys_enable_next(unit u)
 bool sys_enable_fdext(unit u)
 { return rv_enable_fdext; }
 
-bool sys_enable_zfinx(unit u)
-{ return rv_enable_zfinx; }
-
 bool sys_enable_writable_misa(unit u)
 { return rv_enable_writable_misa; }
 

c_emulator/riscv_platform.h

@@ -4,7 +4,6 @@
 bool sys_enable_rvc(unit);
 bool sys_enable_next(unit);
 bool sys_enable_fdext(unit);
-bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
 
 bool plat_enable_dirty_update(unit);

c_emulator/riscv_platform_impl.c

@@ -4,7 +4,6 @@
 
 /* Settings of the platform implementation, with common defaults. */
 bool rv_enable_pmp                  = false;
-bool rv_enable_zfinx                = false;
 bool rv_enable_rvc                  = true;
 bool rv_enable_next                 = false;
 bool rv_enable_writable_misa        = true;

c_emulator/riscv_platform_impl.h

@@ -8,7 +8,6 @@
 #define DEFAULT_RSTVEC     0x00001000
 
 extern bool rv_enable_pmp;
-extern bool rv_enable_zfinx;
 extern bool rv_enable_rvc;
 extern bool rv_enable_next;
 extern bool rv_enable_fdext;

c_emulator/riscv_sim.c

@@ -127,7 +127,6 @@ static struct option options[] = {
   {"trace",                       optional_argument, 0, 'v'},
   {"no-trace",                    optional_argument, 0, 'V'},
   {"inst-limit",                  required_argument, 0, 'l'},
-  {"enable-zfinx",                no_argument,       0, 'x'},
 #ifdef SAILCOV
   {"sailcov-file",                required_argument, 0, 'c'},
 #endif
@@ -237,7 +236,6 @@ char *process_args(int argc, char **argv)
                     "V::"
                     "v::"
                     "l:"
-                    "x"
 #ifdef SAILCOV
                     "c:"
 #endif
@@ -327,10 +325,6 @@ char *process_args(int argc, char **argv)
     case 'l':
       insn_limit = atoi(optarg);
       break;
-    case 'x':
-      fprintf(stderr, "enabling Zfinx support.\n");
-      rv_enable_zfinx = true;
-      break;
 #ifdef SAILCOV
     case 'c':
       sailcov_file = strdup(optarg);

handwritten_support/0.11/riscv_extras.lem

@@ -87,10 +87,6 @@ val sys_enable_fdext : unit -> bool
 let sys_enable_fdext () = true
 declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`
 
-val sys_enable_zfinx : unit -> bool
-let sys_enable_zfinx () = false
-declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
-
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

handwritten_support/0.11/riscv_extras_sequential.lem

@@ -75,10 +75,6 @@ val sys_enable_rvc : unit -> bool
 let sys_enable_rvc () = true
 declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
 
-val sys_enable_zfinx : unit -> bool
-let sys_enable_zfinx () = false
-declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
-
 val sys_enable_next : unit -> bool
 let sys_enable_next () = true
 declare ocaml target_rep function sys_enable_next = `Platform.enable_next`

handwritten_support/riscv_extras.lem

@@ -155,10 +155,6 @@ val sys_enable_fdext : unit -> bool
 let sys_enable_fdext () = true
 declare ocaml target_rep function sys_enable_fdext = `Platform.enable_fdext`
 
-val sys_enable_zfinx : unit -> bool
-let sys_enable_zfinx () = false
-declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
-
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
 declare ocaml target_rep function plat_ram_base = `Platform.dram_base`

handwritten_support/riscv_extras_sequential.lem

@@ -143,10 +143,6 @@ val sys_enable_rvc : unit -> bool
 let sys_enable_rvc () = true
 declare ocaml target_rep function sys_enable_rvc = `Platform.enable_rvc`
 
-val sys_enable_zfinx : unit -> bool
-let sys_enable_zfinx () = false
-declare ocaml target_rep function sys_enable_zfinx = `Platform.enable_zfinx`
-
 val sys_enable_next : unit -> bool
 let sys_enable_next () = true
 declare ocaml target_rep function sys_enable_next = `Platform.enable_next`

model/riscv_fdext_regs.sail

@@ -73,41 +73,6 @@
 
 /* Original version written by Rishiyur S. Nikhil, Sept-Oct 2019    */
 
-/* **************************************************************** */
-/* NaN boxing/unboxing.                                             */
-/* When 32-bit floats (single-precision) are stored in 64-bit regs  */
-/* they must be 'NaN boxed' (upper 32b all ones).                   */
-/* When 32-bit floats (single-precision) are read from 64-bit regs  */
-/* they must be 'NaN unboxed'.                                      */
-
-function canonical_NaN_S() -> bits(32) = 0x_7fc0_0000
-function canonical_NaN_D() -> bits(64) = 0x_7ff8_0000_0000_0000
-
-val nan_unbox_do : (bool, bits(64)) -> bits(32)
-function nan_unbox_do (zfinx_en, regval) =
-  if zfinx_en
-    then regval [31..0]
-  else if regval [63..32] == 0x_FFFF_FFFF
-    then regval [31..0]
-  else canonical_NaN_S()
-
-val nan_unbox_pass : (bool, bits(32)) -> bits(32)
-function nan_unbox_pass (zfinx_en, regval) =
-  regval
-
-val nan_box_do : (bool, bits(32)) -> bits(64)
-function nan_box_do (zfinx_en, regval) =
-  0x_FFFF_FFFF @ regval
-
-
-val nan_box_pass : (bool, bits(32)) -> bits(32)
-function nan_box_pass (zfinx_en, regval) =
-  regval
-
-overload nan_unbox = { nan_unbox_do, nan_unbox_pass }
-overload nan_box = { nan_box_do, nan_box_pass }
-
-
 /* **************************************************************** */
 /* Floating point register file                                     */
 
@@ -245,58 +210,6 @@ function wF_bits(i: bits(5), data: flenbits) -> unit = {
 
 overload F = {rF_bits, wF_bits, rF, wF}
 
-/* ---- Register Read/ Writes */
-
-val rX_or_F_32 : (bool, bits(5)) -> bits(32) effect {escape, rreg}
-function rX_or_F_32(zfinx_en, i) = {
-  if zfinx_en then
-    nan_unbox(zfinx_en, rX(unsigned(i)))
-  else
-    nan_unbox(zfinx_en, rF(unsigned(i)))
-}
-
-val rX_or_F_64 : (bool, bits(5)) -> bits(64) effect {escape, rreg}
-function rX_or_F_64(zfinx_en, i) = {
-  assert (zfinx_en | sizeof(flen) == 64);
-  if zfinx_en & sizeof (xlen) == 32 then {
-    assert (i[0] == bitzero);
-    if i == 0b00000 then
-      sail_zeros(64)
-    else rX(unsigned(i+1)) @ rX(unsigned(i))
-  }
-  else if zfinx_en & sizeof(xlen) == 64 then
-    rX(unsigned(i))
-  else
-    rF(unsigned(i))
-}
-
-val wX_or_F_64 : (bool, bits(5), bits(64)) -> unit effect {escape, wreg}
-function wX_or_F_64(zfinx_en: bool, i: bits(5), data: bits(64)) = {
-  assert (zfinx_en | sizeof(flen) == 64);
-  if zfinx_en & sizeof(xlen) == 32 then {
-    assert (i[0] == bitzero);
-    if i != 0b00000 then {
-      wX(unsigned(i)) = data[31..0];
-      wX(unsigned(i+1)) = data[63..32];
-    }
-  }
-  else if zfinx_en & sizeof (xlen) == 64 then
-    wX(unsigned(i)) = data
-  else if ~ (zfinx_en) & sizeof (flen) == 64 then
-    wF(unsigned(i)) = data
-}
-
-val wX_or_F_32 : (bool, bits(5), bits(32)) -> unit effect {escape, wreg}
-function wX_or_F_32(zfinx_en: bool, i: bits(5), data : bits(32)) = {
-  if zfinx_en then
-    wX(unsigned(i)) = nan_box(zfinx_en, data)
-  else
-    wF(unsigned(i)) = nan_box(zfinx_en, data)
-}
-
-overload X_or_F_S = { rX_or_F_32, wX_or_F_32 }
-overload X_or_F_D = { rX_or_F_64, wX_or_F_64 }
-
 /* register names */
 
 val freg_name_abi : regidx <-> string
@@ -376,12 +289,6 @@ mapping freg_name = {
     0b11111 <-> "ft11"
 }
 
-val reg_or_freg_name : bits(5) <-> string
-mapping reg_or_freg_name = {
-  reg if sys_enable_zfinx()     <-> reg_name(reg)  if sys_enable_zfinx(),
-  reg if ~ (sys_enable_zfinx()) <-> freg_name(reg) if ~ (sys_enable_zfinx())
-}
-
 val init_fdext_regs : unit -> unit effect {wreg}
 function init_fdext_regs () = {
   f0  = zero_freg;
@@ -437,13 +344,13 @@ function ext_write_fcsr (frm, fflags) = {
   fcsr->FRM()    = frm;      /* Note: frm can be an illegal value, 101, 110, 111 */
   fcsr->FFLAGS() = fflags;
   update_softfloat_fflags(fflags);
-  if ~ (sys_enable_zfinx()) then dirty_fd_context();
+  dirty_fd_context();
 }
 
 /* called for softfloat paths (softfloat flags are consistent) */
 val write_fflags : (bits(5)) -> unit effect {rreg, wreg}
 function write_fflags(fflags) = {
-  if   fcsr.FFLAGS() != fflags & ~ (sys_enable_zfinx())
+  if   fcsr.FFLAGS() != fflags
   then dirty_fd_context();
   fcsr->FFLAGS() = fflags;
 }
@@ -456,6 +363,6 @@ function accrue_fflags(flags) = {
   then {
     fcsr->FFLAGS() = f;
     update_softfloat_fflags(f);
-    if ~ (sys_enable_zfinx()) then dirty_fd_context();
+    dirty_fd_context();
   }
 }

model/riscv_insts_cdext.sail

@@ -77,9 +77,9 @@
 union clause ast = C_FLDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b001 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FLDSP(uimm, rd)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -95,9 +95,9 @@ mapping clause assembly = C_FLDSP(uimm, rd)
 union clause ast = C_FSDSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b101 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FSDSP(uimm, rs2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -113,9 +113,9 @@ mapping clause assembly = C_FSDSP(uimm, rs2)
 union clause ast = C_FLD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b001 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FLD(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);
@@ -133,9 +133,9 @@ mapping clause assembly = C_FLD(uimm, rsc, rdc)
 union clause ast = C_FSD : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2)
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
   <-> 0b101 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00
-      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() & ~ (sys_enable_zfinx())
+      if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt()
 
 function clause execute (C_FSD(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b000);

model/riscv_insts_cfext.sail

@@ -77,9 +77,9 @@
 union clause ast = C_FLWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui42 : bits(3) @ ui76 : bits(2) @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FLWSP(imm, rd)) = {
   let imm : bits(12) = EXTZ(imm @ 0b00);
@@ -95,9 +95,9 @@ mapping clause assembly = C_FLWSP(imm, rd)
 union clause ast = C_FSWSP : (bits(6), regidx)
 
 mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b111 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FSWSP(uimm, rs2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -113,9 +113,9 @@ mapping clause assembly = C_FSWSP(uimm, rd)
 union clause ast = C_FLW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FLW(uimm, rsc, rdc)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);
@@ -133,9 +133,9 @@ mapping clause assembly = C_FLW(uimm, rsc, rdc)
 union clause ast = C_FSW : (bits(5), cregidx, cregidx)
 
 mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2)
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
   <-> 0b111 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00
-      if sizeof(xlen) == 32 & haveRVC() & haveFExt() & ~ (sys_enable_zfinx())
+      if sizeof(xlen) == 32 & haveRVC() & haveFExt()
 
 function clause execute (C_FSW(uimm, rsc1, rsc2)) = {
   let imm : bits(12) = EXTZ(uimm @ 0b00);