diff --git a/Makefile b/Makefile
index deaad558f..f1d3dd845 100644
--- a/Makefile
+++ b/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
diff --git a/model/float/riscv_float_common.sail b/model/float/riscv_float_common.sail
new file mode 100644
index 000000000..f3e991d18
--- /dev/null
+++ b/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
diff --git a/model/float/riscv_float_eq.sail b/model/float/riscv_float_eq.sail
new file mode 100644
index 000000000..54128ce8b
--- /dev/null
+++ b/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
+}
diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
index 58c5d5d96..77569ae9d 100644
--- a/model/riscv_insts_dext.sail
+++ b/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));
diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
index e4afb30d5..af55c50c7 100644
--- a/model/riscv_insts_fext.sail
+++ b/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));
diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
index 52b7c647e..cf28df71f 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/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 {
diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
index 1f963e771..99607441d 100755
--- a/model/riscv_insts_vext_vm.sail
+++ b/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),
diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail
index 5522bad22..dbccdd27b 100644
--- a/model/riscv_insts_zfh.sail
+++ b/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));
diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail
index 3a673feb8..68d41a212 100644
--- a/model/riscv_softfloat_interface.sail
+++ b/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) = {
diff --git a/sail-riscv.install b/sail-riscv.install
index 7a539dfb5..99978c4e4 100644
--- a/sail-riscv.install
+++ b/sail-riscv.install
@@ -1,2 +1,2 @@
 bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]
-share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]
+share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/float/riscv_float_common.sail" {"model/float/riscv_float_common.sail"} "model/float/riscv_float_eq.sail" {"model/float/riscv_float_eq.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]