1 files changed, 52 insertions, 0 deletions
diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail
new file mode 100644
index 0000000..3b099db
--- /dev/null
+++ b/model/riscv_freg_type.sail
@@ -0,0 +1,52 @@
+/* Definitions for floating point registers (F and D extensions) */
+
+/* default register type */
+type fregtype = flenbits
+
+/* default zero register */
+let zero_freg : fregtype = EXTZ(0x0)
+
+/* default register printer */
+val FRegStr : fregtype -> string
+function FRegStr(r) = BitStr(r)
+
+/* conversions */
+
+val fregval_from_freg : fregtype -> flenbits
+function fregval_from_freg(r) = r
+
+val fregval_into_freg : flenbits -> fregtype
+function fregval_into_freg(v) = v
+
+
+/* Rounding Mode
+    Rounding modes occur as a 3-bit field in F,D instructions,
+    and also as a 3-bit 'frm' field in the 'fcsr' CSR.
+    RISC-V uses the following IEEE-defined rounding modes.
+*/
+
+enum rounding_mode = {RM_RNE, RM_RTZ, RM_RDN, RM_RUP, RM_RMM, RM_DYN}
+
+enum f_madd_op_S = {FMADD_S, FMSUB_S, FNMSUB_S, FNMADD_S}
+
+enum f_bin_rm_op_S = {FADD_S, FSUB_S, FMUL_S, FDIV_S}
+
+enum f_un_rm_op_S = {FSQRT_S, FCVT_W_S, FCVT_WU_S, FCVT_S_W, FCVT_S_WU,    // RV32 and RV64
+                     FCVT_L_S, FCVT_LU_S, FCVT_S_L, FCVT_S_LU}             // RV64 only
+
+enum f_un_op_S = {FCLASS_S, FMV_X_W, FMV_W_X}    /* RV32 and RV64 */
+
+enum f_bin_op_S = {FSGNJ_S, FSGNJN_S, FSGNJX_S, FMIN_S, FMAX_S, FEQ_S, FLT_S, FLE_S}
+
+enum f_madd_op_D = {FMADD_D, FMSUB_D, FNMSUB_D, FNMADD_D}
+
+enum f_bin_rm_op_D = {FADD_D, FSUB_D, FMUL_D, FDIV_D}
+
+enum f_un_rm_op_D = {FSQRT_D, FCVT_W_D, FCVT_WU_D, FCVT_D_W, FCVT_D_WU,    // RV32 and RV64
+                     FCVT_S_D, FCVT_D_S,
+                     FCVT_L_D, FCVT_LU_D, FCVT_D_L, FCVT_D_LU}             // RV64 only
+
+enum f_bin_op_D = {FSGNJ_D, FSGNJN_D, FSGNJX_D, FMIN_D, FMAX_D, FEQ_D, FLT_D, FLE_D}
+
+enum f_un_op_D = {FCLASS_D,            /* RV32 and RV64 */
+                  FMV_X_D, FMV_D_X}    /* RV64 only */