diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 4b4a28ebb..e6732aae5 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -215,76 +215,34 @@ overload F_box = { rF_box, wF_box } // Access functions that access X registers if Zfinx (float in X) is enabled // (mutually exclusive with the F/D extensions), otherwise F registers. -val rF_or_X_H : regidx -> bits(16) -function rF_or_X_H(i) = { - assert(sizeof(flen) >= 16); - assert(sys_enable_fdext() != sys_enable_zfinx()); - if sys_enable_fdext() - then F_box(i) - else X(i)[15..0] -} - -val rF_or_X_S : regidx -> bits(32) -function rF_or_X_S(i) = { - assert(sizeof(flen) >= 32); - assert(sys_enable_fdext() != sys_enable_zfinx()); - if sys_enable_fdext() - then F_box(i) - else X(i)[31..0] -} - -val rF_or_X_D : regidx -> bits(64) -function rF_or_X_D(i) = { - assert(sizeof(flen) >= 64); +val rF_or_X : forall 'n, 'n in {16, 32, 64} . (implicit('n), regidx) -> bits('n) +function rF_or_X(_n, i) = { + assert(sizeof(flen) >= 'n); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_box(i) - else if sizeof(xlen) >= 64 - then X(i)[63..0] - else { + else if sizeof(xlen) == 32 & 'n == 64 then { assert(i[0] == bitzero); if i == zeros() then zeros() else X(i + 1) @ X(i) - } + } else X(i)['n - 1 .. 0] } -val wF_or_X_H : (regidx, bits(16)) -> unit -function wF_or_X_H(i, data) = { - assert(sizeof(flen) >= 16); - assert(sys_enable_fdext() != sys_enable_zfinx()); - if sys_enable_fdext() - then F_box(i) = data - else X(i) = sign_extend(data) -} - -val wF_or_X_S : (regidx, bits(32)) -> unit -function wF_or_X_S(i, data) = { - assert(sizeof(flen) >= 32); - assert(sys_enable_fdext() != sys_enable_zfinx()); - if sys_enable_fdext() - then F_box(i) = data - else X(i) = sign_extend(data) -} - -val wF_or_X_D : (regidx, bits(64)) -> unit -function wF_or_X_D(i, data) = { - assert (sizeof(flen) >= 64); +val wF_or_X : forall 'n, 'n in {16, 32, 64} . (regidx, bits('n)) -> unit +function wF_or_X(i, data) = { + assert(sizeof(flen) >= 'n); assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_box(i) = data - else if sizeof(xlen) >= 64 - then X(i) = sign_extend(data) - else { + else if sizeof(xlen) == 32 & 'n == 64 then { assert (i[0] == bitzero); if i != zeros() then { X(i) = data[31..0]; X(i + 1) = data[63..32]; } - } + } else X(i) = sign_extend(data) } -overload F_or_X_H = { rF_or_X_H, wF_or_X_H } -overload F_or_X_S = { rF_or_X_S, wF_or_X_S } -overload F_or_X_D = { rF_or_X_D, wF_or_X_D } +overload F_or_X = { rF_or_X, wF_or_X } /* register names */ diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 1ddc51288..9ce22a0be 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -80,9 +80,9 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { - let rs1_val_64b = F_or_X_D(rs1); - let rs2_val_64b = F_or_X_D(rs2); - let rs3_val_64b = F_or_X_D(rs3); + let rs1_val_64b = F_or_X(64, rs1); + let rs2_val_64b = F_or_X(64, rs2); + let rs3_val_64b = F_or_X(64, rs3); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -96,7 +96,7 @@ function clause execute (F_MADD_TYPE_D(rs3, rs2, rs1, rm, rd, op)) = { FNMADD_D => riscv_f64MulAdd (rm_3b, f_negate (rs1_val_64b), rs2_val_64b, f_negate (rs3_val_64b)) }; accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_64b; + F_or_X(rd) = rd_val_64b; RETIRE_SUCCESS } } @@ -147,8 +147,8 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = { - let rs1_val_64b = F_or_X_D(rs1); - let rs2_val_64b = F_or_X_D(rs2); + let rs1_val_64b = F_or_X(64, rs1); + let rs2_val_64b = F_or_X(64, rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -160,7 +160,7 @@ function clause execute (F_BIN_RM_TYPE_D(rs2, rs1, rm, rd, op)) = { FDIV_D => riscv_f64Div (rm_3b, rs1_val_64b, rs2_val_64b) }; accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_64b; + F_or_X(rd) = rd_val_64b; RETIRE_SUCCESS } } @@ -240,7 +240,7 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -248,14 +248,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FSQRT_D)) = { let (fflags, rd_val_D) = riscv_f64Sqrt (rm_3b, rs1_val_D); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -270,7 +270,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = { - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -293,7 +293,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_W)) = { let (fflags, rd_val_D) = riscv_i32ToF64 (rm_3b, rs1_val_W); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -308,14 +308,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_WU)) = { let (fflags, rd_val_D) = riscv_ui32ToF64 (rm_3b, rs1_val_WU); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -323,14 +323,14 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_S_D)) = { let (fflags, rd_val_S) = riscv_f64ToF32 (rm_3b, rs1_val_D); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -338,7 +338,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { let (fflags, rd_val_D) = riscv_f32ToF64 (rm_3b, rs1_val_S); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -346,7 +346,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_S)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { assert(sizeof(xlen) >= 64); - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -362,7 +362,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { assert(sizeof(xlen) >= 64); - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -386,7 +386,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = { let (fflags, rd_val_D) = riscv_i64ToF64 (rm_3b, rs1_val_L); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -402,7 +402,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = { let (fflags, rd_val_D) = riscv_ui64ToF64 (rm_3b, rs1_val_LU); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -528,42 +528,42 @@ mapping clause encdec = F_BIN_TYPE_D(rs2, rs1, rd, FLE_D) if hav /* Execution semantics ================================ */ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJ_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let (s1, e1, m1) = fsplit (rs1_val_D); let (s2, e2, m2) = fsplit (rs2_val_D); let rd_val_D = fmake (s2, e1, m1); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJN_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let (s1, e1, m1) = fsplit (rs1_val_D); let (s2, e2, m2) = fsplit (rs2_val_D); let rd_val_D = fmake (0b1 ^ s2, e1, m1); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FSGNJX_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let (s1, e1, m1) = fsplit (rs1_val_D); let (s2, e2, m2) = fsplit (rs2_val_D); let rd_val_D = fmake (s1 ^ s2, e1, m1); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle(rs1_val_D, rs2_val_D, is_quiet); @@ -577,13 +577,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMIN_D)) = { else /* (not rs1_lt_rs2) */ rs2_val_D; accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle(rs2_val_D, rs1_val_D, is_quiet); @@ -597,13 +597,13 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FMAX_D)) = { else /* (not rs2_lt_rs1) */ rs2_val_D; accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } 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 rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Eq (rs1_val_D, rs2_val_D); @@ -614,8 +614,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Lt (rs1_val_D, rs2_val_D); @@ -626,8 +626,8 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { } function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = { - let rs1_val_D = F_or_X_D(rs1); - let rs2_val_D = F_or_X_D(rs2); + let rs1_val_D = F_or_X(64, rs1); + let rs2_val_D = F_or_X(64, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f64Le (rs1_val_D, rs2_val_D); @@ -719,7 +719,7 @@ mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if /* Execution semantics ================================ */ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); let rd_val_10b : bits (10) = if f_is_neg_inf (rs1_val_D) then 0b_00_0000_0001 diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 0888811f1..006dd70c3 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -250,9 +250,9 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = { - let rs1_val_32b = F_or_X_S(rs1); - let rs2_val_32b = F_or_X_S(rs2); - let rs3_val_32b = F_or_X_S(rs3); + let rs1_val_32b = F_or_X(32, rs1); + let rs2_val_32b = F_or_X(32, rs2); + let rs3_val_32b = F_or_X(32, rs3); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -265,7 +265,7 @@ function clause execute (F_MADD_TYPE_S(rs3, rs2, rs1, rm, rd, op)) = { FNMADD_S => riscv_f32MulAdd (rm_3b, f_negate (rs1_val_32b), rs2_val_32b, f_negate (rs3_val_32b)) }; accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_32b; + F_or_X(rd) = rd_val_32b; RETIRE_SUCCESS } } @@ -316,8 +316,8 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = { - let rs1_val_32b = F_or_X_S(rs1); - let rs2_val_32b = F_or_X_S(rs2); + let rs1_val_32b = F_or_X(32, rs1); + let rs2_val_32b = F_or_X(32, rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -329,7 +329,7 @@ function clause execute (F_BIN_RM_TYPE_S(rs2, rs1, rm, rd, op)) = { FDIV_S => riscv_f32Div (rm_3b, rs1_val_32b, rs2_val_32b) }; accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_32b; + F_or_X(rd) = rd_val_32b; RETIRE_SUCCESS } } @@ -401,7 +401,7 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = { - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -409,14 +409,14 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FSQRT_S)) = { let (fflags, rd_val_S) = riscv_f32Sqrt (rm_3b, rs1_val_S); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -431,7 +431,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = { - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -454,7 +454,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_W)) = { let (fflags, rd_val_S) = riscv_i32ToF32 (rm_3b, rs1_val_W); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } @@ -469,7 +469,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = { let (fflags, rd_val_S) = riscv_ui32ToF32 (rm_3b, rs1_val_WU); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } @@ -477,7 +477,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_WU)) = { function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = { assert(sizeof(xlen) >= 64); - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -493,7 +493,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = { function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = { assert(sizeof(xlen) >= 64); - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -517,7 +517,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = { let (fflags, rd_val_S) = riscv_i64ToF32 (rm_3b, rs1_val_L); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } @@ -533,7 +533,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = { let (fflags, rd_val_S) = riscv_ui64ToF32 (rm_3b, rs1_val_LU); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } @@ -645,41 +645,41 @@ mapping clause encdec = F_BIN_TYPE_S(rs2, rs1, rd, FLE_S) if hav /* Execution semantics ================================ */ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJ_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let (s1, e1, m1) = fsplit (rs1_val_S); let (s2, e2, m2) = fsplit (rs2_val_S); let rd_val_S = fmake (s2, e1, m1); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJN_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let (s1, e1, m1) = fsplit (rs1_val_S); let (s2, e2, m2) = fsplit (rs2_val_S); let rd_val_S = fmake (0b1 ^ s2, e1, m1); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FSGNJX_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let (s1, e1, m1) = fsplit (rs1_val_S); let (s2, e2, m2) = fsplit (rs2_val_S); let rd_val_S = fmake (s1 ^ s2, e1, m1); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle(rs1_val_S, rs2_val_S, is_quiet); @@ -693,13 +693,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMIN_S)) = { else /* (not rs1_lt_rs2) */ rs2_val_S; accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle(rs2_val_S, rs1_val_S, is_quiet); @@ -713,13 +713,13 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FMAX_S)) = { else /* (not rs2_lt_rs1) */ rs2_val_S; accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } 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 rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Eq (rs1_val_S, rs2_val_S); @@ -730,8 +730,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Lt (rs1_val_S, rs2_val_S); @@ -742,8 +742,8 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = { } function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = { - let rs1_val_S = F_or_X_S(rs1); - let rs2_val_S = F_or_X_S(rs2); + let rs1_val_S = F_or_X(32, rs1); + let rs2_val_S = F_or_X(32, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f32Le (rs1_val_S, rs2_val_S); @@ -833,7 +833,7 @@ mapping clause encdec = F_UN_TYPE_S(rs1, rd, FMV_W_X) if /* Execution semantics ================================ */ function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = { - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); let rd_val_10b : bits (10) = if f_is_neg_inf (rs1_val_S) then 0b_00_0000_0001 diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 5b6d28de0..b2585641b 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -441,11 +441,7 @@ function read_vreg_seg(num_elem, SEW, LMUL_pow, nf, vrid) = { val get_scalar_fp : forall 'n, 'n in {16, 32, 64}. (regidx, int('n)) -> bits('n) function get_scalar_fp(rs1, SEW) = { assert(sizeof(flen) >= SEW, "invalid vector floating-point type width: FLEN < SEW"); - match SEW { - 16 => F_box(rs1), - 32 => F_box(rs1), - 64 => F_box(rs1) - } + F_box(rs1) } /* Shift amounts */ diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 8b0301ace..334eccc08 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -63,8 +63,8 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)) = { - let rs1_val_16b = F_or_X_H(rs1); - let rs2_val_16b = F_or_X_H(rs2); + let rs1_val_16b = F_or_X(16, rs1); + let rs2_val_16b = F_or_X(16, rs2); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -76,7 +76,7 @@ function clause execute (F_BIN_RM_TYPE_H(rs2, rs1, rm, rd, op)) = { FDIV_H => riscv_f16Div (rm_3b, rs1_val_16b, rs2_val_16b) }; accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_16b; + F_or_X(rd) = rd_val_16b; RETIRE_SUCCESS } } @@ -126,9 +126,9 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = { - let rs1_val_16b = F_or_X_H(rs1); - let rs2_val_16b = F_or_X_H(rs2); - let rs3_val_16b = F_or_X_H(rs3); + let rs1_val_16b = F_or_X(16, rs1); + let rs2_val_16b = F_or_X(16, rs2); + let rs3_val_16b = F_or_X(16, rs3); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -141,7 +141,7 @@ function clause execute (F_MADD_TYPE_H(rs3, rs2, rs1, rm, rd, op)) = { FNMADD_H => riscv_f16MulAdd (rm_3b, f_negate (rs1_val_16b), rs2_val_16b, f_negate (rs3_val_16b)) }; accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_16b; + F_or_X(rd) = rd_val_16b; RETIRE_SUCCESS } } @@ -200,41 +200,41 @@ mapping clause encdec = F_BIN_TYPE_H(rs2, rs1, rd, FLE_H) if hav /* Execution semantics ================================ */ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJ_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let (s1, e1, m1) = fsplit (rs1_val_H); let (s2, e2, m2) = fsplit (rs2_val_H); let rd_val_H = fmake (s2, e1, m1); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJN_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let (s1, e1, m1) = fsplit (rs1_val_H); let (s2, e2, m2) = fsplit (rs2_val_H); let rd_val_H = fmake (0b1 ^ s2, e1, m1); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FSGNJX_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let (s1, e1, m1) = fsplit (rs1_val_H); let (s2, e2, m2) = fsplit (rs2_val_H); let rd_val_H = fmake (s1 ^ s2, e1, m1); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let is_quiet = true; let (rs1_lt_rs2, fflags) = fle(rs1_val_H, rs2_val_H, is_quiet); @@ -248,13 +248,13 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMIN_H)) = { else /* (not rs1_lt_rs2) */ rs2_val_H; accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let is_quiet = true; let (rs2_lt_rs1, fflags) = fle(rs2_val_H, rs1_val_H, is_quiet); @@ -268,13 +268,13 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FMAX_H)) = { else /* (not rs2_lt_rs1) */ rs2_val_H; accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } 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 rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f16Eq (rs1_val_H, rs2_val_H); @@ -285,8 +285,8 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = { } function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f16Lt (rs1_val_H, rs2_val_H); @@ -297,8 +297,8 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = { } function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)) = { - let rs1_val_H = F_or_X_H(rs1); - let rs2_val_H = F_or_X_H(rs2); + let rs1_val_H = F_or_X(16, rs1); + let rs2_val_H = F_or_X(16, rs2); let (fflags, rd_val) : (bits_fflags, bool) = riscv_f16Le (rs1_val_H, rs2_val_H); @@ -438,7 +438,7 @@ mapping clause encdec = /* Execution semantics ================================ */ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = { - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -446,14 +446,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FSQRT_H)) = { let (fflags, rd_val_H) = riscv_f16Sqrt (rm_3b, rs1_val_H); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = { - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -468,7 +468,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = { } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)) = { - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -491,7 +491,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_W)) = { let (fflags, rd_val_H) = riscv_i32ToF16 (rm_3b, rs1_val_W); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } @@ -506,14 +506,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_WU)) = { let (fflags, rd_val_H) = riscv_ui32ToF16 (rm_3b, rs1_val_WU); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = { - let rs1_val_S = F_or_X_S(rs1); + let rs1_val_S = F_or_X(32, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -521,14 +521,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_S)) = { let (fflags, rd_val_H) = riscv_f32ToF16 (rm_3b, rs1_val_S); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = { - let rs1_val_D = F_or_X_D(rs1); + let rs1_val_D = F_or_X(64, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -536,14 +536,14 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_D)) = { let (fflags, rd_val_H) = riscv_f64ToF16 (rm_3b, rs1_val_D); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -551,7 +551,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { let (fflags, rd_val_S) = riscv_f16ToF32 (rm_3b, rs1_val_H); accrue_fflags(fflags); - F_or_X_S(rd) = rd_val_S; + F_or_X(rd) = rd_val_S; RETIRE_SUCCESS } } @@ -559,7 +559,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_S_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = { - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -567,7 +567,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = { let (fflags, rd_val_D) = riscv_f16ToF64 (rm_3b, rs1_val_H); accrue_fflags(fflags); - F_or_X_D(rd) = rd_val_D; + F_or_X(rd) = rd_val_D; RETIRE_SUCCESS } } @@ -575,7 +575,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_D_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = { assert(sizeof(xlen) >= 64); - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -591,7 +591,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = { function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)) = { assert(sizeof(xlen) >= 64); - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, Some(rm') => { @@ -615,7 +615,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)) = { let (fflags, rd_val_H) = riscv_i64ToF16 (rm_3b, rs1_val_L); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } @@ -631,7 +631,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)) = { let (fflags, rd_val_H) = riscv_ui64ToF16 (rm_3b, rs1_val_LU); accrue_fflags(fflags); - F_or_X_H(rd) = rd_val_H; + F_or_X(rd) = rd_val_H; RETIRE_SUCCESS } } @@ -754,7 +754,7 @@ mapping clause encdec = F_UN_TYPE_H(rs1, rd, FMV_H_X) if /* Execution semantics ================================ */ function clause execute (F_UN_TYPE_H(rs1, rd, FCLASS_H)) = { - let rs1_val_H = F_or_X_H(rs1); + let rs1_val_H = F_or_X(16, rs1); let rd_val_10b : bits (10) = if f_is_neg_inf (rs1_val_H) then 0b_00_0000_0001