diff --git a/model/main.sail b/model/main.sail index 1422635be..9e0357c29 100644 --- a/model/main.sail +++ b/model/main.sail @@ -15,7 +15,7 @@ $ifdef SYMBOLIC $include -function get_entry_point() = to_bits(sizeof(xlen), elf_entry()) +function get_entry_point() = to_bits(xlen, elf_entry()) $else diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index 63652da88..51a59cd68 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -278,7 +278,7 @@ function rF_or_X_D(i) = { assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_D(i) - else if sizeof(xlen) >= 64 + else if xlen >= 64 then X(i)[63..0] else { assert(i[0] == bitzero); @@ -310,7 +310,7 @@ function wF_or_X_D(i, data) = { assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_D(i) = data - else if sizeof(xlen) >= 64 + else if xlen >= 64 then X(i) = sign_extend(data) else { assert (i[0] == bitzero); diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 18c047e49..c3e5a572a 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -38,7 +38,7 @@ function lrsc_width_str(width : word_width) -> string = function lrsc_width_valid(size : word_width) -> bool = { match size { WORD => true, - DOUBLE => sizeof(xlen) >= 64, + DOUBLE => xlen >= 64, _ => false } } @@ -48,7 +48,7 @@ function amo_width_valid(size : word_width) -> bool = { BYTE => extensionEnabled(Ext_Zabha), HALF => extensionEnabled(Ext_Zabha), WORD => true, - DOUBLE => sizeof(xlen) >= 64, + DOUBLE => xlen >= 64, } } diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 438fa15d0..9c180bc0d 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -211,21 +211,21 @@ mapping encdec_sop : sop <-> bits(3) = { RISCV_SRAI <-> 0b101 } -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero -mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if sizeof(xlen) == 64 | shamt[5] == bitzero +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SLLI) <-> 0b000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == bitzero +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRLI) <-> 0b000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == bitzero +mapping clause encdec = SHIFTIOP(shamt, rs1, rd, RISCV_SRAI) <-> 0b010000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if xlen == 64 | shamt[5] == bitzero function clause execute (SHIFTIOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); /* the decoder guard should ensure that shamt[5] = 0 for RV32 */ let result : xlenbits = match op { - RISCV_SLLI => if sizeof(xlen) == 32 + RISCV_SLLI => if xlen == 32 then rs1_val << shamt[4..0] else rs1_val << shamt, - RISCV_SRLI => if sizeof(xlen) == 32 + RISCV_SRLI => if xlen == 32 then rs1_val >> shamt[4..0] else rs1_val >> shamt, - RISCV_SRAI => if sizeof(xlen) == 32 + RISCV_SRAI => if xlen == 32 then shift_right_arith32(rs1_val, shamt[4..0]) else shift_right_arith64(rs1_val, shamt) }; @@ -266,14 +266,14 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = { RISCV_AND => rs1_val & rs2_val, RISCV_OR => rs1_val | rs2_val, RISCV_XOR => rs1_val ^ rs2_val, - RISCV_SLL => if sizeof(xlen) == 32 + RISCV_SLL => if xlen == 32 then rs1_val << (rs2_val[4..0]) else rs1_val << (rs2_val[5..0]), - RISCV_SRL => if sizeof(xlen) == 32 + RISCV_SRL => if xlen == 32 then rs1_val >> (rs2_val[4..0]) else rs1_val >> (rs2_val[5..0]), RISCV_SUB => rs1_val - rs2_val, - RISCV_SRA => if sizeof(xlen) == 32 + RISCV_SRA => if xlen == 32 then shift_right_arith32(rs1_val, rs2_val[4..0]) else shift_right_arith64(rs1_val, rs2_val[5..0]) }; @@ -417,9 +417,9 @@ mapping clause assembly = STORE(imm, rs2, rs1, size, aq, rl) union clause ast = ADDIW : (bits(12), regidx, regidx) mapping clause encdec = ADDIW(imm, rs1, rd) - if sizeof(xlen) == 64 + if xlen == 64 <-> imm @ rs1 @ 0b000 @ rd @ 0b0011011 - if sizeof(xlen) == 64 + if xlen == 64 function clause execute (ADDIW(imm, rs1, rd)) = { let result : xlenbits = sign_extend(imm) + X(rs1); @@ -428,33 +428,33 @@ function clause execute (ADDIW(imm, rs1, rd)) = { } mapping clause assembly = ADDIW(imm, rs1, rd) - if sizeof(xlen) == 64 + if xlen == 64 <-> "addiw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = RTYPEW : (regidx, regidx, regidx, ropw) mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_ADDW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SUBW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0100000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SLLW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRLW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0000000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if xlen == 64 mapping clause encdec = RTYPEW(rs2, rs1, rd, RISCV_SRAW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0100000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 - if sizeof(xlen) == 64 + if xlen == 64 function clause execute (RTYPEW(rs2, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -479,25 +479,25 @@ mapping rtypew_mnemonic : ropw <-> string = { } mapping clause assembly = RTYPEW(rs2, rs1, rd, op) - if sizeof(xlen) == 64 + if xlen == 64 <-> rtypew_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = SHIFTIWOP : (bits(5), regidx, regidx, sopw) mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SLLIW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 - if sizeof(xlen) == 64 + if xlen == 64 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRLIW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0000000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if sizeof(xlen) == 64 + if xlen == 64 mapping clause encdec = SHIFTIWOP(shamt, rs1, rd, RISCV_SRAIW) - if sizeof(xlen) == 64 + if xlen == 64 <-> 0b0100000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 - if sizeof(xlen) == 64 + if xlen == 64 function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = { let rs1_val = (X(rs1))[31..0]; @@ -517,9 +517,9 @@ mapping shiftiwop_mnemonic : sopw <-> string = { } mapping clause assembly = SHIFTIWOP(shamt, rs1, rd, op) - if sizeof(xlen) == 64 + if xlen == 64 <-> shiftiwop_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = FENCE : (bits(4), bits(4)) diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index 22e3d936f..1d5318e26 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -233,7 +233,7 @@ function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | extensionEnabled(Ex /* not used for RV32Zdinx (i.e. RV64-only or D-only). */ val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, regidx)) -> bool function validDoubleRegs(n, regs) = { - if extensionEnabled(Ext_Zdinx) & sizeof(xlen) == 32 then + if extensionEnabled(Ext_Zdinx) & xlen == 32 then foreach (i from 0 to (n - 1)) if (regs[i][0] == bitone) then return false; true @@ -417,20 +417,20 @@ mapping clause encdec = /* D instructions, RV64 only */ mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if haveDoubleFPU() & sizeof(xlen) >= 64 -<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D) if haveDoubleFPU() & xlen >= 64 +<-> 0b110_0001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if haveDoubleFPU() & sizeof(xlen) >= 64 -<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D) if haveDoubleFPU() & xlen >= 64 +<-> 0b110_0001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if haveDoubleFPU() & sizeof(xlen) >= 64 -<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L) if haveDoubleFPU() & xlen >= 64 +<-> 0b110_1001 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if haveDoubleFPU() & sizeof(xlen) >= 64 -<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU) if haveDoubleFPU() & xlen >= 64 +<-> 0b110_1001 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveDoubleFPU() & xlen >= 64 /* Execution semantics ================================ */ @@ -540,7 +540,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); + assert(xlen >= 64); let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -556,7 +556,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); + assert(xlen >= 64); let rs1_val_D = F_or_X_D(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -572,7 +572,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -588,7 +588,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_L)) = { } function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_D_LU)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -905,11 +905,11 @@ mapping clause encdec = F_UN_TYPE_D(rs1, rd, FCLASS_D) if /* D instructions, RV64 only */ -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 - <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_X_D) if extensionEnabled(Ext_D) & xlen >= 64 + <-> 0b111_0001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & xlen >= 64 -mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 - <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & sizeof(xlen) >= 64 +mapping clause encdec = F_UN_TYPE_D(rs1, rd, FMV_D_X) if extensionEnabled(Ext_D) & xlen >= 64 + <-> 0b111_1001 @ 0b00000 @ rs1 @ 0b000 @ rd @ 0b101_0011 if extensionEnabled(Ext_D) & xlen >= 64 /* Execution semantics ================================ */ @@ -934,7 +934,7 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { } function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_D = F(rs1)[63..0]; let rd_val_X : xlenbits = sign_extend(rs1_val_D); X(rd) = rd_val_X; @@ -942,7 +942,7 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = { } function clause execute (F_UN_TYPE_D(rs1, rd, FMV_D_X)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_X = X(rs1); let rd_val_D = rs1_val_X [63..0]; F(rd) = rd_val_D; diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 3a5509ea4..b47955d7f 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -586,20 +586,20 @@ mapping clause encdec = /* F instructions, RV64 only */ mapping clause encdec = - F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) if haveSingleFPU() & sizeof(xlen) >= 64 -<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S) if haveSingleFPU() & xlen >= 64 +<-> 0b110_0000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) if haveSingleFPU() & sizeof(xlen) >= 64 -<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S) if haveSingleFPU() & xlen >= 64 +<-> 0b110_0000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) if haveSingleFPU() & sizeof(xlen) >= 64 -<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L) if haveSingleFPU() & xlen >= 64 +<-> 0b110_1000 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) if haveSingleFPU() & sizeof(xlen) >= 64 -<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU) if haveSingleFPU() & xlen >= 64 +<-> 0b110_1000 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveSingleFPU() & xlen >= 64 /* Execution semantics ================================ */ @@ -679,7 +679,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); + assert(xlen >= 64); let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -695,7 +695,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); + assert(xlen >= 64); let rs1_val_S = F_or_X_S(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -711,7 +711,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = { } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -727,7 +727,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_L)) = { } function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_S_LU)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, diff --git a/model/riscv_insts_hints.sail b/model/riscv_insts_hints.sail index ceddcf28a..ff89493e3 100644 --- a/model/riscv_insts_hints.sail +++ b/model/riscv_insts_hints.sail @@ -97,9 +97,9 @@ mapping clause assembly = C_ADD_HINT(rs2) union clause ast = C_SLLI_HINT : (bits(6), regidx) mapping clause encdec_compressed = C_SLLI_HINT(nzui5 @ nzui40, rsd) - if (nzui5 @ nzui40 == 0b000000 | rsd == zreg) & (sizeof(xlen) == 64 | nzui5 == 0b0) + if (nzui5 @ nzui40 == 0b000000 | rsd == zreg) & (xlen == 64 | nzui5 == 0b0) <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10 - if (nzui5 @ nzui40 == 0b000000 | rsd == zreg) & (sizeof(xlen) == 64 | nzui5 == 0b0) + if (nzui5 @ nzui40 == 0b000000 | rsd == zreg) & (xlen == 64 | nzui5 == 0b0) function clause execute (C_SLLI_HINT(shamt, rsd)) = RETIRE_SUCCESS diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index 5c70eb20c..069ad20de 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -34,10 +34,10 @@ function clause execute (MUL(rs2, rs1, rd, mul_op)) = { let rs2_val = X(rs2); let rs1_int : int = if mul_op.signed_rs1 then signed(rs1_val) else unsigned(rs1_val); let rs2_int : int = if mul_op.signed_rs2 then signed(rs2_val) else unsigned(rs2_val); - let result_wide = to_bits(2 * sizeof(xlen), rs1_int * rs2_int); + let result_wide = to_bits(2 * xlen, rs1_int * rs2_int); let result = if mul_op.high - then result_wide[(2 * sizeof(xlen) - 1) .. sizeof(xlen)] - else result_wide[(sizeof(xlen) - 1) .. 0]; + then result_wide[(2 * xlen - 1) .. xlen] + else result_wide[(xlen - 1) .. 0]; X(rd) = result; RETIRE_SUCCESS } @@ -66,7 +66,7 @@ function clause execute (DIV(rs2, rs1, rd, s)) = { let q : int = if rs2_int == 0 then -1 else quot_round_zero(rs1_int, rs2_int); /* check for signed overflow */ let q': int = if s & q > xlen_max_signed then xlen_min_signed else q; - X(rd) = to_bits(sizeof(xlen), q'); + X(rd) = to_bits(xlen, q'); RETIRE_SUCCESS } @@ -91,7 +91,7 @@ function clause execute (REM(rs2, rs1, rd, s)) = { let rs2_int : int = if s then signed(rs2_val) else unsigned(rs2_val); let r : int = if rs2_int == 0 then rs1_int else rem_round_zero(rs1_int, rs2_int); /* signed overflow case returns zero naturally as required due to -1 divisor */ - X(rd) = to_bits(sizeof(xlen), r); + X(rd) = to_bits(xlen, r); RETIRE_SUCCESS } @@ -102,9 +102,9 @@ mapping clause assembly = REM(rs2, rs1, rd, s) union clause ast = MULW : (regidx, regidx, regidx) mapping clause encdec = MULW(rs2, rs1, rd) - if sizeof(xlen) == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) + if xlen == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) <-> 0b0000001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 - if sizeof(xlen) == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) + if xlen == 64 & (extensionEnabled(Ext_M) | extensionEnabled(Ext_Zmmul)) function clause execute (MULW(rs2, rs1, rd)) = { let rs1_val = X(rs1)[31..0]; @@ -119,17 +119,17 @@ function clause execute (MULW(rs2, rs1, rd)) = { } mapping clause assembly = MULW(rs2, rs1, rd) - if sizeof(xlen) == 64 + if xlen == 64 <-> "mulw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = DIVW : (regidx, regidx, regidx, bool) mapping clause encdec = DIVW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 & extensionEnabled(Ext_M) + if xlen == 64 & extensionEnabled(Ext_M) <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011 - if sizeof(xlen) == 64 & extensionEnabled(Ext_M) + if xlen == 64 & extensionEnabled(Ext_M) function clause execute (DIVW(rs2, rs1, rd, s)) = { let rs1_val = X(rs1)[31..0]; @@ -144,17 +144,17 @@ function clause execute (DIVW(rs2, rs1, rd, s)) = { } mapping clause assembly = DIVW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 + if xlen == 64 <-> "div" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = REMW : (regidx, regidx, regidx, bool) mapping clause encdec = REMW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 & extensionEnabled(Ext_M) + if xlen == 64 & extensionEnabled(Ext_M) <-> 0b0000001 @ rs2 @ rs1 @ 0b11 @ bool_not_bits(s) @ rd @ 0b0111011 - if sizeof(xlen) == 64 & extensionEnabled(Ext_M) + if xlen == 64 & extensionEnabled(Ext_M) function clause execute (REMW(rs2, rs1, rd, s)) = { let rs1_val = X(rs1)[31..0]; @@ -168,6 +168,6 @@ function clause execute (REMW(rs2, rs1, rd, s)) = { } mapping clause assembly = REMW(rs2, rs1, rd, s) - if sizeof(xlen) == 64 + if xlen == 64 <-> "rem" ^ maybe_not_u(s) ^ "w" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) - if sizeof(xlen) == 64 + if xlen == 64 diff --git a/model/riscv_insts_vext_arith.sail b/model/riscv_insts_vext_arith.sail index 77376ed37..78d4e3aae 100644 --- a/model/riscv_insts_vext_arith.sail +++ b/model/riscv_insts_vext_arith.sail @@ -1056,7 +1056,7 @@ function clause execute(VISG(funct6, vm, vs2, simm, vd)) = { let 'm = SEW; let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); - let imm_val : nat = unsigned(zero_extend(sizeof(xlen), simm)); + let imm_val : nat = unsigned(zero_extend(xlen, simm)); let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vs2); let vd_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, LMUL_pow, vd); @@ -1191,7 +1191,7 @@ mapping clause encdec = VMVRTYPE(vs2, simm, vd) if extensionEnabled(Ext_V) function clause execute(VMVRTYPE(vs2, simm, vd)) = { let start_element = get_start_element(); let SEW = get_sew(); - let imm_val = unsigned(zero_extend(sizeof(xlen), simm)); + let imm_val = unsigned(zero_extend(xlen, simm)); let EMUL = imm_val + 1; if not(EMUL == 1 | EMUL == 2 | EMUL == 4 | EMUL == 8) then { handle_illegal(); return RETIRE_FAIL }; @@ -1778,8 +1778,8 @@ function clause execute(VMVXS(vs2, rd)) = { let 'm = SEW; let vs2_val : vector('n, bits('m)) = read_vreg(num_elem, SEW, 0, vs2); - X(rd) = if sizeof(xlen) < SEW then slice(vs2_val[0], 0, sizeof(xlen)) - else if sizeof(xlen) > SEW then sign_extend(vs2_val[0]) + X(rd) = if xlen < SEW then slice(vs2_val[0], 0, xlen) + else if xlen > SEW then sign_extend(vs2_val[0]) else vs2_val[0]; vstart = zeros(); diff --git a/model/riscv_insts_vext_mask.sail b/model/riscv_insts_vext_mask.sail index c586000cc..e4e29a77b 100755 --- a/model/riscv_insts_vext_mask.sail +++ b/model/riscv_insts_vext_mask.sail @@ -105,7 +105,7 @@ function clause execute(VCPOP_M(vm, vs2, rd)) = { if mask[i] & vs2_val[i] then count = count + 1; }; - X(rd) = to_bits(sizeof(xlen), count); + X(rd) = to_bits(xlen, count); vstart = zeros(); RETIRE_SUCCESS } @@ -141,7 +141,7 @@ function clause execute(VFIRST_M(vm, vs2, rd)) = { }; }; - X(rd) = to_bits(sizeof(xlen), index); + X(rd) = to_bits(xlen, index); vstart = zeros(); RETIRE_SUCCESS } diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index cba0d01a7..55bcdfd5d 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -81,7 +81,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) = vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -149,11 +149,11 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) if vm_val[i] then { /* active segments */ foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); + vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); trimmed = true } @@ -162,7 +162,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) if check_misaligned(vaddr, width_type) then { if i == 0 then { handle_mem_exception(vaddr, E_Load_Addr_Align()); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); + vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); trimmed = true } @@ -170,7 +170,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) TR_Failure(e, _) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); + vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); trimmed = true } @@ -181,7 +181,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) MemException(e) => { if i == 0 then { handle_mem_exception(vaddr, e); return RETIRE_FAIL } else { - vl = to_bits(sizeof(xlen), i); + vl = to_bits(xlen, i); print_reg("CSR vl <- " ^ BitStr(vl)); trimmed = true } @@ -251,7 +251,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem) vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = (i * nf + j) * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -313,7 +313,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vd_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vd); - let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); + let rs2_val : int = signed(get_scalar(rs2, xlen)); let (result, mask) = init_masked_result(num_elem, nf * load_width_bytes * 8, EMUL_pow, vd_seg, vm_val); @@ -322,7 +322,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -380,7 +380,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ let width_type : word_width = size_bytes(load_width_bytes); let vm_val : vector('n, bool) = read_vmask(num_elem, vm, 0b00000); let vs3_seg : vector('n, bits('f * 'b * 8)) = read_vreg_seg(num_elem, load_width_bytes * 8, EMUL_pow, nf, vs3); - let rs2_val : int = signed(get_scalar(rs2, sizeof(xlen))); + let rs2_val : int = signed(get_scalar(rs2, xlen)); let mask : vector('n, bool) = init_masked_source(num_elem, EMUL_pow, vm_val); foreach (i from 0 to (num_elem - 1)) { @@ -388,7 +388,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_ vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset = i * rs2_val + j * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -460,7 +460,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), EEW_data_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -551,7 +551,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde vstart = to_bits(16, i); foreach (j from 0 to (nf - 1)) { let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), EEW_data_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -644,7 +644,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { foreach (i from elem_to_align to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -668,7 +668,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = { foreach (i from 0 to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Read(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -726,7 +726,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { foreach (i from elem_to_align to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset : int = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -760,7 +760,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = { foreach (i from 0 to (elem_per_reg - 1)) { vstart = to_bits(16, cur_elem); let elem_offset = cur_elem * load_width_bytes; - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) { + match ext_data_get_addr(rs1, to_bits(xlen, elem_offset), Write(Data), load_width_bytes) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -828,7 +828,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { if i < evl then { /* active elements */ vstart = to_bits(16, i); if op == VLM then { /* load */ - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), 1) { + match ext_data_get_addr(rs1, to_bits(xlen, i), Read(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) @@ -844,7 +844,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = { } } } else if op == VSM then { /* store */ - match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), 1) { + match ext_data_get_addr(rs1, to_bits(xlen, i), Write(Data), 1) { Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL }, Ext_DataAddr_OK(vaddr) => if check_misaligned(vaddr, width_type) diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail index 5aa5bdff1..f71b3739c 100755 --- a/model/riscv_insts_vext_utils.sail +++ b/model/riscv_insts_vext_utils.sail @@ -163,7 +163,7 @@ function illegal_indexed_store(nf, EEW_index, EMUL_pow_index, EMUL_pow_data) = { /* Scalar register shaping */ val get_scalar : forall 'm, 'm >= 8. (regidx, int('m)) -> bits('m) function get_scalar(rs1, SEW) = { - if SEW <= sizeof(xlen) then { + if SEW <= xlen then { /* Least significant SEW bits */ X(rs1)[SEW - 1 .. 0] } else { diff --git a/model/riscv_insts_vext_vset.sail b/model/riscv_insts_vext_vset.sail index 7e73d5724..9cbed51fd 100644 --- a/model/riscv_insts_vext_vset.sail +++ b/model/riscv_insts_vext_vset.sail @@ -49,7 +49,7 @@ function handle_illegal_vtype() = { /* Note: Implementations can set vill or trap if the vtype setting is not supported. * TODO: configuration support for both solutions */ - vtype.bits = 0b1 @ zeros(sizeof(xlen) - 1); /* set vtype.vill */ + vtype.bits = 0b1 @ zeros(xlen - 1); /* set vtype.vill */ vl = zeros(); print_reg("CSR vtype <- " ^ BitStr(vtype.bits)); print_reg("CSR vl <- " ^ BitStr(vl)) @@ -60,9 +60,9 @@ function calculate_new_vl(AVL, VLMAX) = { /* Note: ceil(AVL / 2) ≤ vl ≤ VLMAX when VLMAX < AVL < (2 * VLMAX) * TODO: configuration support for either using ceil(AVL / 2) or VLMAX */ - if AVL <= VLMAX then to_bits(sizeof(xlen), AVL) - else if AVL < 2 * VLMAX then to_bits(sizeof(xlen), (AVL + 1) / 2) - else to_bits(sizeof(xlen), VLMAX) + if AVL <= VLMAX then to_bits(xlen, AVL) + else if AVL < 2 * VLMAX then to_bits(xlen, (AVL + 1) / 2) + else to_bits(xlen, VLMAX) } /* *********************************** vsetvli *********************************** */ @@ -77,7 +77,7 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { let ratio_pow_ori = SEW_pow_ori - LMUL_pow_ori; /* set vtype */ - vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + vtype.bits = 0b0 @ zeros(xlen - 9) @ ma @ ta @ sew @ lmul; /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); @@ -94,8 +94,8 @@ function clause execute VSETVLI(ma, ta, sew, lmul, rs1, rd) = { vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ - let AVL = unsigned(ones(sizeof(xlen))); - vl = to_bits(sizeof(xlen), VLMAX); + let AVL = unsigned(ones(xlen)); + vl = to_bits(xlen, VLMAX); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -145,8 +145,8 @@ function clause execute VSETVL(rs2, rs1, rd) = { vl = calculate_new_vl(AVL, VLMAX); X(rd) = vl; } else if (rd != 0b00000) then { /* set vl to VLMAX */ - let AVL = unsigned(ones(sizeof(xlen))); - vl = to_bits(sizeof(xlen), VLMAX); + let AVL = unsigned(ones(xlen)); + vl = to_bits(xlen, VLMAX); X(rd) = vl; } else { /* keep existing vl */ let AVL = unsigned(vl); @@ -175,7 +175,7 @@ mapping clause encdec = VSETIVLI(ma, ta, sew, lmul, uimm, rd) if extensionEnable function clause execute VSETIVLI(ma, ta, sew, lmul, uimm, rd) = { /* set vtype */ - vtype.bits = 0b0 @ zeros(sizeof(xlen) - 9) @ ma @ ta @ sew @ lmul; + vtype.bits = 0b0 @ zeros(xlen - 9) @ ma @ ta @ sew @ lmul; /* check new SEW and LMUL are legal and calculate VLMAX */ let VLEN_pow = get_vlen_pow(); diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail index 21dd026f1..bef115cc4 100644 --- a/model/riscv_insts_zba.sail +++ b/model/riscv_insts_zba.sail @@ -15,8 +15,8 @@ function clause extensionEnabled(Ext_Zba) = true | extensionEnabled(Ext_B) /* ****************************************************************** */ union clause ast = RISCV_SLLIUW : (bits(6), regidx, regidx) -mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 - <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_SLLIUW(shamt, rs1, rd) if extensionEnabled(Ext_Zba) & xlen == 64 + <-> 0b000010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zba) & xlen == 64 mapping clause assembly = RISCV_SLLIUW(shamt, rs1, rd) <-> "slli.uw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) @@ -31,17 +31,17 @@ function clause execute (RISCV_SLLIUW(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = ZBA_RTYPEUW : (regidx, regidx, regidx, bropw_zba) -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 - <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_ADDUW) if extensionEnabled(Ext_Zba) & xlen == 64 + <-> 0b0000100 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & xlen == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH1ADDUW) if extensionEnabled(Ext_Zba) & xlen == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b010 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & xlen == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH2ADDUW) if extensionEnabled(Ext_Zba) & xlen == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & xlen == 64 -mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 - <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 +mapping clause encdec = ZBA_RTYPEUW(rs2, rs1, rd, RISCV_SH3ADDUW) if extensionEnabled(Ext_Zba) & xlen == 64 + <-> 0b0010000 @ rs2 @ rs1 @ 0b110 @ rd @ 0b0111011 if extensionEnabled(Ext_Zba) & xlen == 64 mapping zba_rtypeuw_mnemonic : bropw_zba <-> string = { RISCV_ADDUW <-> "add.uw", diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index 696619dfe..5a62ba2dd 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -15,8 +15,8 @@ function clause extensionEnabled(Ext_Zbkb) = true /* ****************************************************************** */ union clause ast = RISCV_RORIW : (bits(5), regidx, regidx) -mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 - <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_RORIW(shamt, rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 + <-> 0b0110000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0011011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 mapping clause assembly = RISCV_RORIW(shamt, rs1, rd) <-> "roriw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_5(shamt) @@ -31,15 +31,15 @@ function clause execute (RISCV_RORIW(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_RORI : (bits(6), regidx, regidx) -mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = RISCV_RORI(shamt, rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (xlen == 64 | shamt[5] == bitzero) + <-> 0b011000 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & (xlen == 64 | shamt[5] == bitzero) mapping clause assembly = RISCV_RORI(shamt, rs1, rd) <-> "rori" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_6(shamt) function clause execute (RISCV_RORI(shamt, rs1, rd)) = { let rs1_val = X(rs1); - let result : xlenbits = if sizeof(xlen) == 32 + let result : xlenbits = if xlen == 32 then rs1_val >>> shamt[4..0] else rs1_val >>> shamt; X(rd) = result; @@ -49,11 +49,11 @@ function clause execute (RISCV_RORI(shamt, rs1, rd)) = { /* ****************************************************************** */ union clause ast = ZBB_RTYPEW : (regidx, regidx, regidx, bropw_zbb) -mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 - <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_ROLW) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b001 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 -mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 - <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_RTYPEW(rs2, rs1, rd, RISCV_RORW) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 + <-> 0b0110000 @ rs2 @ rs1 @ 0b101 @ rd @ 0b0111011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 mapping zbb_rtypew_mnemonic : bropw_zbb <-> string = { RISCV_ROLW <-> "rolw", @@ -126,14 +126,14 @@ function clause execute (ZBB_RTYPE(rs2, rs1, rd, op)) = { RISCV_ANDN => rs1_val & ~(rs2_val), RISCV_ORN => rs1_val | ~(rs2_val), RISCV_XNOR => ~(rs1_val ^ rs2_val), - RISCV_MAX => to_bits(sizeof(xlen), max(signed(rs1_val), signed(rs2_val))), - RISCV_MAXU => to_bits(sizeof(xlen), max(unsigned(rs1_val), unsigned(rs2_val))), - RISCV_MIN => to_bits(sizeof(xlen), min(signed(rs1_val), signed(rs2_val))), - RISCV_MINU => to_bits(sizeof(xlen), min(unsigned(rs1_val), unsigned(rs2_val))), - RISCV_ROL => if sizeof(xlen) == 32 + RISCV_MAX => to_bits(xlen, max(signed(rs1_val), signed(rs2_val))), + RISCV_MAXU => to_bits(xlen, max(unsigned(rs1_val), unsigned(rs2_val))), + RISCV_MIN => to_bits(xlen, min(signed(rs1_val), signed(rs2_val))), + RISCV_MINU => to_bits(xlen, min(unsigned(rs1_val), unsigned(rs2_val))), + RISCV_ROL => if xlen == 32 then rs1_val <<< rs2_val[4..0] else rs1_val <<< rs2_val[5..0], - RISCV_ROR => if sizeof(xlen) == 32 + RISCV_ROR => if xlen == 32 then rs1_val >>> rs2_val[4..0] else rs1_val >>> rs2_val[5..0] }; @@ -150,11 +150,11 @@ mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTB) if extensionEnabled(Ext_ mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_SEXTH) if extensionEnabled(Ext_Zbb) <-> 0b0110000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbb) -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 32 - <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 32 +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & xlen == 32 + <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0110011 if extensionEnabled(Ext_Zbb) & xlen == 32 -mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 - <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 +mapping clause encdec = ZBB_EXTOP(rs1, rd, RISCV_ZEXTH) if extensionEnabled(Ext_Zbb) & xlen == 64 + <-> 0b0000100 @ 0b00000 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbb) & xlen == 64 mapping zbb_extop_mnemonic : extop_zbb <-> string = { RISCV_SEXTB <-> "sext.b", @@ -179,11 +179,11 @@ function clause execute (ZBB_EXTOP(rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = RISCV_REV8 : (regidx, regidx) -mapping clause encdec = RISCV_REV8(rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32 - <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 32 +mapping clause encdec = RISCV_REV8(rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 32 + <-> 0b011010011000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 32 -mapping clause encdec = RISCV_REV8(rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 - <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_REV8(rs1, rd) if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 + <-> 0b011010111000 @ rs1 @ 0b101 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zbb) | extensionEnabled(Ext_Zbkb)) & xlen == 64 mapping clause assembly = RISCV_REV8(rs1, rd) <-> "rev8" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -191,8 +191,8 @@ mapping clause assembly = RISCV_REV8(rs1, rd) function clause execute (RISCV_REV8(rs1, rd)) = { let rs1_val = X(rs1); var result : xlenbits = zeros(); - foreach (i from 0 to (sizeof(xlen) - 8) by 8) - result[(i + 7) .. i] = rs1_val[(sizeof(xlen) - i - 1) .. (sizeof(xlen) - i - 8)]; + foreach (i from 0 to (xlen - 8) by 8) + result[(i + 7) .. i] = rs1_val[(xlen - i - 1) .. (xlen - i - 8)]; X(rd) = result; RETIRE_SUCCESS } @@ -209,7 +209,7 @@ mapping clause assembly = RISCV_ORCB(rs1, rd) function clause execute (RISCV_ORCB(rs1, rd)) = { let rs1_val = X(rs1); var result : xlenbits = zeros(); - foreach (i from 0 to (sizeof(xlen) - 8) by 8) + foreach (i from 0 to (xlen - 8) by 8) result[(i + 7) .. i] = if rs1_val[(i + 7) .. i] == zeros() then 0x00 else 0xFF; @@ -231,15 +231,15 @@ function clause execute (RISCV_CPOP(rs1, rd)) = { var result : nat = 0; foreach (i from 0 to (xlen_val - 1)) if rs1_val[i] == bitone then result = result + 1; - X(rd) = to_bits(sizeof(xlen), result); + X(rd) = to_bits(xlen, result); RETIRE_SUCCESS } /* ****************************************************************** */ union clause ast = RISCV_CPOPW : (regidx, regidx) -mapping clause encdec = RISCV_CPOPW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 - <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CPOPW(rs1, rd) if extensionEnabled(Ext_Zbb) & xlen == 64 + <-> 0b011000000010 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & xlen == 64 mapping clause assembly = RISCV_CPOPW(rs1, rd) <-> "cpopw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -249,7 +249,7 @@ function clause execute (RISCV_CPOPW(rs1, rd)) = { var result : nat = 0; foreach (i from 0 to 31) if rs1_val[i] == bitone then result = result + 1; - X(rd) = to_bits(sizeof(xlen), result); + X(rd) = to_bits(xlen, result); RETIRE_SUCCESS } @@ -266,19 +266,19 @@ function clause execute (RISCV_CLZ(rs1, rd)) = { let rs1_val = X(rs1); var result : nat = 0; var done : bool = false; - foreach (i from (sizeof(xlen) - 1) downto 0) + foreach (i from (xlen - 1) downto 0) if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; - X(rd) = to_bits(sizeof(xlen), result); + X(rd) = to_bits(xlen, result); RETIRE_SUCCESS } /* ****************************************************************** */ union clause ast = RISCV_CLZW : (regidx, regidx) -mapping clause encdec = RISCV_CLZW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 - <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CLZW(rs1, rd) if extensionEnabled(Ext_Zbb) & xlen == 64 + <-> 0b011000000000 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & xlen == 64 mapping clause assembly = RISCV_CLZW(rs1, rd) <-> "clzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -291,7 +291,7 @@ function clause execute (RISCV_CLZW(rs1, rd)) = { if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; - X(rd) = to_bits(sizeof(xlen), result); + X(rd) = to_bits(xlen, result); RETIRE_SUCCESS } @@ -308,19 +308,19 @@ function clause execute (RISCV_CTZ(rs1, rd)) = { let rs1_val = X(rs1); var result : nat = 0; var done : bool = false; - foreach (i from 0 to (sizeof(xlen) - 1)) + foreach (i from 0 to (xlen - 1)) if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; - X(rd) = to_bits(sizeof(xlen), result); + X(rd) = to_bits(xlen, result); RETIRE_SUCCESS } /* ****************************************************************** */ union clause ast = RISCV_CTZW : (regidx, regidx) -mapping clause encdec = RISCV_CTZW(rs1, rd) if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 - <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & sizeof(xlen) == 64 +mapping clause encdec = RISCV_CTZW(rs1, rd) if extensionEnabled(Ext_Zbb) & xlen == 64 + <-> 0b011000000001 @ rs1 @ 0b001 @ rd @ 0b0011011 if extensionEnabled(Ext_Zbb) & xlen == 64 mapping clause assembly = RISCV_CTZW(rs1, rd) <-> "ctzw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -333,6 +333,6 @@ function clause execute (RISCV_CTZW(rs1, rd)) = { if not(done) then if rs1_val[i] == bitzero then result = result + 1 else done = true; - X(rd) = to_bits(sizeof(xlen), result); + X(rd) = to_bits(xlen, result); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail index b8ce9569b..f7fa3ec1d 100644 --- a/model/riscv_insts_zbkb.sail +++ b/model/riscv_insts_zbkb.sail @@ -37,14 +37,14 @@ function clause execute (ZBKB_RTYPE(rs2, rs1, rd, op)) = { /* ****************************************************************** */ union clause ast = ZBKB_PACKW : (regidx, regidx, regidx) -mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 64 - <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 64 +mapping clause encdec = ZBKB_PACKW(rs2, rs1, rd) if extensionEnabled(Ext_Zbkb) & xlen == 64 + <-> 0b0000100 @ rs2 @ rs1 @ 0b100 @ rd @ 0b0111011 if extensionEnabled(Ext_Zbkb) & xlen == 64 mapping clause assembly = ZBKB_PACKW(rs2, rs1, rd) <-> "packw" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) function clause execute (ZBKB_PACKW(rs2, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let rs1_val = X(rs1); let rs2_val = X(rs2); let result : bits(32) = rs2_val[15..0] @ rs1_val[15..0]; @@ -55,14 +55,14 @@ function clause execute (ZBKB_PACKW(rs2, rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_ZIP : (regidx, regidx) -mapping clause encdec = RISCV_ZIP(rs1, rd) if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 - <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 +mapping clause encdec = RISCV_ZIP(rs1, rd) if extensionEnabled(Ext_Zbkb) & xlen == 32 + <-> 0b000010001111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) & xlen == 32 mapping clause assembly = RISCV_ZIP(rs1, rd) <-> "zip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) function clause execute (RISCV_ZIP(rs1, rd)) = { - assert(sizeof(xlen) == 32); + assert(xlen == 32); let rs1_val = X(rs1); var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) { @@ -76,14 +76,14 @@ function clause execute (RISCV_ZIP(rs1, rd)) = { /* ****************************************************************** */ union clause ast = RISCV_UNZIP : (regidx, regidx) -mapping clause encdec = RISCV_UNZIP(rs1, rd) if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 - <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) & sizeof(xlen) == 32 +mapping clause encdec = RISCV_UNZIP(rs1, rd) if extensionEnabled(Ext_Zbkb) & xlen == 32 + <-> 0b000010001111 @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbkb) & xlen == 32 mapping clause assembly = RISCV_UNZIP(rs1, rd) <-> "unzip" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) function clause execute (RISCV_UNZIP(rs1, rd)) = { - assert(sizeof(xlen) == 32); + assert(xlen == 32); let rs1_val = X(rs1); var result : xlenbits = zeros(); foreach (i from 0 to (sizeof(xlen_bytes)*4 - 1)) { @@ -106,7 +106,7 @@ mapping clause assembly = RISCV_BREV8(rs1, rd) function clause execute (RISCV_BREV8(rs1, rd)) = { let rs1_val = X(rs1); var result : xlenbits = zeros(); - foreach (i from 0 to (sizeof(xlen) - 8) by 8) + foreach (i from 0 to (xlen - 8) by 8) result[i+7..i] = reverse(rs1_val[i+7..i]); X(rd) = result; RETIRE_SUCCESS diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail index 52c812035..226938477 100644 --- a/model/riscv_insts_zbkx.sail +++ b/model/riscv_insts_zbkx.sail @@ -22,9 +22,9 @@ function clause execute (RISCV_XPERM8(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); var result : xlenbits = zeros(); - foreach (i from 0 to (sizeof(xlen) - 8) by 8) { + foreach (i from 0 to (xlen - 8) by 8) { let index = unsigned(rs2_val[i+7..i]); - result[i+7..i] = if 8*index < sizeof(xlen) + result[i+7..i] = if 8*index < xlen then rs1_val[8*index+7..8*index] else zeros() }; @@ -45,9 +45,9 @@ function clause execute (RISCV_XPERM4(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); var result : xlenbits = zeros(); - foreach (i from 0 to (sizeof(xlen) - 4) by 4) { + foreach (i from 0 to (xlen - 4) by 4) { let index = unsigned(rs2_val[i+3..i]); - result[i+3..i] = if 4*index < sizeof(xlen) + result[i+3..i] = if 4*index < xlen then rs1_val[4*index+3..4*index] else zeros() }; diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail index 348b702ec..a016612c9 100644 --- a/model/riscv_insts_zbs.sail +++ b/model/riscv_insts_zbs.sail @@ -12,17 +12,17 @@ function clause extensionEnabled(Ext_Zbs) = true | extensionEnabled(Ext_B) /* ****************************************************************** */ union clause ast = ZBS_IOP : (bits(6), regidx, regidx, biop_zbs) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BCLRI) if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) + <-> 0b010010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BEXTI) if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) + <-> 0b010010 @ shamt @ rs1 @ 0b101 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BINVI) if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) + <-> 0b011010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) -mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) - <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (sizeof(xlen) == 64 | shamt[5] == bitzero) +mapping clause encdec = ZBS_IOP(shamt, rs1, rd, RISCV_BSETI) if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) + <-> 0b001010 @ shamt @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zbs) & (xlen == 64 | shamt[5] == bitzero) mapping zbs_iop_mnemonic : biop_zbs <-> string = { RISCV_BCLRI <-> "bclri", @@ -36,7 +36,7 @@ mapping clause assembly = ZBS_IOP(shamt, rs1, rd, op) function clause execute (ZBS_IOP(shamt, rs1, rd, op)) = { let rs1_val = X(rs1); - let mask : xlenbits = if sizeof(xlen) == 32 + let mask : xlenbits = if xlen == 32 then zero_extend(0b1) << shamt[4..0] else zero_extend(0b1) << shamt; let result : xlenbits = match op { @@ -77,7 +77,7 @@ mapping clause assembly = ZBS_RTYPE(rs2, rs1, rd, op) function clause execute (ZBS_RTYPE(rs2, rs1, rd, op)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); - let mask : xlenbits = if sizeof(xlen) == 32 + let mask : xlenbits = if xlen == 32 then zero_extend(0b1) << rs2_val[4..0] else zero_extend(0b1) << rs2_val[5..0]; let result : xlenbits = match op { diff --git a/model/riscv_insts_zca.sail b/model/riscv_insts_zca.sail index 2e08c179e..5a6dbfb77 100644 --- a/model/riscv_insts_zca.sail +++ b/model/riscv_insts_zca.sail @@ -63,9 +63,9 @@ mapping clause assembly = C_LW(uimm, rsc, rdc) union clause ast = C_LD : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd) - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b011 @ ui53 : bits(3) @ rs1 : cregidx @ ui76 : bits(2) @ rd : cregidx @ 0b00 - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_LD(uimm, rsc, rdc)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -75,9 +75,9 @@ function clause execute (C_LD(uimm, rsc, rdc)) = { } mapping clause assembly = C_LD(uimm, rsc, rdc) - if sizeof(xlen) == 64 + if xlen == 64 <-> "c.ld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_SW : (bits(5), cregidx, cregidx) @@ -99,9 +99,9 @@ mapping clause assembly = C_SW(uimm, rsc1, rsc2) union clause ast = C_SD : (bits(5), cregidx, cregidx) mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2) - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b111 @ ui53 : bits(3) @ rs1 : bits(3) @ ui76 : bits(2) @ rs2 : bits(3) @ 0b00 - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_SD(uimm, rsc1, rsc2)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -111,9 +111,9 @@ function clause execute (C_SD(uimm, rsc1, rsc2)) = { } mapping clause assembly = C_SD(uimm, rsc1, rsc2) - if sizeof(xlen) == 64 + if xlen == 64 <-> "c.sd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_ADDI : (bits(6), regidx) @@ -137,33 +137,33 @@ mapping clause assembly = C_ADDI(nzi, rsd) union clause ast = C_JAL : (bits(11)) mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31) - if sizeof(xlen) == 32 & extensionEnabled(Ext_Zca) + if xlen == 32 & extensionEnabled(Ext_Zca) <-> 0b001 @ i11 : bits(1) @ i4 : bits(1) @ i98 : bits(2) @ i10 : bits(1) @ i6 : bits(1) @ i7 : bits(1) @ i31 : bits(3) @ i5 : bits(1) @ 0b01 - if sizeof(xlen) == 32 & extensionEnabled(Ext_Zca) + if xlen == 32 & extensionEnabled(Ext_Zca) function clause execute (C_JAL(imm)) = execute(RISCV_JAL(sign_extend(imm @ 0b0), ra)) mapping clause assembly = C_JAL(imm) - if sizeof(xlen) == 32 + if xlen == 32 <-> "c.jal" ^ spc() ^ hex_bits_signed_12(imm @ 0b0) - if sizeof(xlen) == 32 + if xlen == 32 /* ****************************************************************** */ union clause ast = C_ADDIW : (bits(6), regidx) mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) - if rsd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if rsd != zreg & xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b001 @ imm5 : bits(1) @ rsd : regidx @ imm40 : bits(5) @ 0b01 - if rsd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if rsd != zreg & xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_ADDIW(imm, rsd)) = execute(ADDIW(sign_extend(imm), rsd, rsd)) mapping clause assembly = C_ADDIW(imm, rsd) - if sizeof(xlen) == 64 + if xlen == 64 <-> "c.addiw" ^ spc() ^ reg_name(rsd) ^ sep() ^ hex_bits_signed_6(imm) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_LI : (bits(6), regidx) @@ -223,9 +223,9 @@ mapping clause assembly = C_LUI(imm, rd) union clause ast = C_SRLI : (bits(6), cregidx) mapping clause encdec_compressed = C_SRLI(nzui5 @ nzui40, rsd) - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) + if nzui5 @ nzui40 != 0b000000 & (xlen == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) <-> 0b100 @ nzui5 : bits(1) @ 0b00 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01 - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) + if nzui5 @ nzui40 != 0b000000 & (xlen == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) function clause execute (C_SRLI(shamt, rsd)) = { let rsd = creg2reg_idx(rsd); @@ -241,9 +241,9 @@ mapping clause assembly = C_SRLI(shamt, rsd) union clause ast = C_SRAI : (bits(6), cregidx) mapping clause encdec_compressed = C_SRAI(nzui5 @ nzui40, rsd) - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) + if nzui5 @ nzui40 != 0b000000 & (xlen == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) <-> 0b100 @ nzui5 : bits(1) @ 0b01 @ rsd : cregidx @ nzui40 : bits(5) @ 0b01 - if nzui5 @ nzui40 != 0b000000 & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) + if nzui5 @ nzui40 != 0b000000 & (xlen == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) function clause execute (C_SRAI(shamt, rsd)) = { let rsd = creg2reg_idx(rsd); @@ -333,9 +333,9 @@ mapping clause assembly = C_AND(rsd, rs2) union clause ast = C_SUBW : (cregidx, cregidx) mapping clause encdec_compressed = C_SUBW(rsd, rs2) - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b00 @ rs2 : cregidx @ 0b01 - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_SUBW(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -344,17 +344,17 @@ function clause execute (C_SUBW(rsd, rs2)) = { } mapping clause assembly = C_SUBW(rsd, rs2) - if sizeof(xlen) == 64 + if xlen == 64 <-> "c.subw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_ADDW : (cregidx, cregidx) mapping clause encdec_compressed = C_ADDW(rsd, rs2) - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b100 @ 0b1 @ 0b11 @ rsd : cregidx @ 0b01 @ rs2 : cregidx @ 0b01 - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_ADDW(rsd, rs2)) = { let rsd = creg2reg_idx(rsd); @@ -363,9 +363,9 @@ function clause execute (C_ADDW(rsd, rs2)) = { } mapping clause assembly = C_ADDW(rsd, rs2) - if sizeof(xlen) == 64 + if xlen == 64 <-> "c.addw" ^ spc() ^ creg_name(rsd) ^ sep() ^ creg_name(rs2) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_J : (bits(11)) @@ -407,9 +407,9 @@ mapping clause assembly = C_BNEZ(imm, rs) union clause ast = C_SLLI : (bits(6), regidx) mapping clause encdec_compressed = C_SLLI(nzui5 @ nzui40, rsd) - if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) + if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (xlen == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) <-> 0b000 @ nzui5 : bits(1) @ rsd : regidx @ nzui40 : bits(5) @ 0b10 - if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (sizeof(xlen) == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) + if nzui5 @ nzui40 != 0b000000 & rsd != zreg & (xlen == 64 | nzui5 == 0b0) & extensionEnabled(Ext_Zca) function clause execute (C_SLLI(shamt, rsd)) = execute(SHIFTIOP(shamt, rsd, rsd, RISCV_SLLI)) @@ -441,9 +441,9 @@ mapping clause assembly = C_LWSP(uimm, rd) union clause ast = C_LDSP : (bits(6), regidx) mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd) - if rd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if rd != zreg & xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b011 @ ui5 : bits(1) @ rd : regidx @ ui43 : bits(2) @ ui86 : bits(3) @ 0b10 - if rd != zreg & sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if rd != zreg & xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_LDSP(uimm, rd)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -451,9 +451,9 @@ function clause execute (C_LDSP(uimm, rd)) = { } mapping clause assembly = C_LDSP(uimm, rd) - if rd != zreg & sizeof(xlen) == 64 + if rd != zreg & xlen == 64 <-> "c.ldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm) - if rd != zreg & sizeof(xlen) == 64 + if rd != zreg & xlen == 64 /* ****************************************************************** */ union clause ast = C_SWSP : (bits(6), regidx) @@ -475,9 +475,9 @@ mapping clause assembly = C_SWSP(uimm, rs2) union clause ast = C_SDSP : (bits(6), regidx) mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2) - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) <-> 0b111 @ ui53 : bits(3) @ ui86 : bits(3) @ rs2 : regidx @ 0b10 - if sizeof(xlen) == 64 & extensionEnabled(Ext_Zca) + if xlen == 64 & extensionEnabled(Ext_Zca) function clause execute (C_SDSP(uimm, rs2)) = { let imm : bits(12) = zero_extend(uimm @ 0b000); @@ -485,9 +485,9 @@ function clause execute (C_SDSP(uimm, rs2)) = { } mapping clause assembly = C_SDSP(uimm, rs2) - if sizeof(xlen) == 64 + if xlen == 64 <-> "c.sdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm) - if sizeof(xlen) == 64 + if xlen == 64 /* ****************************************************************** */ union clause ast = C_JR : (regidx) diff --git a/model/riscv_insts_zcb.sail b/model/riscv_insts_zcb.sail index e0e104081..821ce0bd6 100644 --- a/model/riscv_insts_zcb.sail +++ b/model/riscv_insts_zcb.sail @@ -167,8 +167,8 @@ function clause execute C_SEXT_H(rsdc) = { union clause ast = C_ZEXT_W : (cregidx) mapping clause encdec_compressed = - C_ZEXT_W(rsdc) if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 - <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & sizeof(xlen) == 64 + C_ZEXT_W(rsdc) if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & xlen == 64 + <-> 0b100 @ 0b111 @ rsdc : cregidx @ 0b11 @ 0b100 @ 0b01 if extensionEnabled(Ext_Zcb) & extensionEnabled(Ext_Zba) & xlen == 64 mapping clause assembly = C_ZEXT_W(rsdc) <-> "c.zext.w" ^ spc() ^ creg_name(rsdc) diff --git a/model/riscv_insts_zcd.sail b/model/riscv_insts_zcd.sail index fc608a41e..2d5f7c032 100644 --- a/model/riscv_insts_zcd.sail +++ b/model/riscv_insts_zcd.sail @@ -7,7 +7,7 @@ /*=======================================================================================*/ enum clause extension = Ext_Zcd -function clause extensionEnabled(Ext_Zcd) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_D) & (sizeof(xlen) == 32 | sizeof(xlen) == 64) +function clause extensionEnabled(Ext_Zcd) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_D) & (xlen == 32 | xlen == 64) union clause ast = C_FLDSP : (bits(6), regidx) @@ -20,9 +20,9 @@ function clause execute (C_FLDSP(uimm, rd)) = { } mapping clause assembly = C_FLDSP(uimm, rd) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) <-> "c.fldsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(uimm) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) /* ****************************************************************** */ union clause ast = C_FSDSP : (bits(6), regidx) @@ -36,9 +36,9 @@ function clause execute (C_FSDSP(uimm, rs2)) = { } mapping clause assembly = C_FSDSP(uimm, rs2) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) <-> "c.fsdsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) /* ****************************************************************** */ union clause ast = C_FLD : (bits(5), cregidx, cregidx) @@ -54,9 +54,9 @@ function clause execute (C_FLD(uimm, rsc, rdc)) = { } mapping clause assembly = C_FLD(uimm, rsc, rdc) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) <-> "c.fld" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) /* ****************************************************************** */ union clause ast = C_FSD : (bits(5), cregidx, cregidx) @@ -72,6 +72,6 @@ function clause execute (C_FSD(uimm, rsc1, rsc2)) = { } mapping clause assembly = C_FSD(uimm, rsc1, rsc2) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) <-> "c.fsd" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_8(uimm @ 0b000) - if (sizeof(xlen) == 32 | sizeof(xlen) == 64) + if (xlen == 32 | xlen == 64) diff --git a/model/riscv_insts_zcf.sail b/model/riscv_insts_zcf.sail index ce601de87..d061c1b93 100644 --- a/model/riscv_insts_zcf.sail +++ b/model/riscv_insts_zcf.sail @@ -16,7 +16,7 @@ /* ****************************************************************** */ enum clause extension = Ext_Zcf -function clause extensionEnabled(Ext_Zcf) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_F) & sizeof(xlen) == 32 +function clause extensionEnabled(Ext_Zcf) = extensionEnabled(Ext_Zca) & extensionEnabled(Ext_F) & xlen == 32 union clause ast = C_FLWSP : (bits(6), regidx) @@ -29,9 +29,9 @@ function clause execute (C_FLWSP(imm, rd)) = { } mapping clause assembly = C_FLWSP(imm, rd) - if sizeof(xlen) == 32 + if xlen == 32 <-> "c.flwsp" ^ spc() ^ reg_name(rd) ^ sep() ^ hex_bits_6(imm) - if sizeof(xlen) == 32 + if xlen == 32 /* ****************************************************************** */ union clause ast = C_FSWSP : (bits(6), regidx) @@ -45,9 +45,9 @@ function clause execute (C_FSWSP(uimm, rs2)) = { } mapping clause assembly = C_FSWSP(uimm, rs2) - if sizeof(xlen) == 32 + if xlen == 32 <-> "c.fswsp" ^ spc() ^ reg_name(rs2) ^ sep() ^ hex_bits_6(uimm) - if sizeof(xlen) == 32 + if xlen == 32 /* ****************************************************************** */ union clause ast = C_FLW : (bits(5), cregidx, cregidx) @@ -63,9 +63,9 @@ function clause execute (C_FLW(uimm, rsc, rdc)) = { } mapping clause assembly = C_FLW(uimm, rsc, rdc) - if sizeof(xlen) == 32 + if xlen == 32 <-> "c.flw" ^ spc() ^ creg_name(rdc) ^ sep() ^ creg_name(rsc) ^ sep() ^ hex_bits_7(uimm @ 0b00) - if sizeof(xlen) == 32 + if xlen == 32 /* ****************************************************************** */ union clause ast = C_FSW : (bits(5), cregidx, cregidx) @@ -81,6 +81,6 @@ function clause execute (C_FSW(uimm, rsc1, rsc2)) = { } mapping clause assembly = C_FSW(uimm, rsc1, rsc2) - if sizeof(xlen) == 32 + if xlen == 32 <-> "c.fsw" ^ spc() ^ creg_name(rsc1) ^ sep() ^ creg_name(rsc2) ^ sep() ^ hex_bits_7(uimm @ 0b00) - if sizeof(xlen) == 32 + if xlen == 32 diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 5e55fb8a2..e484b4577 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -559,20 +559,20 @@ mapping clause encdec = /* F instructions, RV64 only */ mapping clause encdec = - F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H) if haveHalfFPU() & sizeof(xlen) >= 64 -<-> 0b110_0010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H) if haveHalfFPU() & xlen >= 64 +<-> 0b110_0010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H) if haveHalfFPU() & sizeof(xlen) >= 64 -<-> 0b110_0010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H) if haveHalfFPU() & xlen >= 64 +<-> 0b110_0010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L) if haveHalfFPU() & sizeof(xlen) >= 64 -<-> 0b110_1010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L) if haveHalfFPU() & xlen >= 64 +<-> 0b110_1010 @ 0b00010 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & xlen >= 64 mapping clause encdec = - F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU) if haveHalfFPU() & sizeof(xlen) >= 64 -<-> 0b110_1010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & sizeof(xlen) >= 64 + F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU) if haveHalfFPU() & xlen >= 64 +<-> 0b110_1010 @ 0b00011 @ rs1 @ encdec_rounding_mode (rm) @ rd @ 0b101_0011 if haveHalfFPU() & xlen >= 64 /* Execution semantics ================================ */ @@ -713,7 +713,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); + assert(xlen >= 64); let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -729,7 +729,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); + assert(xlen >= 64); let rs1_val_H = F_or_X_H(rs1); match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -745,7 +745,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)) = { } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_L = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, @@ -761,7 +761,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_L)) = { } function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_H_LU)) = { - assert(sizeof(xlen) >= 64); + assert(xlen >= 64); let rs1_val_LU = X(rs1)[63..0]; match (select_instr_or_fcsr_rm (rm)) { None() => { handle_illegal(); RETIRE_FAIL }, diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index c96d31a5b..e996f71b2 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -37,9 +37,9 @@ function clause read_CSR(0x303) = mideleg.bits function clause read_CSR(0x304) = mie.bits function clause read_CSR(0x305) = get_mtvec() function clause read_CSR(0x306) = zero_extend(mcounteren.bits) -function clause read_CSR(0x30A) = menvcfg.bits[sizeof(xlen) - 1 .. 0] -function clause read_CSR(0x310 if sizeof(xlen) == 32) = mstatush.bits -function clause read_CSR(0x31A if sizeof(xlen) == 32) = menvcfg.bits[63 .. 32] +function clause read_CSR(0x30A) = menvcfg.bits[xlen - 1 .. 0] +function clause read_CSR(0x310 if xlen == 32) = mstatush.bits +function clause read_CSR(0x31A if xlen == 32) = menvcfg.bits[63 .. 32] function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits) /* Hardware Performance Monitoring event selection */ @@ -52,7 +52,7 @@ function clause read_CSR(0x343) = mtval function clause read_CSR(0x344) = mip.bits // pmpcfgN -function clause read_CSR(0x3A @ idx : bits(4) if idx[0] == bitzero | sizeof(xlen) == 32) = pmpReadCfgReg(unsigned(idx)) +function clause read_CSR(0x3A @ idx : bits(4) if idx[0] == bitzero | xlen == 32) = pmpReadCfgReg(unsigned(idx)) // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. function clause read_CSR(0x3B @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b00 @ idx)) function clause read_CSR(0x3C @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b01 @ idx)) @@ -60,14 +60,14 @@ function clause read_CSR(0x3D @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b10 @ function clause read_CSR(0x3E @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b11 @ idx)) /* machine mode counters */ -function clause read_CSR(0xB00) = mcycle[(sizeof(xlen) - 1) .. 0] -function clause read_CSR(0xB02) = minstret[(sizeof(xlen) - 1) .. 0] -function clause read_CSR(0xB80 if sizeof(xlen) == 32)= mcycle[63 .. 32] -function clause read_CSR(0xB82 if sizeof(xlen) == 32) = minstret[63 .. 32] +function clause read_CSR(0xB00) = mcycle[(xlen - 1) .. 0] +function clause read_CSR(0xB02) = minstret[(xlen - 1) .. 0] +function clause read_CSR(0xB80 if xlen == 32)= mcycle[63 .. 32] +function clause read_CSR(0xB82 if xlen == 32) = minstret[63 .. 32] /* Hardware Performance Monitoring machine mode counters */ function clause read_CSR(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index)) -function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if sizeof(xlen) == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) +function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) /* vector */ function clause read_CSR(0x008) = zero_extend(vstart) @@ -88,7 +88,7 @@ function clause read_CSR(0x103) = sideleg.bits function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits function clause read_CSR(0x105) = get_stvec() function clause read_CSR(0x106) = zero_extend(scounteren.bits) -function clause read_CSR(0x10A) = senvcfg.bits[sizeof(xlen) - 1 .. 0] +function clause read_CSR(0x10A) = senvcfg.bits[xlen - 1 .. 0] function clause read_CSR(0x140) = sscratch function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask() function clause read_CSR(0x142) = scause.bits @@ -97,16 +97,16 @@ function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits function clause read_CSR(0x180) = satp /* user mode counters */ -function clause read_CSR(0xC00) = mcycle[(sizeof(xlen) - 1) .. 0] -function clause read_CSR(0xC01) = mtime[(sizeof(xlen) - 1) .. 0] -function clause read_CSR(0xC02) = minstret[(sizeof(xlen) - 1) .. 0] -function clause read_CSR(0xC80 if sizeof(xlen) == 32) = mcycle[63 .. 32] -function clause read_CSR(0xC81 if sizeof(xlen) == 32) = mtime[63 .. 32] -function clause read_CSR(0xC82 if sizeof(xlen) == 32) = minstret[63 .. 32] +function clause read_CSR(0xC00) = mcycle[(xlen - 1) .. 0] +function clause read_CSR(0xC01) = mtime[(xlen - 1) .. 0] +function clause read_CSR(0xC02) = minstret[(xlen - 1) .. 0] +function clause read_CSR(0xC80 if xlen == 32) = mcycle[63 .. 32] +function clause read_CSR(0xC81 if xlen == 32) = mtime[63 .. 32] +function clause read_CSR(0xC82 if xlen == 32) = minstret[63 .. 32] /* Hardware Performance Monitoring user mode counters */ function clause read_CSR(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index)) -function clause read_CSR(0b1100100 /* 0xC80 */ @ index : bits(5) if sizeof(xlen) == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) +function clause read_CSR(0b1100100 /* 0xC80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) /* user mode: Zkr */ function clause read_CSR(0x015) = read_seed_csr() @@ -119,10 +119,10 @@ function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits } function clause write_CSR(0x305, value) = { set_mtvec(value) } function clause write_CSR(0x306, value) = { mcounteren = legalize_mcounteren(mcounteren, value); zero_extend(mcounteren.bits) } -function clause write_CSR((0x30A, value) if sizeof(xlen) == 32) = { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); menvcfg.bits[31 .. 0] } -function clause write_CSR((0x30A, value) if sizeof(xlen) == 64) = { menvcfg = legalize_menvcfg(menvcfg, value); menvcfg.bits } -function clause write_CSR((0x310, value) if sizeof(xlen) == 32) = { mstatush.bits } // ignore writes for now -function clause write_CSR((0x31A, value) if sizeof(xlen) == 32) = { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); menvcfg.bits[63 .. 32] } +function clause write_CSR((0x30A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); menvcfg.bits[31 .. 0] } +function clause write_CSR((0x30A, value) if xlen == 64) = { menvcfg = legalize_menvcfg(menvcfg, value); menvcfg.bits } +function clause write_CSR((0x310, value) if xlen == 32) = { mstatush.bits } // ignore writes for now +function clause write_CSR((0x31A, value) if xlen == 32) = { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); menvcfg.bits[63 .. 32] } function clause write_CSR(0x320, value) = { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); zero_extend(mcountinhibit.bits) } function clause write_CSR(0x340, value) = { mscratch = value; mscratch } function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) } @@ -131,7 +131,7 @@ function clause write_CSR(0x343, value) = { mtval = value; mtval } function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits } // pmpcfgN -function clause write_CSR((0x3A @ idx : bits(4), value) if idx[0] == bitzero | sizeof(xlen) == 32) = { +function clause write_CSR((0x3A @ idx : bits(4), value) if idx[0] == bitzero | xlen == 32) = { let idx = unsigned(idx); pmpWriteCfgReg(idx, value); pmpReadCfgReg(idx) @@ -144,10 +144,10 @@ function clause write_CSR(0x3D @ idx : bits(4), value) = { let idx = unsigned(0b function clause write_CSR(0x3E @ idx : bits(4), value) = { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) } /* machine mode counters */ -function clause write_CSR(0xB00, value) = { mcycle[(sizeof(xlen) - 1) .. 0] = value; value } -function clause write_CSR(0xB02, value) = { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; value } -function clause write_CSR((0xB80, value) if sizeof(xlen) == 32) = { mcycle[63 .. 32] = value; value } -function clause write_CSR((0xB82, value) if sizeof(xlen) == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value } +function clause write_CSR(0xB00, value) = { mcycle[(xlen - 1) .. 0] = value; value } +function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; minstret_increment = false; value } +function clause write_CSR((0xB80, value) if xlen == 32) = { mcycle[63 .. 32] = value; value } +function clause write_CSR((0xB82, value) if xlen == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value } /* Hardware Performance Monitoring machine mode counters */ function clause write_CSR((0b0011001 /* 0x320 */ @ index : bits(5), value) if unsigned(index) >= 3) = { @@ -160,7 +160,7 @@ function clause write_CSR((0b1011000 /* 0xB00 */ @ index : bits(5), value) if un write_mhpmcounter(index, value); read_mhpmcounter(index) } -function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if sizeof(xlen) == 32 & unsigned(index) >= 3) = { +function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if xlen == 32 & unsigned(index) >= 3) = { let index = hpmidx_from_bits(index); write_mhpmcounterh(index, value); read_mhpmcounterh(index) @@ -176,7 +176,7 @@ function clause write_CSR(0x103, value) = { sideleg.bits = value; sideleg.bits } function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits } function clause write_CSR(0x105, value) = { set_stvec(value) } function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) } -function clause write_CSR(0x10A, value) = { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); senvcfg.bits[sizeof(xlen) - 1 .. 0] } +function clause write_CSR(0x10A, value) = { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); senvcfg.bits[xlen - 1 .. 0] } function clause write_CSR(0x140, value) = { sscratch = value; sscratch } function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) } function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits } diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail index 4bb94eefa..d4a3c9107 100644 --- a/model/riscv_insts_zkn.sail +++ b/model/riscv_insts_zkn.sail @@ -80,8 +80,8 @@ function clause extensionEnabled(Ext_Zkne) = true union clause ast = AES32ESMI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 - <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 +mapping clause encdec = AES32ESMI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & xlen == 32 + <-> bs @ 0b10011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & xlen == 32 mapping clause assembly = AES32ESMI (bs, rs2, rs1, rd) <-> "aes32esmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -98,8 +98,8 @@ function clause execute (AES32ESMI (bs, rs2, rs1, rd)) = { union clause ast = AES32ESI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 - <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 32 +mapping clause encdec = AES32ESI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & xlen == 32 + <-> bs @ 0b10001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & xlen == 32 mapping clause assembly = AES32ESI (bs, rs2, rs1, rd) <-> "aes32esi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -123,8 +123,8 @@ function clause extensionEnabled(Ext_Zknd) = true union clause ast = AES32DSMI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 - <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 +mapping clause encdec = AES32DSMI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & xlen == 32 + <-> bs @ 0b10111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & xlen == 32 mapping clause assembly = AES32DSMI (bs, rs2, rs1, rd) <-> "aes32dsmi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -141,8 +141,8 @@ function clause execute (AES32DSMI (bs, rs2, rs1, rd)) = { union clause ast = AES32DSI : (bits(2), regidx, regidx, regidx) -mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 - <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 32 +mapping clause encdec = AES32DSI (bs, rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & xlen == 32 + <-> bs @ 0b10101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & xlen == 32 mapping clause assembly = AES32DSI (bs, rs2, rs1, rd) <-> "aes32dsi" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) ^ sep() ^ hex_bits_2(bs) @@ -168,23 +168,23 @@ union clause ast = SHA512SIG1H : (regidx, regidx, regidx) union clause ast = SHA512SUM0R : (regidx, regidx, regidx) union clause ast = SHA512SUM1R : (regidx, regidx, regidx) -mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 - <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 +mapping clause encdec = SHA512SUM0R (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 32 + <-> 0b01 @ 0b01000 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & xlen == 32 -mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 - <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 +mapping clause encdec = SHA512SUM1R (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 32 + <-> 0b01 @ 0b01001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & xlen == 32 -mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 - <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG0L (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 32 + <-> 0b01 @ 0b01010 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & xlen == 32 -mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 - <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG0H (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 32 + <-> 0b01 @ 0b01110 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & xlen == 32 -mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 - <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG1L (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 32 + <-> 0b01 @ 0b01011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & xlen == 32 -mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 - <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 32 +mapping clause encdec = SHA512SIG1H (rs2, rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 32 + <-> 0b01 @ 0b01111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknh) & xlen == 32 mapping clause assembly = SHA512SIG0L (rs2, rs1, rd) <-> "sha512sig0l" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) @@ -253,26 +253,26 @@ union clause ast = AES64ES : (regidx, regidx, regidx) union clause ast = AES64DSM : (regidx, regidx, regidx) union clause ast = AES64DS : (regidx, regidx, regidx) -mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & (sizeof(xlen) == 64) & (rnum <_u 0xB) - <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & (sizeof(xlen) == 64) & (rnum <_u 0xB) +mapping clause encdec = AES64KS1I (rnum, rs1, rd) if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & (xlen == 64) & (rnum <_u 0xB) + <-> 0b00 @ 0b11000 @ 0b1 @ rnum @ rs1 @ 0b001 @ rd @ 0b0010011 if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & (xlen == 64) & (rnum <_u 0xB) -mapping clause encdec = AES64IM (rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 - <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 +mapping clause encdec = AES64IM (rs1, rd) if extensionEnabled(Ext_Zknd) & xlen == 64 + <-> 0b00 @ 0b11000 @ 0b00000 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknd) & xlen == 64 -mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & sizeof(xlen) == 64 - <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & sizeof(xlen) == 64 +mapping clause encdec = AES64KS2 (rs2, rs1, rd) if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & xlen == 64 + <-> 0b01 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if (extensionEnabled(Ext_Zkne) | extensionEnabled(Ext_Zknd)) & xlen == 64 -mapping clause encdec = AES64ESM (rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 - <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 +mapping clause encdec = AES64ESM (rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & xlen == 64 + <-> 0b00 @ 0b11011 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & xlen == 64 -mapping clause encdec = AES64ES (rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 - <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & sizeof(xlen) == 64 +mapping clause encdec = AES64ES (rs2, rs1, rd) if extensionEnabled(Ext_Zkne) & xlen == 64 + <-> 0b00 @ 0b11001 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zkne) & xlen == 64 -mapping clause encdec = AES64DSM (rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 - <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 +mapping clause encdec = AES64DSM (rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & xlen == 64 + <-> 0b00 @ 0b11111 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & xlen == 64 -mapping clause encdec = AES64DS (rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 - <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & sizeof(xlen) == 64 +mapping clause encdec = AES64DS (rs2, rs1, rd) if extensionEnabled(Ext_Zknd) & xlen == 64 + <-> 0b00 @ 0b11101 @ rs2 @ rs1 @ 0b000 @ rd @ 0b0110011 if extensionEnabled(Ext_Zknd) & xlen == 64 mapping clause assembly = AES64KS1I (rnum, rs1, rd) <-> "aes64ks1i" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_4(rnum) @@ -299,7 +299,7 @@ mapping clause assembly = AES64DS (rs2, rs1, rd) the range 0x0..0xA. See the encdec clause for AES64KS1I. The rum == 0xA case is used specifically for the AES-256 KeySchedule */ function clause execute (AES64KS1I(rnum, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let prev : bits(32) = X(rs1)[63..32]; let subwords : bits(32) = aes_subword_fwd(prev); let result : bits(32) = if (rnum == 0xA) then subwords @@ -309,7 +309,7 @@ function clause execute (AES64KS1I(rnum, rs1, rd)) = { } function clause execute (AES64KS2(rs2, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let w0 : bits(32) = X(rs1)[63..32] ^ X(rs2)[31..0]; let w1 : bits(32) = X(rs1)[63..32] ^ X(rs2)[31..0] ^ X(rs2)[63..32]; X(rd) = w1 @ w0; @@ -317,7 +317,7 @@ function clause execute (AES64KS2(rs2, rs1, rd)) = { } function clause execute (AES64IM(rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let w0 : bits(32) = aes_mixcolumn_inv(X(rs1)[31.. 0]); let w1 : bits(32) = aes_mixcolumn_inv(X(rs1)[63..32]); X(rd) = w1 @ w0; @@ -325,7 +325,7 @@ function clause execute (AES64IM(rs1, rd)) = { } function clause execute (AES64ESM(rs2, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let sr : bits(64) = aes_rv64_shiftrows_fwd(X(rs2), X(rs1)); let wd : bits(64) = sr[63..0]; let sb : bits(64) = aes_apply_fwd_sbox_to_each_byte(wd); @@ -334,7 +334,7 @@ function clause execute (AES64ESM(rs2, rs1, rd)) = { } function clause execute (AES64ES(rs2, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let sr : bits(64) = aes_rv64_shiftrows_fwd(X(rs2), X(rs1)); let wd : bits(64) = sr[63..0]; X(rd) = aes_apply_fwd_sbox_to_each_byte(wd); @@ -342,7 +342,7 @@ function clause execute (AES64ES(rs2, rs1, rd)) = { } function clause execute (AES64DSM(rs2, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let sr : bits(64) = aes_rv64_shiftrows_inv(X(rs2), X(rs1)); let wd : bits(64) = sr[63..0]; let sb : bits(64) = aes_apply_inv_sbox_to_each_byte(wd); @@ -351,7 +351,7 @@ function clause execute (AES64DSM(rs2, rs1, rd)) = { } function clause execute (AES64DS(rs2, rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let sr : bits(64) = aes_rv64_shiftrows_inv(X(rs2), X(rs1)); let wd : bits(64) = sr[63..0]; X(rd) = aes_apply_inv_sbox_to_each_byte(wd); @@ -368,17 +368,17 @@ union clause ast = SHA512SIG1 : (regidx, regidx) union clause ast = SHA512SUM0 : (regidx, regidx) union clause ast = SHA512SUM1 : (regidx, regidx) -mapping clause encdec = SHA512SUM0 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 +mapping clause encdec = SHA512SUM0 (rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 64 + <-> 0b00 @ 0b01000 @ 0b00100 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & xlen == 64 -mapping clause encdec = SHA512SUM1 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 +mapping clause encdec = SHA512SUM1 (rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 64 + <-> 0b00 @ 0b01000 @ 0b00101 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & xlen == 64 -mapping clause encdec = SHA512SIG0 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 +mapping clause encdec = SHA512SIG0 (rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 64 + <-> 0b00 @ 0b01000 @ 0b00110 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & xlen == 64 -mapping clause encdec = SHA512SIG1 (rs1, rd) if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 - <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & sizeof(xlen) == 64 +mapping clause encdec = SHA512SIG1 (rs1, rd) if extensionEnabled(Ext_Zknh) & xlen == 64 + <-> 0b00 @ 0b01000 @ 0b00111 @ rs1 @ 0b001 @ rd @ 0b0010011 if extensionEnabled(Ext_Zknh) & xlen == 64 mapping clause assembly = SHA512SIG0 (rs1, rd) <-> "sha512sig0" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) @@ -395,7 +395,7 @@ mapping clause assembly = SHA512SUM1 (rs1, rd) /* Execute clauses for the 64-bit SHA512 instructions. */ function clause execute (SHA512SIG0(rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let input : bits(64) = X(rs1); let result : bits(64) = (input >>> 1) ^ (input >>> 8) ^ (input >> 7); X(rd) = result; @@ -403,7 +403,7 @@ function clause execute (SHA512SIG0(rs1, rd)) = { } function clause execute (SHA512SIG1(rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let input : bits(64) = X(rs1); let result : bits(64) = (input >>> 19) ^ (input >>> 61) ^ (input >> 6); X(rd) = result; @@ -411,7 +411,7 @@ function clause execute (SHA512SIG1(rs1, rd)) = { } function clause execute (SHA512SUM0(rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let input : bits(64) = X(rs1); let result : bits(64) = (input >>> 28) ^ (input >>> 34) ^ (input >>> 39); X(rd) = result; @@ -419,7 +419,7 @@ function clause execute (SHA512SUM0(rs1, rd)) = { } function clause execute (SHA512SUM1(rs1, rd)) = { - assert(sizeof(xlen) == 64); + assert(xlen == 64); let input : bits(64) = X(rs1); let result : bits(64) = (input >>> 14) ^ (input >>> 18) ^ (input >>> 41); X(rd) = result; diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index a17e86d32..018512336 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -22,7 +22,7 @@ function get_next_pc() = nextPC val set_next_pc : xlenbits -> unit function set_next_pc(pc) = { - sail_branch_announce(sizeof(xlen), pc); + sail_branch_announce(xlen, pc); nextPC = pc } diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 6155e1c13..e407d8aae 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -60,7 +60,7 @@ val plat_clint_size = pure {interpreter: "Platform.clint_size", c: "plat_clint_s /* Location of HTIF ports */ val plat_htif_tohost = pure {c: "plat_htif_tohost", lem: "plat_htif_tohost"} : unit -> xlenbits -function plat_htif_tohost () = to_bits(sizeof(xlen), elf_tohost ()) +function plat_htif_tohost () = to_bits(xlen, elf_tohost ()) // todo: fromhost val phys_mem_segments : unit -> list((xlenbits, xlenbits)) diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index ce53caf06..9862b245d 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -113,7 +113,7 @@ function accessToFault(acc : AccessType(ext_access_type)) -> ExceptionType = function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: int('n), acc: AccessType(ext_access_type), priv: Privilege) -> option(ExceptionType) = { - let width : xlenbits = to_bits(sizeof(xlen), width); + let width : xlenbits = to_bits(xlen, width); foreach (i from 0 to 63) { let prev_pmpaddr = (if i > 0 then pmpReadAddrReg(i - 1) else zeros()); diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 46ab8020c..3764f3533 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -46,7 +46,7 @@ register pmpaddr_n : vector(64, xlenbits) /* Packing and unpacking pmpcfg regs for xlen-width accesses */ function pmpReadCfgReg(n : range(0, 15)) -> xlenbits = { - if sizeof(xlen) == 32 + if xlen == 32 then { pmpcfg_n[n*4 + 3].bits @ pmpcfg_n[n*4 + 2].bits @ @@ -74,13 +74,13 @@ function pmpReadAddrReg(n : range(0, 63)) -> xlenbits = { match match_type[1] { bitone if G >= 2 => { // [G-2..0] read as all ones to form mask, therefore we need G-1 bits. - let mask : xlenbits = zero_extend(ones(min(G - 1, sizeof(xlen)))); + let mask : xlenbits = zero_extend(ones(min(G - 1, xlen))); addr | mask }, bitzero if G >= 1 => { // [G-1..0] read as all zeros to form mask, therefore we need G bits. - let mask : xlenbits = zero_extend(ones(min(G , sizeof(xlen)))); + let mask : xlenbits = zero_extend(ones(min(G , xlen))); addr & ~(mask) }, @@ -117,7 +117,7 @@ function pmpWriteCfg(n: range(0, 63), cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent } function pmpWriteCfgReg(n : range(0, 15), v : xlenbits) -> unit = { - if sizeof(xlen) == 32 + if xlen == 32 then { foreach (i from 0 to 3) { let idx = n*4 + i; @@ -134,7 +134,7 @@ function pmpWriteCfgReg(n : range(0, 15), v : xlenbits) -> unit = { } function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits) -> xlenbits = - if sizeof(xlen) == 32 + if xlen == 32 then { if (locked | tor_locked) then reg else v } else { if (locked | tor_locked) then reg else zero_extend(v[53..0]) } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 8a8c9daa7..6a06caec3 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -34,8 +34,8 @@ function clause is_CSR_defined(0x304) = true // mie function clause is_CSR_defined(0x305) = true // mtvec function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren function clause is_CSR_defined(0x30A) = extensionEnabled(Ext_U) // menvcfg -function clause is_CSR_defined(0x310) = sizeof(xlen) == 32 // mstatush -function clause is_CSR_defined(0x31A) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // menvcfgh +function clause is_CSR_defined(0x310) = xlen == 32 // mstatush +function clause is_CSR_defined(0x31A) = extensionEnabled(Ext_U) & (xlen == 32) // menvcfgh function clause is_CSR_defined(0x320) = true // mcountinhibit @@ -47,7 +47,7 @@ function clause is_CSR_defined(0x343) = true // mtval function clause is_CSR_defined(0x344) = true // mip // pmpcfgN -function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32) +function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | xlen == 32) // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. function clause is_CSR_defined(0x3B) @ idx : bits(4) = sys_pmp_count() > unsigned(0b00 @ idx) @@ -63,10 +63,10 @@ function clause is_CSR_defined(0xB02) = true // minstret function clause is_CSR_defined(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmcounter3..31 -function clause is_CSR_defined(0xB80) = sizeof(xlen) == 32 // mcycleh -function clause is_CSR_defined(0xB82) = sizeof(xlen) == 32 // minstreth +function clause is_CSR_defined(0xB80) = xlen == 32 // mcycleh +function clause is_CSR_defined(0xB82) = xlen == 32 // minstreth -function clause is_CSR_defined(0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & (sizeof(xlen) == 32) // mhpmcounterh3..31 +function clause is_CSR_defined(0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & (xlen == 32) // mhpmcounterh3..31 /* disabled trigger/debug module */ function clause is_CSR_defined(0x7a0) = true @@ -97,11 +97,11 @@ function clause is_CSR_defined(0xC02) = extensionEnabled(Ext_U) // instret function clause is_CSR_defined(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) // hpmcounter3..31 -function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // cycleh -function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // timeh -function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // instreth +function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (xlen == 32) // cycleh +function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (xlen == 32) // timeh +function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (xlen == 32) // instreth -function clause is_CSR_defined(0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // hpmcounterh3..31 +function clause is_CSR_defined(0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (xlen == 32) // hpmcounterh3..31 /* user mode: Zkr */ function clause is_CSR_defined(0x015) = extensionEnabled(Ext_Zkr) @@ -499,7 +499,7 @@ function init_sys() -> unit = { mhartid = zero_extend(0b0); mconfigptr = zero_extend(0b0); - misa[MXL] = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); + misa[MXL] = arch_to_bits(if xlen == 32 then RV32 else RV64); misa[A] = 0b1; /* atomics */ misa[C] = bool_to_bits(sys_enable_rvc()); /* RVC */ misa[B] = bool_to_bits(sys_enable_bext()); /* Bit-manipulation */ @@ -524,7 +524,7 @@ function init_sys() -> unit = { mstatus[MPP] = privLevel_to_bits(lowest_supported_privLevel()); /* set to little-endian mode */ - if sizeof(xlen) == 64 then { + if xlen == 64 then { mstatus = Mk_Mstatus([mstatus.bits with 37 .. 36 = 0b00]) }; mstatush.bits = zero_extend(0b0); @@ -552,7 +552,7 @@ function init_sys() -> unit = { /* initialize vector csrs */ elen = 0b1; /* ELEN=64 as the common case */ vlen = 0b0100; /* VLEN=512 as a default value */ - vlenb = to_bits(sizeof(xlen), 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */ + vlenb = to_bits(xlen, 2 ^ (get_vlen_pow() - 3)); /* vlenb holds the constant value VLEN/8 */ /* VLEN value needs to be manually changed currently. * See riscv_vlen.sail for details. */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 65336f2e1..9df7bf8f7 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -214,13 +214,13 @@ function effectivePrivilege(t : AccessType(ext_access_type), m : Mstatus, priv : else priv function get_mstatus_SXL(m : Mstatus) -> arch_xlen = { - if sizeof(xlen) == 32 + if xlen == 32 then arch_to_bits(RV32) else m.bits[35 .. 34] } function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { - if sizeof(xlen) == 32 + if xlen == 32 then m else { let m = vector_update_subrange(m.bits, 35, 34, a); @@ -229,13 +229,13 @@ function set_mstatus_SXL(m : Mstatus, a : arch_xlen) -> Mstatus = { } function get_mstatus_UXL(m : Mstatus) -> arch_xlen = { - if sizeof(xlen) == 32 + if xlen == 32 then arch_to_bits(RV32) else m.bits[33 .. 32] } function set_mstatus_UXL(m : Mstatus, a : arch_xlen) -> Mstatus = { - if sizeof(xlen) == 32 + if xlen == 32 then m else { let m = vector_update_subrange(m.bits, 33, 32, a); @@ -273,7 +273,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { let m = set_mstatus_UXL(m, get_mstatus_UXL(o)); /* We don't currently support changing MBE and SBE. */ - let m = if sizeof(xlen) == 64 then { + let m = if xlen == 64 then { Mk_Mstatus([m.bits with 37 .. 36 = 0b00]) } else m; @@ -519,13 +519,13 @@ function hpmidx_from_bits(b : bits(5)) -> hpmidx = { index } -function read_mhpmcounter(index : hpmidx) -> xlenbits = mhpmcounter[index][(sizeof(xlen) - 1) .. 0] +function read_mhpmcounter(index : hpmidx) -> xlenbits = mhpmcounter[index][(xlen - 1) .. 0] function read_mhpmcounterh(index : hpmidx) -> bits(32) = mhpmcounter[index][63 .. 32] function read_mhpmevent(index : hpmidx) -> xlenbits = mhpmevent[index] // Write the HPM CSRs. These return the new value of the CSR, for use in writeCSR. function write_mhpmcounter(index : hpmidx, value : xlenbits) -> unit = - if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][(sizeof(xlen) - 1) .. 0] = value + if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][(xlen - 1) .. 0] = value function write_mhpmcounterh(index : hpmidx, value : bits(32)) -> unit = if sys_writable_hpm_counters()[index] == bitone then mhpmcounter[index][63 .. 32] = value diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 94c57a34e..c333c4e17 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -22,11 +22,11 @@ scattered function extensionEnabled /* this value is only defined for the runtime platform for ELF loading * checks, and not used in the model. */ -let xlen_val = sizeof(xlen) +let xlen_val = xlen -let xlen_max_unsigned = 2 ^ sizeof(xlen) - 1 -let xlen_max_signed = 2 ^ (sizeof(xlen) - 1) - 1 -let xlen_min_signed = 0 - 2 ^ (sizeof(xlen) - 1) +let xlen_max_unsigned = 2 ^ xlen - 1 +let xlen_max_signed = 2 ^ (xlen - 1) - 1 +let xlen_min_signed = 0 - 2 ^ (xlen - 1) type half = bits(16) type word = bits(32) @@ -408,5 +408,5 @@ struct mul_op = { val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a function report_invalid_width(f , l, w, k) -> 'a = { internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^ - " with xlen=" ^ dec_str(sizeof(xlen))) + " with xlen=" ^ dec_str(xlen)) } diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail index e846439a9..6b394354d 100644 --- a/model/riscv_vmem.sail +++ b/model/riscv_vmem.sail @@ -40,7 +40,7 @@ function vpn_j_of_va(sv_params : SV_Params, va : bits(64), level : PTW_Level) -> bits(64) = { let lsb : range(0,63) = pagesize_bits + level * sv_params.vpn_size_bits; - assert (lsb < sizeof(xlen)); + assert (lsb < xlen); let mask : bits(64) = zero_extend(ones(sv_params.vpn_size_bits)); ((va >> lsb) & mask) } @@ -101,7 +101,7 @@ function pt_walk(sv_params, // Below, 'pte_phys_addr' is XLEN bits because it's an arg to // 'mem_read_priv()' [riscv_mem.sail] where it's declared as xlenbits. // That def and this use need to be fixed together (TODO) - let pte_phys_addr : xlenbits = pte_addr[(sizeof(xlen) - 1) .. 0]; + let pte_phys_addr : xlenbits = pte_addr[(xlen - 1) .. 0]; // Read this-level PTE from mem let mem_result = mem_read_priv(Read(Data), // AccessType @@ -187,22 +187,22 @@ function legalize_satp(a : Architecture, o : xlenbits, // previous value of satp v : xlenbits) // proposed new value of satp -> xlenbits = { // new legal value of satp - if sizeof(xlen) == 32 then { + if xlen == 32 then { // The slice and extend ops below are no-ops when xlen==32, // but appease the type-checker when xlen==64 (when this code is not executed!) let o32 : bits(32) = o[31 .. 0]; let v32 : bits(32) = v[31 .. 0]; let new_satp : bits(32) = legalize_satp32(a, o32, v32); zero_extend(new_satp); - } else if sizeof(xlen) == 64 then { + } else if xlen == 64 then { // The extend and truncate ops below are no-ops when xlen==64, // but appease the type-checker when xlen==32 (when this code is not executed!) let o64 : bits(64) = zero_extend(o); let v64 : bits(64) = zero_extend(v); let new_satp : bits(64) = legalize_satp64(a, o64, v64); - truncate(new_satp, sizeof(xlen)) + truncate(new_satp, xlen) } else - internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(sizeof(xlen))) + internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(xlen)) } // ---------------- @@ -211,18 +211,18 @@ function legalize_satp(a : Architecture, // ASID is 9b in Sv32, 16b in Sv39/Sv48/Sv57: we use 16b for both // PRIVATE function satp_to_asid(satp_val : xlenbits) -> asidbits = - if sizeof(xlen) == 32 then zero_extend(Mk_Satp32(satp_val)[Asid]) - else if sizeof(xlen) == 64 then Mk_Satp64(satp_val)[Asid] + if xlen == 32 then zero_extend(Mk_Satp32(satp_val)[Asid]) + else if xlen == 64 then Mk_Satp64(satp_val)[Asid] else internal_error(__FILE__, __LINE__, - "Unsupported xlen" ^ dec_str(sizeof(xlen))) + "Unsupported xlen" ^ dec_str(xlen)) // Result is 64b to cover both RV32 and RV64 addrs // PRIVATE function satp_to_PT_base(satp_val : xlenbits) -> bits(64) = { - let ppn = if sizeof(xlen) == 32 then zero_extend (64, Mk_Satp32(satp_val)[PPN]) - else if sizeof(xlen) == 64 then zero_extend (64, Mk_Satp64(satp_val)[PPN]) + let ppn = if xlen == 32 then zero_extend (64, Mk_Satp32(satp_val)[PPN]) + else if xlen == 64 then zero_extend (64, Mk_Satp64(satp_val)[PPN]) else internal_error(__FILE__, __LINE__, - "Unsupported xlen" ^ dec_str(sizeof(xlen))); + "Unsupported xlen" ^ dec_str(xlen)); ppn << pagesize_bits } @@ -231,12 +231,12 @@ function satp_to_PT_base(satp_val : xlenbits) -> bits(64) = { function translationMode(priv : Privilege) -> SATPMode = { if priv == Machine then Sbare - else if sizeof(xlen) == 32 then + else if xlen == 32 then match Mk_Satp32(satp)[Mode] { 0b0 => Sbare, 0b1 => Sv32 } - else if sizeof(xlen) == 64 then { + else if xlen == 64 then { // Translation mode is based on mstatus.SXL, which could be RV32 when xlen==64 let arch = architecture(get_mstatus_SXL(mstatus)); match arch { @@ -316,7 +316,7 @@ function translate_TLB_hit(sv_params : SV_Params, // Writeback the PTE (which has new A/D bits) let n_ent = {ent with pte=pte'}; write_TLB(tlb_index, n_ent); - let pte_phys_addr = ent.pteAddr[(sizeof(xlen) - 1) .. 0]; + let pte_phys_addr = ent.pteAddr[(xlen - 1) .. 0]; match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => (), @@ -362,7 +362,7 @@ function translate_TLB_miss(sv_params : SV_Params, TR_Failure(PTW_PTE_Update(), ext_ptw) else { // Writeback the PTE (which has new A/D bits) - let pte_phys_addr = pteAddr[(sizeof(xlen) - 1) .. 0]; + let pte_phys_addr = pteAddr[(xlen - 1) .. 0]; match write_pte(pte_phys_addr, 2 ^ sv_params.log_pte_size_bytes, pte') { MemValue(_) => { @@ -435,7 +435,7 @@ function translateAddr(vAddr : xlenbits, init_ext_ptw); // Fixup result PA or exception match tr_result1 { - TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw), + TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, xlen), ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } }