diff --git a/model/prelude.sail b/model/prelude.sail index 24363b93f..5ff8a1213 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -187,11 +187,11 @@ function get_config_print_reg () = false function get_config_print_mem () = false function get_config_print_platform () = false -val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) -val EXTZ : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) +val sign_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) +val zero_extend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) -function EXTS(m, v) = sail_sign_extend(v, m) -function EXTZ(m, v) = sail_zero_extend(v, m) +function sign_extend(m, v) = sail_sign_extend(v, m) +function zero_extend(m, v) = sail_zero_extend(v, m) val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) function zeros_implicit (n) = sail_zeros(n) @@ -245,11 +245,11 @@ overload operator << = {shift_bits_left, shiftl} /* Ideally these would be sail builtin */ function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = - let v128 : bits(128) = EXTS(v) in + let v128 : bits(128) = sign_extend(v) in (v128 >> shift)[63..0] function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = - let v64 : bits(64) = EXTS(v) in + let v64 : bits(64) = sign_extend(v) in (v64 >> shift)[31..0] infix 7 >>> diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 02f5d959e..21e3e50aa 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -98,14 +98,14 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst }, RISCV_JAL(imm, rd) => { if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = EXTS(imm) in + let offset : bits(64) = sign_extend(imm) in Nias = [| NIAFP_concrete_address (PC + offset) |]; ik = IK_branch(); }, RISCV_JALR(imm, rs, rd) => { if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = EXTS(imm) in + let offset : bits(64) = sign_extend(imm) in Nias = [| NIAFP_indirect_address() |]; ik = IK_branch(); }, @@ -113,7 +113,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; ik = IK_branch(); - let offset : bits(64) = EXTS(imm) in + let offset : bits(64) = sign_extend(imm) in Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; }, ITYPE(imm, rs, rd, op) => { @@ -271,14 +271,14 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst }, RISCV_JAL(imm, rd) => { if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = EXTS(imm) in + let offset : bits(64) = sign_extend(imm) in Nias = [| NIAFP_concrete_address (PC + offset) |]; ik = IK_branch(); }, RISCV_JALR(imm, rs, rd) => { if (rs == 0b00000) then () else iR = RFull(GPRstr(rs)) :: iR; if (rd == 0b00000) then () else oR = RFull(GPRstr(rd)) :: oR; - let offset : bits(64) = EXTS(imm) in + let offset : bits(64) = sign_extend(imm) in Nias = [| NIAFP_indirect_address() |]; ik = IK_branch(); }, @@ -286,7 +286,7 @@ function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,inst if (rs2 == 0b00000) then () else iR = RFull(GPRstr(rs2)) :: iR; if (rs1 == 0b00000) then () else iR = RFull(GPRstr(rs1)) :: iR; ik = IK_branch(); - let offset : bits(64) = EXTS(imm) in + let offset : bits(64) = sign_extend(imm) in Nias = [| NIAFP_concrete_address(PC + offset), NIAFP_successor() |]; }, ITYPE(imm, rs, rd, op) => { diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 8724db867..768aede02 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -83,12 +83,12 @@ function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx() function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx() function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx() -function clause ext_read_CSR (0x001) = Some (EXTZ (fcsr.FFLAGS())) -function clause ext_read_CSR (0x002) = Some (EXTZ (fcsr.FRM())) -function clause ext_read_CSR (0x003) = Some (EXTZ (fcsr.bits())) +function clause ext_read_CSR (0x001) = Some (zero_extend (fcsr.FFLAGS())) +function clause ext_read_CSR (0x002) = Some (zero_extend (fcsr.FRM())) +function clause ext_read_CSR (0x003) = Some (zero_extend (fcsr.bits())) -function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(EXTZ(fcsr.FFLAGS())) } -function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(EXTZ(fcsr.FRM())) } -function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(EXTZ(fcsr.bits())) } +function clause ext_write_CSR (0x001, value) = { ext_write_fcsr (fcsr.FRM(), value [4..0]); Some(zero_extend(fcsr.FFLAGS())) } +function clause ext_write_CSR (0x002, value) = { ext_write_fcsr (value [2..0], fcsr.FFLAGS()); Some(zero_extend(fcsr.FRM())) } +function clause ext_write_CSR (0x003, value) = { ext_write_fcsr (value [7..5], value [4..0]); Some(zero_extend(fcsr.bits())) } /* **************************************************************** */ diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index d2af59fef..f2e0fb33c 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -356,7 +356,7 @@ function wF_or_X_H(i, data) = { assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_H(i) = data - else X(i) = EXTS(data) + else X(i) = sign_extend(data) } val wF_or_X_S : (bits(5), bits(32)) -> unit effect {escape, wreg} @@ -365,7 +365,7 @@ function wF_or_X_S(i, data) = { assert(sys_enable_fdext() != sys_enable_zfinx()); if sys_enable_fdext() then F_S(i) = data - else X(i) = EXTS(data) + else X(i) = sign_extend(data) } val wF_or_X_D : (bits(5), bits(64)) -> unit effect {escape, wreg} @@ -375,7 +375,7 @@ function wF_or_X_D(i, data) = { if sys_enable_fdext() then F_D(i) = data else if sizeof(xlen) >= 64 - then X(i) = EXTS(data) + then X(i) = sign_extend(data) else { assert (i[0] == bitzero); if i != zeros() then { diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index de17b8f55..b036c1b84 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -70,9 +70,9 @@ function fetch() -> FetchResult = { rvfi_inst_data->rvfi_order() = minstret; - rvfi_pc_data->rvfi_pc_rdata() = EXTZ(get_arch_pc()); - rvfi_inst_data->rvfi_mode() = EXTZ(privLevel_to_bits(cur_privilege)); - rvfi_inst_data->rvfi_ixl() = EXTZ(misa.MXL()); + rvfi_pc_data->rvfi_pc_rdata() = zero_extend(get_arch_pc()); + rvfi_inst_data->rvfi_mode() = zero_extend(privLevel_to_bits(cur_privilege)); + rvfi_inst_data->rvfi_ixl() = zero_extend(misa.MXL()); /* First allow extensions to check pc */ match ext_fetch_check_pc(PC, PC) { @@ -85,7 +85,7 @@ function fetch() -> FetchResult = { TR_Failure(e, _) => F_Error(e, PC), TR_Address(_, _) => { let i = rvfi_instruction.rvfi_insn(); - rvfi_inst_data->rvfi_insn() = EXTZ(i); + rvfi_inst_data->rvfi_insn() = zero_extend(i); if (i[1 .. 0] != 0b11) then F_RVC(i[15 .. 0]) else { diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail index 816fb90c9..fc41f631e 100644 --- a/model/riscv_freg_type.sail +++ b/model/riscv_freg_type.sail @@ -74,7 +74,7 @@ type fregtype = flenbits /* default zero register */ -let zero_freg : fregtype = EXTZ(0x0) +let zero_freg : fregtype = zero_extend(0x0) /* default register printer */ val FRegStr : fregtype -> string diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 6e64101d1..b1bfcef88 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -179,7 +179,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { /* should only happen in rmem * rmem: allow SC to fail very early */ - X(rd) = EXTZ(0b1); RETIRE_SUCCESS + X(rd) = zero_extend(0b1); RETIRE_SUCCESS } else { if haveAtomics() then { /* normal non-rmem case @@ -206,7 +206,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { else { if match_reservation(vaddr) == false then { /* cannot happen in rmem */ - X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS + X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS } else { match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here: * both result in a SAMO exception */ @@ -231,8 +231,8 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { _ => internal_error(__FILE__, __LINE__, "STORECON expected word or double") }; match (res) { - MemValue(true) => { X(rd) = EXTZ(0b0); cancel_reservation(); RETIRE_SUCCESS }, - MemValue(false) => { X(rd) = EXTZ(0b1); cancel_reservation(); RETIRE_SUCCESS }, + MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS }, + MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS }, MemException(e) => { handle_mem_exception(addr, e); RETIRE_FAIL } } } @@ -297,9 +297,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { _ => false }; let rs2_val : xlenbits = match width { - BYTE => if is_unsigned then EXTZ(X(rs2)[7..0]) else EXTS(X(rs2)[7..0]), - HALF => if is_unsigned then EXTZ(X(rs2)[15..0]) else EXTS(X(rs2)[15..0]), - WORD => if is_unsigned then EXTZ(X(rs2)[31..0]) else EXTS(X(rs2)[31..0]), + BYTE => if is_unsigned then zero_extend(X(rs2)[7..0]) else sign_extend(X(rs2)[7..0]), + HALF => if is_unsigned then zero_extend(X(rs2)[15..0]) else sign_extend(X(rs2)[15..0]), + WORD => if is_unsigned then zero_extend(X(rs2)[31..0]) else sign_extend(X(rs2)[31..0]), DOUBLE => X(rs2) }; match (eares) { @@ -332,9 +332,9 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = { AMOMAXU => to_bits(sizeof(xlen), max(unsigned(rs2_val), unsigned(loaded))) }; let rval : xlenbits = match width { - BYTE => EXTS(loaded[7..0]), - HALF => EXTS(loaded[15..0]), - WORD => EXTS(loaded[31..0]), + BYTE => sign_extend(loaded[7..0]), + HALF => sign_extend(loaded[15..0]), + WORD => sign_extend(loaded[31..0]), DOUBLE => loaded }; let wval : MemoryOpResult(bool) = match (width, sizeof(xlen)) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index eccaac4f5..d68e7a34f 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -84,7 +84,7 @@ mapping clause encdec = UTYPE(imm, rd, op) <-> imm @ rd @ encdec_uop(op) function clause execute UTYPE(imm, rd, op) = { - let off : xlenbits = EXTS(imm @ 0x000); + let off : xlenbits = sign_extend(imm @ 0x000); let ret : xlenbits = match op { RISCV_LUI => off, RISCV_AUIPC => get_arch_pc() + off @@ -120,7 +120,7 @@ but this is difficult */ function clause execute (RISCV_JAL(imm, rd)) = { - let t : xlenbits = PC + EXTS(imm); + let t : xlenbits = PC + sign_extend(imm); /* Extensions get the first checks on the prospective target address. */ match ext_control_check_pc(t) { Ext_ControlAddr_Error(e) => { @@ -184,7 +184,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = { RISCV_BLTU => rs1_val <_u rs2_val, RISCV_BGEU => rs1_val >=_u rs2_val }; - let t : xlenbits = PC + EXTS(imm); + let t : xlenbits = PC + sign_extend(imm); if taken then { /* Extensions get the first checks on the prospective target address. */ match ext_control_check_pc(t) { @@ -234,11 +234,11 @@ mapping clause encdec = ITYPE(imm, rs1, rd, op) function clause execute (ITYPE (imm, rs1, rd, op)) = { let rs1_val = X(rs1); - let immext : xlenbits = EXTS(imm); + let immext : xlenbits = sign_extend(imm); let result : xlenbits = match op { RISCV_ADDI => rs1_val + immext, - RISCV_SLTI => EXTZ(bool_to_bits(rs1_val <_s immext)), - RISCV_SLTIU => EXTZ(bool_to_bits(rs1_val <_u immext)), + RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)), + RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)), RISCV_ANDI => rs1_val & immext, RISCV_ORI => rs1_val | immext, RISCV_XORI => rs1_val ^ immext @@ -318,8 +318,8 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = { let rs2_val = X(rs2); let result : xlenbits = match op { RISCV_ADD => rs1_val + rs2_val, - RISCV_SLT => EXTZ(bool_to_bits(rs1_val <_s rs2_val)), - RISCV_SLTU => EXTZ(bool_to_bits(rs1_val <_u rs2_val)), + RISCV_SLT => zero_extend(bool_to_bits(rs1_val <_s rs2_val)), + RISCV_SLTU => zero_extend(bool_to_bits(rs1_val <_u rs2_val)), RISCV_AND => rs1_val & rs2_val, RISCV_OR => rs1_val | rs2_val, RISCV_XOR => rs1_val ^ rs2_val, @@ -364,7 +364,7 @@ mapping clause encdec = LOAD(imm, rs1, rd, is_unsigned, size, false, false) if ( val extend_value : forall 'n, 0 < 'n <= xlen_bytes. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits) function extend_value(is_unsigned, value) = match (value) { - MemValue(v) => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits), + MemValue(v) => MemValue(if is_unsigned then zero_extend(v) else sign_extend(v) : xlenbits), MemException(e) => MemException(e) } @@ -385,7 +385,7 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool = } function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = { - let offset : xlenbits = EXTS(imm); + let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), width) { @@ -441,7 +441,7 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false) /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = { - let offset : xlenbits = EXTS(imm); + let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Write(Data), width) { @@ -494,8 +494,8 @@ mapping clause encdec = ADDIW(imm, rs1, rd) if sizeof(xlen) == 64 function clause execute (ADDIW(imm, rs1, rd)) = { - let result : xlenbits = EXTS(imm) + X(rs1); - X(rd) = EXTS(result[31..0]); + let result : xlenbits = sign_extend(imm) + X(rs1); + X(rd) = sign_extend(result[31..0]); RETIRE_SUCCESS } @@ -527,7 +527,7 @@ function clause execute (SHIFTW(shamt, rs1, rd, op)) = { RISCV_SRLI => rs1_val >> shamt, RISCV_SRAI => shift_right_arith32(rs1_val, shamt) }; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -576,7 +576,7 @@ function clause execute (RTYPEW(rs2, rs1, rd, op)) = { RISCV_SRLW => rs1_val >> (rs2_val[4..0]), RISCV_SRAW => shift_right_arith32(rs1_val, rs2_val[4..0]) }; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -616,7 +616,7 @@ function clause execute (SHIFTIWOP(shamt, rs1, rd, op)) = { RISCV_SRLIW => rs1_val[31..0] >> shamt, RISCV_SRAIW => shift_right_arith32(rs1_val[31..0], shamt) }; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail index dd95469c3..8851e348f 100644 --- a/model/riscv_insts_cdext.sail +++ b/model/riscv_insts_cdext.sail @@ -84,7 +84,7 @@ mapping clause encdec_compressed = C_FLDSP(ui86 @ ui5 @ ui43, rd) if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() function clause execute (C_FLDSP(uimm, rd)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); execute(LOAD_FP(imm, sp, rd, DOUBLE)) } @@ -102,7 +102,7 @@ mapping clause encdec_compressed = C_FSDSP(ui86 @ ui53, rs2) if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() function clause execute (C_FSDSP(uimm, rs2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); execute(STORE_FP(imm, rs2, sp, DOUBLE)) } @@ -120,7 +120,7 @@ mapping clause encdec_compressed = C_FLD(ui76 @ ui53, rs1, rd) if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() function clause execute (C_FLD(uimm, rsc, rdc)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); let rd = creg2reg_idx(rdc); let rs = creg2reg_idx(rsc); execute(LOAD_FP(imm, rs, rd, DOUBLE)) @@ -140,7 +140,7 @@ mapping clause encdec_compressed = C_FSD(ui76 @ ui53, rs1, rs2) if (sizeof(xlen) == 32 | sizeof(xlen) == 64) & haveRVC() & haveDExt() function clause execute (C_FSD(uimm, rsc1, rsc2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); let rs1 = creg2reg_idx(rsc1); let rs2 = creg2reg_idx(rsc2); execute(STORE_FP(imm, rs2, rs1, DOUBLE)) diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail index 42bc2e70f..f9f49d39b 100644 --- a/model/riscv_insts_cext.sail +++ b/model/riscv_insts_cext.sail @@ -113,7 +113,7 @@ mapping clause encdec_compressed = C_LW(ui6 @ ui53 @ ui2, rs1, rd) <-> 0b010 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rd : cregidx @ 0b00 function clause execute (C_LW(uimm, rsc, rdc)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); let rd = creg2reg_idx(rdc); let rs = creg2reg_idx(rsc); execute(LOAD(imm, rs, rd, false, WORD, false, false)) @@ -131,7 +131,7 @@ mapping clause encdec_compressed = C_LD(ui76 @ ui53, rs1, rd) if sizeof(xlen) == 64 function clause execute (C_LD(uimm, rsc, rdc)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); let rd = creg2reg_idx(rdc); let rs = creg2reg_idx(rsc); execute(LOAD(imm, rs, rd, false, DOUBLE, false, false)) @@ -149,7 +149,7 @@ mapping clause encdec_compressed = C_SW(ui6 @ ui53 @ ui2, rs1, rs2) <-> 0b110 @ ui53 : bits(3) @ rs1 : cregidx @ ui2 : bits(1) @ ui6 : bits(1) @ rs2 : cregidx @ 0b00 function clause execute (C_SW(uimm, rsc1, rsc2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); let rs1 = creg2reg_idx(rsc1); let rs2 = creg2reg_idx(rsc2); execute(STORE(imm, rs2, rs1, WORD, false, false)) @@ -167,7 +167,7 @@ mapping clause encdec_compressed = C_SD(ui76 @ ui53, rs1, rs2) if sizeof(xlen) == 64 function clause execute (C_SD(uimm, rsc1, rsc2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); let rs1 = creg2reg_idx(rsc1); let rs2 = creg2reg_idx(rsc2); execute(STORE(imm, rs2, rs1, DOUBLE, false, false)) @@ -187,7 +187,7 @@ mapping clause encdec_compressed = C_ADDI(nzi5 @ nzi40, rsd) if nzi5 @ nzi40 != 0b000000 & rsd != zreg function clause execute (C_ADDI(nzi, rsd)) = { - let imm : bits(12) = EXTS(nzi); + let imm : bits(12) = sign_extend(nzi); execute(ITYPE(imm, rsd, rsd, RISCV_ADDI)) } @@ -205,7 +205,7 @@ mapping clause encdec_compressed = C_JAL(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i if sizeof(xlen) == 32 function clause execute (C_JAL(imm)) = - execute(RISCV_JAL(EXTS(imm @ 0b0), ra)) + execute(RISCV_JAL(sign_extend(imm @ 0b0), ra)) mapping clause assembly = C_JAL(imm) if sizeof(xlen) == 32 @@ -221,7 +221,7 @@ mapping clause encdec_compressed = C_ADDIW(imm5 @ imm40, rsd) if rsd != zreg & sizeof(xlen) == 64 function clause execute (C_ADDIW(imm, rsd)) = - execute(ADDIW(EXTS(imm), rsd, rsd)) + execute(ADDIW(sign_extend(imm), rsd, rsd)) mapping clause assembly = C_ADDIW(imm, rsd) if sizeof(xlen) == 64 @@ -237,7 +237,7 @@ mapping clause encdec_compressed = C_LI(imm5 @ imm40, rd) if rd != zreg function clause execute (C_LI(imm, rd)) = { - let imm : bits(12) = EXTS(imm); + let imm : bits(12) = sign_extend(imm); execute(ITYPE(imm, zreg, rd, RISCV_ADDI)) } @@ -255,7 +255,7 @@ mapping clause encdec_compressed = C_ADDI16SP(nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4) if nzi9 @ nzi87 @ nzi6 @ nzi5 @ nzi4 != 0b000000 function clause execute (C_ADDI16SP(imm)) = { - let imm : bits(12) = EXTS(imm @ 0x0); + let imm : bits(12) = sign_extend(imm @ 0x0); execute(ITYPE(imm, sp, sp, RISCV_ADDI)) } @@ -273,7 +273,7 @@ mapping clause encdec_compressed = C_LUI(imm17 @ imm1612, rd) if rd != zreg & rd != sp & imm17 @ imm1612 != 0b000000 function clause execute (C_LUI(imm, rd)) = { - let res : bits(20) = EXTS(imm); + let res : bits(20) = sign_extend(imm); execute(UTYPE(res, rd, RISCV_LUI)) } @@ -326,7 +326,7 @@ mapping clause encdec_compressed = C_ANDI(i5 @ i40, rsd) function clause execute (C_ANDI(imm, rsd)) = { let rsd = creg2reg_idx(rsd); - execute(ITYPE(EXTS(imm), rsd, rsd, RISCV_ANDI)) + execute(ITYPE(sign_extend(imm), rsd, rsd, RISCV_ANDI)) } mapping clause assembly = C_ANDI(imm, rsd) @@ -437,7 +437,7 @@ mapping clause encdec_compressed = C_J(i11 @ i10 @ i98 @ i7 @ i6 @ i5 @ i4 @ i31 <-> 0b101 @ 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 function clause execute (C_J(imm)) = - execute(RISCV_JAL(EXTS(imm @ 0b0), zreg)) + execute(RISCV_JAL(sign_extend(imm @ 0b0), zreg)) mapping clause assembly = C_J(imm) <-> "c.j" ^ spc() ^ hex_bits_11(imm) @@ -449,7 +449,7 @@ mapping clause encdec_compressed = C_BEQZ(i8 @ i76 @ i5 @ i43 @ i21, rs) <-> 0b110 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 function clause execute (C_BEQZ(imm, rs)) = - execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ)) + execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BEQ)) mapping clause assembly = C_BEQZ(imm, rs) <-> "c.beqz" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_8(imm) @@ -461,7 +461,7 @@ mapping clause encdec_compressed = C_BNEZ(i8 @ i76 @ i5 @ i43 @ i21, rs) <-> 0b111 @ i8 : bits(1) @ i43 : bits(2) @ rs : cregidx @ i76 : bits(2) @ i21 : bits(2) @ i5 : bits(1) @ 0b01 function clause execute (C_BNEZ(imm, rs)) = - execute(BTYPE(EXTS(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE)) + execute(BTYPE(sign_extend(imm @ 0b0), zreg, creg2reg_idx(rs), RISCV_BNE)) mapping clause assembly = C_BNEZ(imm, rs) <-> "c.bnez" ^ spc() ^ creg_name(rs) ^ sep() ^ hex_bits_8(imm) @@ -491,7 +491,7 @@ mapping clause encdec_compressed = C_LWSP(ui76 @ ui5 @ ui42, rd) if rd != zreg function clause execute (C_LWSP(uimm, rd)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); execute(LOAD(imm, sp, rd, false, WORD, false, false)) } @@ -509,7 +509,7 @@ mapping clause encdec_compressed = C_LDSP(ui86 @ ui5 @ ui43, rd) if rd != zreg & sizeof(xlen) == 64 function clause execute (C_LDSP(uimm, rd)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); execute(LOAD(imm, sp, rd, false, DOUBLE, false, false)) } @@ -525,7 +525,7 @@ mapping clause encdec_compressed = C_SWSP(ui76 @ ui52, rs2) <-> 0b110 @ ui52 : bits(4) @ ui76 : bits(2) @ rs2 : regidx @ 0b10 function clause execute (C_SWSP(uimm, rs2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); execute(STORE(imm, rs2, sp, WORD, false, false)) } @@ -541,7 +541,7 @@ mapping clause encdec_compressed = C_SDSP(ui86 @ ui53, rs2) if sizeof(xlen) == 64 function clause execute (C_SDSP(uimm, rs2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b000); + let imm : bits(12) = zero_extend(uimm @ 0b000); execute(STORE(imm, rs2, sp, DOUBLE, false, false)) } @@ -559,7 +559,7 @@ mapping clause encdec_compressed = C_JR(rs1) if rs1 != zreg function clause execute (C_JR(rs1)) = - execute(RISCV_JALR(EXTZ(0b0), rs1, zreg)) + execute(RISCV_JALR(zero_extend(0b0), rs1, zreg)) mapping clause assembly = C_JR(rs1) if rs1 != zreg @@ -575,7 +575,7 @@ mapping clause encdec_compressed = C_JALR(rs1) if rs1 != zreg function clause execute (C_JALR(rs1)) = - execute(RISCV_JALR(EXTZ(0b0), rs1, ra)) + execute(RISCV_JALR(zero_extend(0b0), rs1, ra)) mapping clause assembly = C_JALR(rs1) if rs1 != zreg diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail index b952901f5..632495ee4 100644 --- a/model/riscv_insts_cfext.sail +++ b/model/riscv_insts_cfext.sail @@ -84,7 +84,7 @@ mapping clause encdec_compressed = C_FLWSP(ui76 @ ui5 @ ui42, rd) if sizeof(xlen) == 32 & haveRVC() & haveFExt() function clause execute (C_FLWSP(imm, rd)) = { - let imm : bits(12) = EXTZ(imm @ 0b00); + let imm : bits(12) = zero_extend(imm @ 0b00); execute(LOAD_FP(imm, sp, rd, WORD)) } @@ -102,7 +102,7 @@ mapping clause encdec_compressed = C_FSWSP(ui76 @ ui52, rs2) if sizeof(xlen) == 32 & haveRVC() & haveFExt() function clause execute (C_FSWSP(uimm, rs2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); execute(STORE_FP(imm, rs2, sp, WORD)) } @@ -120,7 +120,7 @@ mapping clause encdec_compressed = C_FLW(ui6 @ ui53 @ ui2, rs1, rd) if sizeof(xlen) == 32 & haveRVC() & haveFExt() function clause execute (C_FLW(uimm, rsc, rdc)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); let rd = creg2reg_idx(rdc); let rs = creg2reg_idx(rsc); execute(LOAD_FP(imm, rs, rd, WORD)) @@ -140,7 +140,7 @@ mapping clause encdec_compressed = C_FSW(ui6 @ ui53 @ ui2, rs1, rs2) if sizeof(xlen) == 32 & haveRVC() & haveFExt() function clause execute (C_FSW(uimm, rsc1, rsc2)) = { - let imm : bits(12) = EXTZ(uimm @ 0b00); + let imm : bits(12) = zero_extend(uimm @ 0b00); let rs1 = creg2reg_idx(rsc1); let rs2 = creg2reg_idx(rsc2); execute(STORE_FP(imm, rs2, rs1, WORD)) diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index ff1c4c179..5afde5c97 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -517,7 +517,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_W_D)) = { let (fflags, rd_val_W) = riscv_f64ToI32 (rm_3b, rs1_val_D); write_fflags(fflags); - X(rd) = EXTS (rd_val_W); + X(rd) = sign_extend (rd_val_W); RETIRE_SUCCESS } } @@ -532,7 +532,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_WU_D)) = { let (fflags, rd_val_WU) = riscv_f64ToUi32 (rm_3b, rs1_val_D); write_fflags(fflags); - X(rd) = EXTS (rd_val_WU); + X(rd) = sign_extend (rd_val_WU); RETIRE_SUCCESS } } @@ -608,7 +608,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_L_D)) = { let (fflags, rd_val_L) = riscv_f64ToI64 (rm_3b, rs1_val_D); write_fflags(fflags); - X(rd) = EXTS(rd_val_L); + X(rd) = sign_extend(rd_val_L); RETIRE_SUCCESS } } @@ -624,7 +624,7 @@ function clause execute (F_UN_RM_TYPE_D(rs1, rm, rd, FCVT_LU_D)) = { let (fflags, rd_val_LU) = riscv_f64ToUi64 (rm_3b, rs1_val_D); write_fflags(fflags); - X(rd) = EXTS(rd_val_LU); + X(rd) = sign_extend(rd_val_LU); RETIRE_SUCCESS } } @@ -863,7 +863,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = { riscv_f64Eq (rs1_val_D, rs2_val_D); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -875,7 +875,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = { riscv_f64Lt (rs1_val_D, rs2_val_D); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -887,7 +887,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = { riscv_f64Le (rs1_val_D, rs2_val_D); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -988,14 +988,14 @@ function clause execute (F_UN_TYPE_D(rs1, rd, FCLASS_D)) = { else if f_is_QNaN_D (rs1_val_D) then 0b_10_0000_0000 else zeros(); - X(rd) = EXTZ (rd_val_10b); + X(rd) = zero_extend (rd_val_10b); RETIRE_SUCCESS } function clause execute (F_UN_TYPE_D(rs1, rd, FMV_X_D)) = { assert(sizeof(xlen) >= 64); let rs1_val_D = F(rs1)[63..0]; - let rd_val_X : xlenbits = EXTS(rs1_val_D); + let rd_val_X : xlenbits = sign_extend(rs1_val_D); X(rd) = rd_val_X; RETIRE_SUCCESS } diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index c7e1541f3..e60b96b5d 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -374,7 +374,7 @@ function process_fload16(rd, addr, value) = } function clause execute(LOAD_FP(imm, rs1, rd, width)) = { - let offset : xlenbits = EXTS(imm); + let offset : xlenbits = sign_extend(imm); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ match ext_data_get_addr(rs1, offset, Read(Data), width) { @@ -439,7 +439,7 @@ function process_fstore(vaddr, value) = } function clause execute (STORE_FP(imm, rs2, rs1, width)) = { - let offset : xlenbits = EXTS(imm); + let offset : xlenbits = sign_extend(imm); let (aq, rl, con) = (false, false, false); /* Get the address, X(rs1) + offset. Some extensions perform additional checks on address validity. */ @@ -686,7 +686,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_W_S)) = { let (fflags, rd_val_W) = riscv_f32ToI32 (rm_3b, rs1_val_S); write_fflags(fflags); - X(rd) = EXTS (rd_val_W); + X(rd) = sign_extend (rd_val_W); RETIRE_SUCCESS } } @@ -701,7 +701,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_WU_S)) = { let (fflags, rd_val_WU) = riscv_f32ToUi32 (rm_3b, rs1_val_S); write_fflags(fflags); - X(rd) = EXTS (rd_val_WU); + X(rd) = sign_extend (rd_val_WU); RETIRE_SUCCESS } } @@ -747,7 +747,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_L_S)) = { let (fflags, rd_val_L) = riscv_f32ToI64 (rm_3b, rs1_val_S); write_fflags(fflags); - X(rd) = EXTS(rd_val_L); + X(rd) = sign_extend(rd_val_L); RETIRE_SUCCESS } } @@ -763,7 +763,7 @@ function clause execute (F_UN_RM_TYPE_S(rs1, rm, rd, FCVT_LU_S)) = { let (fflags, rd_val_LU) = riscv_f32ToUi64 (rm_3b, rs1_val_S); write_fflags(fflags); - X(rd) = EXTS(rd_val_LU); + X(rd) = sign_extend(rd_val_LU); RETIRE_SUCCESS } } @@ -987,7 +987,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = { riscv_f32Eq (rs1_val_S, rs2_val_S); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -999,7 +999,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = { riscv_f32Lt (rs1_val_S, rs2_val_S); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -1011,7 +1011,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = { riscv_f32Le (rs1_val_S, rs2_val_S); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -1110,13 +1110,13 @@ function clause execute (F_UN_TYPE_S(rs1, rd, FCLASS_S)) = { else if f_is_QNaN_S (rs1_val_S) then 0b_10_0000_0000 else zeros(); - X(rd) = EXTZ (rd_val_10b); + X(rd) = zero_extend (rd_val_10b); RETIRE_SUCCESS } function clause execute (F_UN_TYPE_S(rs1, rd, FMV_X_W)) = { let rs1_val_S = F(rs1)[31..0]; - let rd_val_X : xlenbits = EXTS(rs1_val_S); + let rd_val_X : xlenbits = sign_extend(rs1_val_S); X(rd) = rd_val_X; RETIRE_SUCCESS } diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index de0e093be..7cee33789 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -186,7 +186,7 @@ function clause execute (MULW(rs2, rs1, rd)) = { let rs2_int : int = signed(rs2_val); /* to_bits requires expansion to 64 bits followed by truncation */ let result32 = to_bits(64, rs1_int * rs2_int)[31..0]; - let result : xlenbits = EXTS(result32); + let result : xlenbits = sign_extend(result32); X(rd) = result; RETIRE_SUCCESS } else { @@ -217,7 +217,7 @@ function clause execute (DIVW(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 > (2 ^ 31 - 1) then (0 - 2^31) else q; - X(rd) = EXTS(to_bits(32, q')); + X(rd) = sign_extend(to_bits(32, q')); RETIRE_SUCCESS } else { handle_illegal(); @@ -246,7 +246,7 @@ function clause execute (REMW(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) = EXTS(to_bits(32, r)); + X(rd) = sign_extend(to_bits(32, r)); RETIRE_SUCCESS } else { handle_illegal(); diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail index 20bd7feb4..2e474defd 100644 --- a/model/riscv_insts_zba.sail +++ b/model/riscv_insts_zba.sail @@ -79,7 +79,7 @@ mapping clause assembly = RISCV_SLLIUW(shamt, rs1, rd) function clause execute (RISCV_SLLIUW(shamt, rs1, rd)) = { let rs1_val = X(rs1); - let result : xlenbits = EXTZ(rs1_val[31..0]) << shamt; + let result : xlenbits = zero_extend(rs1_val[31..0]) << shamt; X(rd) = result; RETIRE_SUCCESS } @@ -118,7 +118,7 @@ function clause execute (ZBA_RTYPEUW(rs2, rs1, rd, op)) = { RISCV_SH2ADDUW => 0b10, RISCV_SH3ADDUW => 0b11 }; - let result : xlenbits = (EXTZ(rs1_val[31..0]) << shamt) + rs2_val; + let result : xlenbits = (zero_extend(rs1_val[31..0]) << shamt) + rs2_val; X(rd) = result; RETIRE_SUCCESS } diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index 1aecbc5ab..62e456764 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -79,7 +79,7 @@ mapping clause assembly = RISCV_RORIW(shamt, rs1, rd) function clause execute (RISCV_RORIW(shamt, rs1, rd)) = { let rs1_val = (X(rs1))[31..0]; - let result : xlenbits = EXTS(rs1_val >>> shamt); + let result : xlenbits = sign_extend(rs1_val >>> shamt); X(rd) = result; RETIRE_SUCCESS } @@ -126,7 +126,7 @@ function clause execute (ZBB_RTYPEW(rs2, rs1, rd, op)) = { RISCV_ROLW => rs1_val <<< shamt, RISCV_RORW => rs1_val >>> shamt }; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -224,9 +224,9 @@ mapping clause assembly = ZBB_EXTOP(rs1, rd, op) function clause execute (ZBB_EXTOP(rs1, rd, op)) = { let rs1_val = X(rs1); let result : xlenbits = match op { - RISCV_SEXTB => EXTS(rs1_val[7..0]), - RISCV_SEXTH => EXTS(rs1_val[15..0]), - RISCV_ZEXTH => EXTZ(rs1_val[15..0]) + RISCV_SEXTB => sign_extend(rs1_val[7..0]), + RISCV_SEXTH => sign_extend(rs1_val[15..0]), + RISCV_ZEXTH => zero_extend(rs1_val[15..0]) }; X(rd) = result; RETIRE_SUCCESS diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail index fd993d990..5983fe6b3 100644 --- a/model/riscv_insts_zbkb.sail +++ b/model/riscv_insts_zbkb.sail @@ -90,7 +90,7 @@ function clause execute (ZBKB_RTYPE(rs2, rs1, rd, op)) = { let rs2_val = X(rs2); let result : xlenbits = match op { RISCV_PACK => rs2_val[(sizeof(xlen_bytes)*4 - 1)..0] @ rs1_val[(sizeof(xlen_bytes)*4 - 1)..0], - RISCV_PACKH => EXTZ(rs2_val[7..0] @ rs1_val[7..0]) + RISCV_PACKH => zero_extend(rs2_val[7..0] @ rs1_val[7..0]) }; X(rd) = result; RETIRE_SUCCESS @@ -110,7 +110,7 @@ function clause execute (ZBKB_PACKW(rs2, rs1, rd)) = { let rs1_val = X(rs1); let rs2_val = X(rs2); let result : bits(32) = rs2_val[15..0] @ rs1_val[15..0]; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail index 0a79dd644..75a12b3c5 100644 --- a/model/riscv_insts_zbs.sail +++ b/model/riscv_insts_zbs.sail @@ -96,11 +96,11 @@ 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 - then EXTZ(0b1) << shamt[4..0] - else EXTZ(0b1) << shamt; + then zero_extend(0b1) << shamt[4..0] + else zero_extend(0b1) << shamt; let result : xlenbits = match op { RISCV_BCLRI => rs1_val & ~(mask), - RISCV_BEXTI => EXTZ(bool_to_bits((rs1_val & mask) != zeros())), + RISCV_BEXTI => zero_extend(bool_to_bits((rs1_val & mask) != zeros())), RISCV_BINVI => rs1_val ^ mask, RISCV_BSETI => rs1_val | mask }; @@ -137,11 +137,11 @@ 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 - then EXTZ(0b1) << rs2_val[4..0] - else EXTZ(0b1) << rs2_val[5..0]; + then zero_extend(0b1) << rs2_val[4..0] + else zero_extend(0b1) << rs2_val[5..0]; let result : xlenbits = match op { RISCV_BCLR => rs1_val & ~(mask), - RISCV_BEXT => EXTZ(bool_to_bits((rs1_val & mask) != zeros())), + RISCV_BEXT => zero_extend(bool_to_bits((rs1_val & mask) != zeros())), RISCV_BINV => rs1_val ^ mask, RISCV_BSET => rs1_val | mask }; diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 9a7f05cdc..cad5b1cde 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -576,7 +576,7 @@ mapping clause assembly = RISCV_FMVH_X_D(rs1, rd) function clause execute (RISCV_FMVH_X_D(rs1, rd)) = { let rs1_val_D = F_D(rs1)[63..32]; - let rd_val_X : xlenbits = EXTS(rs1_val_D); + let rd_val_X : xlenbits = sign_extend(rs1_val_D); X(rd) = rd_val_X; RETIRE_SUCCESS } @@ -628,7 +628,7 @@ function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = { riscv_f16Le_quiet (rs1_val_H, rs2_val_H); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -652,7 +652,7 @@ function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = { riscv_f16Lt_quiet (rs1_val_H, rs2_val_H); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -676,7 +676,7 @@ function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = { riscv_f32Le_quiet (rs1_val_S, rs2_val_S); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -700,7 +700,7 @@ function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = { riscv_f32Lt_quiet (rs1_val_S, rs2_val_S); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -725,7 +725,7 @@ function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = { riscv_f64Le_quiet (rs1_val_D, rs2_val_D); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -749,7 +749,7 @@ function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = { riscv_f64Lt_quiet (rs1_val_D, rs2_val_D); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -798,7 +798,7 @@ function fcvtmod_helper(x64) = { /* Perform the exponentation on the fixed-point mantissa and extract the integer part */ - let fixedpoint : bits(84) = EXTZ(true_mant) << true_exp; + let fixedpoint : bits(84) = zero_extend(true_mant) << true_exp; let integer = fixedpoint[83..52]; let fractional = fixedpoint[51..0]; @@ -829,6 +829,6 @@ function clause execute(RISCV_FCVTMOD_W_D(rs1, rd)) = { let rs1_val_D = F_D(rs1); let (fflags, rd_val) = fcvtmod_helper(rs1_val_D); write_fflags(fflags); - X(rd) = EXTS(rd_val); + X(rd) = sign_extend(rd_val); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index b30e5ab27..87ccab934 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -478,7 +478,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = { riscv_f16Eq (rs1_val_H, rs2_val_H); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -490,7 +490,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = { riscv_f16Lt (rs1_val_H, rs2_val_H); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -502,7 +502,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)) = { riscv_f16Le (rs1_val_H, rs2_val_H); write_fflags(fflags); - X(rd) = EXTZ(bool_to_bits(rd_val)); + X(rd) = zero_extend(bool_to_bits(rd_val)); RETIRE_SUCCESS } @@ -659,7 +659,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_W_H)) = { let (fflags, rd_val_W) = riscv_f16ToI32 (rm_3b, rs1_val_H); write_fflags(fflags); - X(rd) = EXTS (rd_val_W); + X(rd) = sign_extend (rd_val_W); RETIRE_SUCCESS } } @@ -674,7 +674,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_WU_H)) = { let (fflags, rd_val_WU) = riscv_f16ToUi32 (rm_3b, rs1_val_H); write_fflags(fflags); - X(rd) = EXTS (rd_val_WU); + X(rd) = sign_extend (rd_val_WU); RETIRE_SUCCESS } } @@ -781,7 +781,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_L_H)) = { let (fflags, rd_val_L) = riscv_f16ToI64 (rm_3b, rs1_val_H); write_fflags(fflags); - X(rd) = EXTS(rd_val_L); + X(rd) = sign_extend(rd_val_L); RETIRE_SUCCESS } } @@ -797,7 +797,7 @@ function clause execute (F_UN_RM_TYPE_H(rs1, rm, rd, FCVT_LU_H)) = { let (fflags, rd_val_LU) = riscv_f16ToUi64 (rm_3b, rs1_val_H); write_fflags(fflags); - X(rd) = EXTS(rd_val_LU); + X(rd) = sign_extend(rd_val_LU); RETIRE_SUCCESS } } @@ -967,13 +967,13 @@ function clause execute (F_UN_TYPE_H(rs1, rd, FCLASS_H)) = { else if f_is_QNaN_H (rs1_val_H) then 0b_10_0000_0000 else zeros(); - X(rd) = EXTZ (rd_val_10b); + X(rd) = zero_extend (rd_val_10b); RETIRE_SUCCESS } function clause execute (F_UN_TYPE_H(rs1, rd, FMV_X_H)) = { let rs1_val_H = F(rs1)[15..0]; - let rd_val_X : xlenbits = EXTS(rs1_val_H); + let rd_val_X : xlenbits = sign_extend(rs1_val_H); X(rd) = rd_val_X; RETIRE_SUCCESS } diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index b93283483..f6e767265 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -87,7 +87,7 @@ function readCSR csr : csreg -> xlenbits = { let res : xlenbits = match (csr, sizeof(xlen)) { /* machine mode */ - (0xF11, _) => EXTZ(mvendorid), + (0xF11, _) => zero_extend(mvendorid), (0xF12, _) => marchid, (0xF13, _) => mimpid, (0xF14, _) => mhartid, @@ -97,9 +97,9 @@ function readCSR csr : csreg -> xlenbits = { (0x303, _) => mideleg.bits(), (0x304, _) => mie.bits(), (0x305, _) => get_mtvec(), - (0x306, _) => EXTZ(mcounteren.bits()), + (0x306, _) => zero_extend(mcounteren.bits()), (0x310, 32) => mstatush.bits(), - (0x320, _) => EXTZ(mcountinhibit.bits()), + (0x320, _) => zero_extend(mcountinhibit.bits()), (0x340, _) => mscratch, (0x341, _) => get_xret_target(Machine) & pc_alignment_mask(), @@ -144,7 +144,7 @@ function readCSR csr : csreg -> xlenbits = { (0x103, _) => sideleg.bits(), (0x104, _) => lower_mie(mie, mideleg).bits(), (0x105, _) => get_stvec(), - (0x106, _) => EXTZ(scounteren.bits()), + (0x106, _) => zero_extend(scounteren.bits()), (0x140, _) => sscratch, (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), (0x142, _) => scause.bits(), @@ -167,7 +167,7 @@ function readCSR csr : csreg -> xlenbits = { match ext_read_CSR(csr) { Some(res) => res, None() => { print_bits("unhandled read to CSR ", csr); - EXTZ(0x0) } + zero_extend(0x0) } } }; if get_config_print_reg() @@ -185,9 +185,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x303, _) => { mideleg = legalize_mideleg(mideleg, value); Some(mideleg.bits()) }, (0x304, _) => { mie = legalize_mie(mie, value); Some(mie.bits()) }, (0x305, _) => { Some(set_mtvec(value)) }, - (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) }, + (0x306, _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(zero_extend(mcounteren.bits())) }, (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now - (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(EXTZ(mcountinhibit.bits())) }, + (0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(zero_extend(mcountinhibit.bits())) }, (0x340, _) => { mscratch = value; Some(mscratch) }, (0x341, _) => { Some(set_xret_target(Machine, value)) }, (0x342, _) => { mcause->bits() = value; Some(mcause.bits()) }, @@ -232,7 +232,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x103, _) => { sideleg->bits() = value; Some(sideleg.bits()) }, /* TODO: does this need legalization? */ (0x104, _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) }, (0x105, _) => { Some(set_stvec(value)) }, - (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) }, + (0x106, _) => { scounteren = legalize_scounteren(scounteren, value); Some(zero_extend(scounteren.bits())) }, (0x140, _) => { sscratch = value; Some(sscratch) }, (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, (0x142, _) => { scause->bits() = value; Some(scause.bits()) }, @@ -253,7 +253,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { } function clause execute CSR(csr, rs1, rd, is_imm, op) = { - let rs1_val : xlenbits = if is_imm then EXTZ(rs1) else X(rs1); + let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1); let isWrite : bool = match op { CSRRW => true, _ => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0 diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail index ddc51480c..43256ed3a 100644 --- a/model/riscv_insts_zkn.sail +++ b/model/riscv_insts_zkn.sail @@ -105,28 +105,28 @@ mapping clause assembly = SHA256SUM1 (rs1, rd) function clause execute (SHA256SIG0(rs1, rd)) = { let inb : bits(32) = X(rs1)[31..0]; let result : bits(32) = (inb >>> 7) ^ (inb >>> 18) ^ (inb >> 3); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } function clause execute (SHA256SIG1(rs1, rd)) = { let inb : bits(32) = X(rs1)[31..0]; let result : bits(32) = (inb >>> 17) ^ (inb >>> 19) ^ (inb >> 10); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } function clause execute (SHA256SUM0(rs1, rd)) = { let inb : bits(32) = X(rs1)[31..0]; let result : bits(32) = (inb >>> 2) ^ (inb >>> 13) ^ (inb >>> 22); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } function clause execute (SHA256SUM1(rs1, rd)) = { let inb : bits(32) = X(rs1)[31..0]; let result : bits(32) = (inb >>> 6) ^ (inb >>> 11) ^ (inb >>> 25); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -149,7 +149,7 @@ function clause execute (AES32ESMI (bs, rs2, rs1, rd)) = { let so : bits( 8) = aes_sbox_fwd(si); let mixed : bits(32) = aes_mixcolumn_byte_fwd(so); let result : bits(32) = X(rs1)[31..0] ^ (mixed <<< shamt); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -166,7 +166,7 @@ function clause execute (AES32ESI (bs, rs2, rs1, rd)) = { let si : bits( 8) = (X(rs2) >> shamt)[7..0]; /* SBox Input */ let so : bits(32) = 0x000000 @ aes_sbox_fwd(si); let result : bits(32) = X(rs1)[31..0] ^ (so <<< shamt); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -189,7 +189,7 @@ function clause execute (AES32DSMI (bs, rs2, rs1, rd)) = { let so : bits( 8) = aes_sbox_inv(si); let mixed : bits(32) = aes_mixcolumn_byte_inv(so); let result : bits(32) = X(rs1)[31..0] ^ (mixed <<< shamt); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -206,7 +206,7 @@ function clause execute (AES32DSI (bs, rs2, rs1, rd)) = { let si : bits( 8) = (X(rs2) >> shamt)[7..0]; /* SBox Input */ let so : bits(32) = 0x000000 @ aes_sbox_inv(si); let result : bits(32) = X(rs1)[31..0] ^ (so <<< shamt); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -259,37 +259,37 @@ mapping clause assembly = SHA512SUM1R (rs2, rs1, rd) <-> "sha512sum1r" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2) function clause execute (SHA512SIG0H(rs2, rs1, rd)) = { - X(rd) = EXTS((X(rs1) >> 1) ^ (X(rs1) >> 7) ^ (X(rs1) >> 8) ^ + X(rd) = sign_extend((X(rs1) >> 1) ^ (X(rs1) >> 7) ^ (X(rs1) >> 8) ^ (X(rs2) << 31) ^ (X(rs2) << 24)); RETIRE_SUCCESS } function clause execute (SHA512SIG0L(rs2, rs1, rd)) = { - X(rd) = EXTS((X(rs1) >> 1) ^ (X(rs1) >> 7) ^ (X(rs1) >> 8) ^ + X(rd) = sign_extend((X(rs1) >> 1) ^ (X(rs1) >> 7) ^ (X(rs1) >> 8) ^ (X(rs2) << 31) ^ (X(rs2) << 25) ^ (X(rs2) << 24)); RETIRE_SUCCESS } function clause execute (SHA512SIG1H(rs2, rs1, rd)) = { - X(rd) = EXTS((X(rs1) << 3) ^ (X(rs1) >> 6) ^ (X(rs1) >> 19) ^ + X(rd) = sign_extend((X(rs1) << 3) ^ (X(rs1) >> 6) ^ (X(rs1) >> 19) ^ (X(rs2) >> 29) ^ (X(rs2) << 13)); RETIRE_SUCCESS } function clause execute (SHA512SIG1L(rs2, rs1, rd)) = { - X(rd) = EXTS((X(rs1) << 3) ^ (X(rs1) >> 6) ^ (X(rs1) >> 19) ^ + X(rd) = sign_extend((X(rs1) << 3) ^ (X(rs1) >> 6) ^ (X(rs1) >> 19) ^ (X(rs2) >> 29) ^ (X(rs2) << 26) ^ (X(rs2) << 13)); RETIRE_SUCCESS } function clause execute (SHA512SUM0R(rs2, rs1, rd)) = { - X(rd) = EXTS((X(rs1) << 25) ^ (X(rs1) << 30) ^ (X(rs1) >> 28) ^ + X(rd) = sign_extend((X(rs1) << 25) ^ (X(rs1) << 30) ^ (X(rs1) >> 28) ^ (X(rs2) >> 7) ^ (X(rs2) >> 2) ^ (X(rs2) << 4)); RETIRE_SUCCESS } function clause execute (SHA512SUM1R(rs2, rs1, rd)) = { - X(rd) = EXTS((X(rs1) << 23) ^ (X(rs1) >> 14) ^ (X(rs1) >> 18) ^ + X(rd) = sign_extend((X(rs1) << 23) ^ (X(rs1) >> 14) ^ (X(rs1) >> 18) ^ (X(rs2) >> 9) ^ (X(rs2) << 18) ^ (X(rs2) << 14)); RETIRE_SUCCESS } diff --git a/model/riscv_insts_zks.sail b/model/riscv_insts_zks.sail index cdd8fd3b3..1c29d3ada 100644 --- a/model/riscv_insts_zks.sail +++ b/model/riscv_insts_zks.sail @@ -91,14 +91,14 @@ mapping clause assembly = SM3P1 (rs1, rd) <-> function clause execute (SM3P0(rs1, rd)) = { let r1 : bits(32) = X(rs1)[31..0]; let result : bits(32) = r1 ^ (r1 <<< 9) ^ (r1 <<< 17); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } function clause execute (SM3P1(rs1, rd)) = { let r1 : bits(32) = X(rs1)[31..0]; let result : bits(32) = r1 ^ (r1 <<< 15) ^ (r1 <<< 23); - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -131,7 +131,7 @@ function clause execute (SM4ED (bs, rs2, rs1, rd)) = { ((x & 0x000000C0) << 10); let z : bits(32) = (y <<< shamt); let result : bits(32) = z ^ X(rs1)[31..0]; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } @@ -143,6 +143,6 @@ function clause execute (SM4KS (bs, rs2, rs1, rd)) = { ((x & 0x00000001) << 23) ^ ((x & 0x000000F8) << 13) ; let z : bits(32) = (y <<< shamt); let result : bits(32) = z ^ X(rs1)[31..0]; - X(rd) = EXTS(result); + X(rd) = sign_extend(result); RETIRE_SUCCESS } diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index e9e4cbdbb..216cbfd11 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -74,7 +74,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { /* FIXME: this does not check for a misaligned target address. See riscv_jalr_seq.sail. */ /* write rd before anything else to prevent unintended strength */ X(rd) = nextPC; /* compatible with JALR, C.JR and C.JALR */ - let newPC : xlenbits = X(rs1) + EXTS(imm); + let newPC : xlenbits = X(rs1) + sign_extend(imm); nextPC = [newPC with 0 = bitzero]; /* Clear newPC[0] */ RETIRE_SUCCESS } diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index 9d370c64b..35d370b5e 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -77,7 +77,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = { * some manner, but for now, we just keep a reordered definition to improve simulator * performance. */ - let t : xlenbits = X(rs1) + EXTS(imm); + let t : xlenbits = X(rs1) + sign_extend(imm); /* Extensions get the first checks on the prospective target address. */ match ext_control_check_addr(t) { Ext_ControlAddr_Error(e) => { diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index fb3df0255..147258908 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -158,7 +158,7 @@ function pmp_mem_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_ $ifdef RVFI_DII val rvfi_read : forall 'n, 'n > 0. (xlenbits, atom('n), MemoryOpResult((bits(8 * 'n), mem_meta))) -> unit effect {wreg} function rvfi_read (addr, width, result) = { - rvfi_mem_data->rvfi_mem_addr() = EXTZ(addr); + rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); rvfi_mem_data_present = true; match result { /* TODO: report tag bit for capability writes and extend mask by one bit. */ @@ -232,7 +232,7 @@ function mem_write_ea (addr, width, aq, rl, con) = { $ifdef RVFI_DII val rvfi_write : forall 'n, 0 < 'n <= max_mem_access . (xlenbits, atom('n), bits(8 * 'n), mem_meta, MemoryOpResult(bool)) -> unit effect {wreg} function rvfi_write (addr, width, value, meta, result) = { - rvfi_mem_data->rvfi_mem_addr() = EXTZ(addr); + rvfi_mem_data->rvfi_mem_addr() = zero_extend(addr); rvfi_mem_data_present = true; match result { /* Log only the memory address (without the value) if the write fails. */ diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail index 507f50c11..b078bf88f 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -78,7 +78,7 @@ bitfield Ustatus : xlenbits = { /* This is a view, so there is no register defined. */ function lower_sstatus(s : Sstatus) -> Ustatus = { - let u = Mk_Ustatus(EXTZ(0b0)); + let u = Mk_Ustatus(zero_extend(0b0)); let u = update_UPIE(u, s.UPIE()); let u = update_UIE(u, s.UIE()); u @@ -106,7 +106,7 @@ bitfield Uinterrupts : xlenbits = { /* Provides the uip read view of sip (s) as delegated by sideleg (d). */ function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { - let u : Uinterrupts = Mk_Uinterrupts(EXTZ(0b0)); + let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); let u = update_UEI(u, s.UEI() & d.UEI()); let u = update_UTI(u, s.UTI() & d.UTI()); let u = update_USI(u, s.USI() & d.USI()); @@ -115,7 +115,7 @@ function lower_sip(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { /* Provides the uie read view of sie as delegated by sideleg. */ function lower_sie(s : Sinterrupts, d : Sinterrupts) -> Uinterrupts = { - let u : Uinterrupts = Mk_Uinterrupts(EXTZ(0b0)); + let u : Uinterrupts = Mk_Uinterrupts(zero_extend(0b0)); let u = update_UEI(u, s.UEI() & d.UEI()); let u = update_UTI(u, s.UTI() & d.UTI()); let u = update_USI(u, s.USI() & d.USI()); diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index aed996626..6194b8f9c 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -206,11 +206,11 @@ register mtimecmp : bits(64) // memory-mapped internal clint register. * bffc mtime hi */ -let MSIP_BASE : xlenbits = EXTZ(0x00000) -let MTIMECMP_BASE : xlenbits = EXTZ(0x04000) -let MTIMECMP_BASE_HI : xlenbits = EXTZ(0x04004) -let MTIME_BASE : xlenbits = EXTZ(0x0bff8) -let MTIME_BASE_HI : xlenbits = EXTZ(0x0bffc) +let MSIP_BASE : xlenbits = zero_extend(0x00000) +let MTIMECMP_BASE : xlenbits = zero_extend(0x04000) +let MTIMECMP_BASE_HI : xlenbits = zero_extend(0x04004) +let MTIME_BASE : xlenbits = zero_extend(0x0bff8) +let MTIME_BASE_HI : xlenbits = zero_extend(0x0bffc) val clint_load : forall 'n, 'n > 0. (AccessType(ext_access_type), xlenbits, int('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rreg} function clint_load(t, addr, width) = { @@ -359,7 +359,7 @@ register htif_payload_writes : bits(4) function reset_htif () -> unit = { htif_cmd_write = bitzero; htif_payload_writes = 0x0; - htif_tohost = EXTZ(0b0); + htif_tohost = zero_extend(0b0); } /* Since the htif tohost port is only available at a single address, @@ -394,7 +394,7 @@ function htif_store(paddr, width, data) = { if width == 8 then { htif_cmd_write = bitone; htif_payload_writes = htif_payload_writes + 1; - htif_tohost = EXTZ(data) } + htif_tohost = zero_extend(data) } else if width == 4 & paddr == plat_htif_tohost() then { if data == htif_tohost[31 .. 0] then htif_payload_writes = htif_payload_writes + 1 @@ -407,7 +407,7 @@ function htif_store(paddr, width, data) = { htif_cmd_write = bitone; htif_tohost = vector_update_subrange(htif_tohost, 63, 32, data) } /* unaligned command writes are not supported and will not be detected */ - else { htif_tohost = EXTZ(data) }; + else { htif_tohost = zero_extend(data) }; /* Execute if there were repeated writes of the same payload without * a cmd (e.g. in riscv-tests), or we have a complete htif command. @@ -487,11 +487,11 @@ function mmio_write forall 'n, 0 <'n <= max_mem_access . (paddr : xlenbits, widt /* Platform initialization and ticking. */ function init_platform() -> unit = { - htif_tohost = EXTZ(0b0); + htif_tohost = zero_extend(0b0); htif_done = false; - htif_exit_code = EXTZ(0b0); + htif_exit_code = zero_extend(0b0); htif_cmd_write = bitzero; - htif_payload_writes = EXTZ(0b0); + htif_payload_writes = zero_extend(0b0); } function tick_platform() -> unit = { diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 9b76c2db7..d02200669 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -221,4 +221,4 @@ function pmpWriteCfgReg(n, v) = { function pmpWriteAddr(locked: bool, tor_locked: bool, reg: xlenbits, v: xlenbits) -> xlenbits = if sizeof(xlen) == 32 then { if (locked | tor_locked) then reg else v } - else { if (locked | tor_locked) then reg else EXTZ(v[53..0]) } + else { if (locked | tor_locked) then reg else zero_extend(v[53..0]) } diff --git a/model/riscv_reg_type.sail b/model/riscv_reg_type.sail index 5428587fa..d338207c2 100644 --- a/model/riscv_reg_type.sail +++ b/model/riscv_reg_type.sail @@ -72,7 +72,7 @@ type regtype = xlenbits /* default zero register */ -let zero_reg : regtype = EXTZ(0x0) +let zero_reg : regtype = zero_extend(0x0) /* default register printer */ val RegStr : regtype -> string diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index 8391ef012..ec4a2c63e 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -154,7 +154,7 @@ function rX r = { $ifdef RVFI_DII val rvfi_wX : forall 'n, 0 <= 'n < 32. (regno('n), xlenbits) -> unit effect {wreg} function rvfi_wX (r,v) = { - rvfi_int_data->rvfi_rd_wdata() = EXTZ(v); + rvfi_int_data->rvfi_rd_wdata() = zero_extend(v); rvfi_int_data->rvfi_rd_addr() = to_bits(8,r); rvfi_int_data_present = true; } diff --git a/model/riscv_step.sail b/model/riscv_step.sail index ebf3b3fd8..550f11a4a 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -109,7 +109,7 @@ function step(step_no : int) -> bool = { }, /* non-error cases: */ F_RVC(h) => { - instbits = EXTZ(h); + instbits = zero_extend(h); let ast = ext_decode_compressed(h); if get_config_print_instr() then { @@ -125,7 +125,7 @@ function step(step_no : int) -> bool = { } }, F_Base(w) => { - instbits = EXTZ(w); + instbits = zero_extend(w); let ast = ext_decode(w); if get_config_print_instr() then { diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail index 585e64312..c266e6b87 100644 --- a/model/riscv_step_rvfi.sail +++ b/model/riscv_step_rvfi.sail @@ -76,7 +76,7 @@ function ext_pre_step_hook() -> unit = () function ext_post_step_hook() -> unit = { /* record the next pc */ - rvfi_pc_data->rvfi_pc_wdata() = EXTZ(get_arch_pc()) + rvfi_pc_data->rvfi_pc_wdata() = zero_extend(get_arch_pc()) } val ext_init : unit -> unit effect {wreg} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index c2d968095..d057ad6c0 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -287,9 +287,9 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits /* the others are delegated */ let effective_delg = xip.bits() & xideleg; /* we have pending interrupts if this privilege is enabled */ - if priv_enabled & (effective_pend != EXTZ(0b0)) + if priv_enabled & (effective_pend != zero_extend(0b0)) then Ints_Pending(effective_pend) - else if effective_delg != EXTZ(0b0) + else if effective_delg != zero_extend(0b0) then Ints_Delegated(effective_delg) else Ints_Empty() } @@ -304,7 +304,7 @@ function processPending(xip : Minterrupts, xie : Minterrupts, xideleg : xlenbits function getPendingSet(priv : Privilege) -> option((xlenbits, Privilege)) = { assert(haveUsrMode(), "no user mode: M/U or M/S/U system required"); let effective_pending = mip.bits() & mie.bits(); - if effective_pending == EXTZ(0b0) then None() /* fast path */ + if effective_pending == zero_extend(0b0) then None() /* fast path */ else { /* Higher privileges than the current one are implicitly enabled, * while lower privileges are blocked. An unsupported privilege is @@ -373,7 +373,7 @@ union ctl_result = { function tval(excinfo : option(xlenbits)) -> xlenbits = { match (excinfo) { Some(e) => e, - None() => EXTZ(0b0) + None() => zero_extend(0b0) } } @@ -402,7 +402,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen match (del_priv) { Machine => { mcause->IsInterrupt() = bool_to_bits(intr); - mcause->Cause() = EXTZ(c); + mcause->Cause() = zero_extend(c); mstatus->MPIE() = mstatus.MIE(); mstatus->MIE() = 0b0; @@ -423,7 +423,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen assert (haveSupMode(), "no supervisor mode present for delegation"); scause->IsInterrupt() = bool_to_bits(intr); - scause->Cause() = EXTZ(c); + scause->Cause() = zero_extend(c); mstatus->SPIE() = mstatus.SIE(); mstatus->SIE() = 0b0; @@ -448,7 +448,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen assert(haveUsrMode(), "no user mode present for delegation"); ucause->IsInterrupt() = bool_to_bits(intr); - ucause->Cause() = EXTZ(c); + ucause->Cause() = zero_extend(c); mstatus->UPIE() = mstatus.UIE(); mstatus->UIE() = 0b0; @@ -551,7 +551,7 @@ function handle_interrupt(i : InterruptType, del_priv : Privilege) -> unit = function init_sys() -> unit = { cur_privilege = Machine; - mhartid = EXTZ(0b0); + mhartid = zero_extend(0b0); misa->MXL() = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); misa->A() = 0b1; /* atomics */ @@ -578,31 +578,31 @@ function init_sys() -> unit = { if sizeof(xlen) == 64 then { mstatus = Mk_Mstatus([mstatus.bits() with 37 .. 36 = 0b00]) }; - mstatush->bits() = EXTZ(0b0); + mstatush->bits() = zero_extend(0b0); - mip->bits() = EXTZ(0b0); - mie->bits() = EXTZ(0b0); - mideleg->bits() = EXTZ(0b0); - medeleg->bits() = EXTZ(0b0); - mtvec->bits() = EXTZ(0b0); - mcause->bits() = EXTZ(0b0); - mepc = EXTZ(0b0); - mtval = EXTZ(0b0); - mscratch = EXTZ(0b0); + mip->bits() = zero_extend(0b0); + mie->bits() = zero_extend(0b0); + mideleg->bits() = zero_extend(0b0); + medeleg->bits() = zero_extend(0b0); + mtvec->bits() = zero_extend(0b0); + mcause->bits() = zero_extend(0b0); + mepc = zero_extend(0b0); + mtval = zero_extend(0b0); + mscratch = zero_extend(0b0); - mcycle = EXTZ(0b0); - mtime = EXTZ(0b0); + mcycle = zero_extend(0b0); + mtime = zero_extend(0b0); - mcounteren->bits() = EXTZ(0b0); + mcounteren->bits() = zero_extend(0b0); - minstret = EXTZ(0b0); + minstret = zero_extend(0b0); minstret_increment = true; init_pmp(); // log compatibility with spike if get_config_print_reg() - then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(EXTZ(0b0) : xlenbits) ^ ")") + then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")") } /* memory access exceptions, defined here for use by the platform model. */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index ecc7735b7..fedb02e9e 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -297,7 +297,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { * that does not have a matching bitfield entry. All bits above 32 are handled * explicitly later. */ - let m : Mstatus = Mk_Mstatus(EXTZ(v[22 .. 11] @ 0b00 @ v[8 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); + let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 11] @ 0b00 @ v[8 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0])); /* We don't have any extension context yet. */ let m = update_XS(m, extStatus_to_bits(Off)); @@ -480,7 +480,7 @@ function tvec_addr(m : Mtvec, c : Mcause) -> option(xlenbits) = { match (trapVectorMode_of_bits(m.Mode())) { TV_Direct => Some(base), TV_Vector => if c.IsInterrupt() == 0b1 - then Some(base + (EXTZ(c.Cause()) << 2)) + then Some(base + (zero_extend(c.Cause()) << 2)) else Some(base), TV_Reserved => None() } @@ -498,11 +498,11 @@ function legalize_xepc(v : xlenbits) -> xlenbits = XXX specification says this legalization should be done on read */ if (sys_enable_writable_misa() & sys_enable_rvc()) | misa.C() == 0b1 then [v with 0 = bitzero] - else v & EXTS(0b100) + else v & sign_extend(0b100) /* masking for reads to xepc */ function pc_alignment_mask() -> xlenbits = - ~(EXTZ(if misa.C() == 0b1 then 0b00 else 0b10)) + ~(zero_extend(if misa.C() == 0b1 then 0b00 else 0b10)) /* auxiliary exception registers */ @@ -612,7 +612,7 @@ function set_sstatus_UXL(s : Sstatus, a : arch_xlen) -> Sstatus = { } function lower_mstatus(m : Mstatus) -> Sstatus = { - let s = Mk_Sstatus(EXTZ(0b0)); + let s = Mk_Sstatus(zero_extend(0b0)); let s = update_SD(s, m.SD()); let s = set_sstatus_UXL(s, get_mstatus_UXL(m)); let s = update_MXR(s, m.MXR()); @@ -663,7 +663,7 @@ bitfield Sedeleg : xlenbits = { register sedeleg : Sedeleg function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = { - Mk_Sedeleg(EXTZ(v[8..0])) + Mk_Sedeleg(zero_extend(v[8..0])) } bitfield Sinterrupts : xlenbits = { @@ -679,7 +679,7 @@ bitfield Sinterrupts : xlenbits = { /* Provides the sip read view of mip (m) as delegated by mideleg (d). */ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { - let s : Sinterrupts = Mk_Sinterrupts(EXTZ(0b0)); + let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); let s = update_SEI(s, m.SEI() & d.SEI()); let s = update_STI(s, m.STI() & d.STI()); let s = update_SSI(s, m.SSI() & d.SSI()); @@ -692,7 +692,7 @@ function lower_mip(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { /* Provides the sie read view of mie (m) as delegated by mideleg (d). */ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { - let s : Sinterrupts = Mk_Sinterrupts(EXTZ(0b0)); + let s : Sinterrupts = Mk_Sinterrupts(zero_extend(0b0)); let s = update_SEI(s, m.SEI() & d.SEI()); let s = update_STI(s, m.STI() & d.STI()); let s = update_SSI(s, m.SSI() & d.SSI()); @@ -825,7 +825,7 @@ function read_seed_csr() -> xlenbits = { let reserved_bits : bits(6) = 0b000000; let custom_bits : bits(8) = 0x00; let seed : bits(16) = get_16_random_bits(); - EXTZ(opst_code(ES16) @ reserved_bits @ custom_bits @ seed) + zero_extend(opst_code(ES16) @ reserved_bits @ custom_bits @ seed) } /* Writes to the seed CSR are ignored */ diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index adf903f28..46134d2d9 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -97,7 +97,7 @@ function curAsid32(satp : bits(32)) -> asid32 = { /* page table base from satp */ function curPTB32(satp : bits(32)) -> paddr32 = { let s : Satp32 = Mk_Satp32(satp); - shiftl(EXTZ(s.PPN()), PAGESIZE_BITS) + shiftl(zero_extend(s.PPN()), PAGESIZE_BITS) } /* Sv32 parameters and bitfield layouts */ @@ -153,7 +153,7 @@ function curAsid64(satp : bits(64)) -> asid64 = { /* page table base from satp */ function curPTB64(satp : bits(64)) -> paddr64 = { let s = Mk_Satp64(satp); - shiftl(EXTZ(s.PPN()), PAGESIZE_BITS) + shiftl(zero_extend(s.PPN()), PAGESIZE_BITS) } /* Sv39 parameters and bitfield layouts */ diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index ecb705ede..10b2067d6 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -133,14 +133,14 @@ function translateAddr_priv(vAddr, ac, effPriv) = { Sbare => TR_Address(vAddr, ext_ptw), Sv39 => { if isValidSv39Addr(vAddr) then match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(EXTZ(pa), ext_ptw), + TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) }, Sv48 => { if isValidSv48Addr(vAddr) then match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV48_LEVELS - 1, ext_ptw) { - TR_Address(pa, ext_ptw) => TR_Address(EXTZ(pa), ext_ptw), + TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw), TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw) } else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index 7531e9d60..e0f5bc985 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -79,7 +79,7 @@ function to_phys_addr(a : paddr32) -> xlenbits = a[31..0] val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE) effect {rmem, rmemt, rreg, escape} function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV32_Vaddr(vaddr); - let pt_ofs : paddr32 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]), PTE32_LOG_SIZE); let pte_addr = ptb + pt_ofs; match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) { @@ -109,7 +109,7 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, ext_pte) then { if level > 0 then { /* walk down the pointer to the next level */ - walk32(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk32: last-level pte contains a ptr"); */ @@ -124,14 +124,14 @@ function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV32_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != EXTZ(0b0) then { + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk32: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); + let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); /* let res = append(ppn, va.PgOfs()); print("walk32: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ @@ -197,7 +197,7 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { match update_PTE_Bits(pteBits, ac, ext_pte) { - None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw), + None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), Some(pbits, ext) => { if not(plat_enable_dirty_update()) then { @@ -211,11 +211,11 @@ function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = n_ent.pte = n_pte.bits(); write_TLB32(idx, n_ent); /* update page table */ - match mem_write_value_priv(to_phys_addr(EXTZ(ent.pteAddr)), 4, n_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits(), Supervisor, false, false, false) { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; - TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw) + TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw) } } } diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index 1c5a2241f..12f1eafcc 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -73,10 +73,10 @@ val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rmemt, rreg, escape} function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV39_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]), PTE39_LOG_SIZE); let pte_addr = ptb + pt_ofs; - match (mem_read_priv(Read(Data), Supervisor, EXTZ(pte_addr), 8, false, false, false)) { + match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { MemException(_) => { /* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) @@ -103,7 +103,7 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, ext_pte) then { if level > 0 then { /* walk down the pointer to the next level */ - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk39: last-level pte contains a ptr"); */ @@ -118,14 +118,14 @@ function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != EXTZ(0b0) then { + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk39: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); + let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); /* let res = append(ppn, va.PgOfs()); print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ @@ -191,7 +191,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) }, PTE_Check_Success(ext_ptw) => { match update_PTE_Bits(pteBits, ac, ext_pte) { - None() => TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw), + None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw), Some(pbits, ext) => { if not(plat_enable_dirty_update()) then { @@ -205,11 +205,11 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = n_ent.pte = n_pte.bits(); write_TLB39(idx, n_ent); /* update page table */ - match mem_write_value_priv(EXTZ(ent.pteAddr), 8, n_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits(), Supervisor, false, false, false) { MemValue(_) => (), MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB") }; - TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw) + TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw) } } } @@ -233,7 +233,7 @@ function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = } else { w_pte : SV39_PTE = update_BITS(pte, pbits.bits()); w_pte : SV39_PTE = update_Ext(w_pte, ext); - match mem_write_value_priv(EXTZ(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 1beea3219..601ed0f17 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -73,10 +73,10 @@ val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE) effect {rmem, rmemt, rreg, escape} function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { let va = Mk_SV48_Vaddr(vaddr); - let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), + let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va.VPNi(), (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]), PTE48_LOG_SIZE); let pte_addr = ptb + pt_ofs; - match (mem_read_priv(Read(Data), Supervisor, EXTZ(pte_addr), 8, false, false, false)) { + match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) { MemException(_) => { /* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level) ^ " pt_base=" ^ BitStr(ptb) @@ -103,7 +103,7 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { if isPTEPtr(pbits, ext_pte) then { if level > 0 then { /* walk down the pointer to the next level */ - walk48(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) + walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw) } else { /* last-level PTE contains a pointer instead of a leaf */ /* print("walk48: last-level pte contains a ptr"); */ @@ -118,14 +118,14 @@ function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = { PTE_Check_Success(ext_ptw) => { if level > 0 then { /* superpage */ /* fixme hack: to get a mask of appropriate size */ - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV48_LEVEL_BITS) - 1; - if (pte.PPNi() & mask) != EXTZ(0b0) then { + let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1; + if (pte.PPNi() & mask) != zero_extend(0b0) then { /* misaligned superpage mapping */ /* print("walk48: misaligned superpage mapping"); */ PTW_Failure(PTW_Misaligned(), ext_ptw) } else { /* add the appropriate bits of the VPN to the superpage PPN */ - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask); + let ppn = pte.PPNi() | (zero_extend(va.VPNi()) & mask); /* let res = append(ppn, va.PgOfs()); print("walk48: using superpage: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */ @@ -197,7 +197,7 @@ function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = } else { w_pte : SV48_PTE = update_BITS(pte, pbits.bits()); w_pte : SV48_PTE = update_Ext(w_pte, ext); - match mem_write_value_priv(EXTZ(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { + match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits(), Supervisor, false, false, false) { MemValue(_) => { add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global); TR_Address(pAddr, ext_ptw) diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index 39d696d11..ae24815f0 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -89,7 +89,7 @@ val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0. function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = { let shift : nat = PAGESIZE_BITS + (level * levelBitSize); /* fixme hack: use a better idiom for masks */ - let vAddrMask : bits('valen) = shiftl(vAddr ^ vAddr ^ EXTZ(0b1), shift) - 1; + let vAddrMask : bits('valen) = shiftl(vAddr ^ vAddr ^ zero_extend(0b1), shift) - 1; let vMatchMask : bits('valen) = ~ (vAddrMask); struct { asid = asid, diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 89989ffd3..5c87465b6 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -264,13 +264,13 @@ register rvfi_mem_data_present : bool val rvfi_zero_exec_packet : unit -> unit effect {wreg} function rvfi_zero_exec_packet () = { - rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(EXTZ(0b0)); - rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(EXTZ(0b0)); - rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(EXTZ(0x0)); + rvfi_inst_data = Mk_RVFI_DII_Execution_Packet_InstMetaData(zero_extend(0b0)); + rvfi_pc_data = Mk_RVFI_DII_Execution_Packet_PC(zero_extend(0b0)); + rvfi_int_data = Mk_RVFI_DII_Execution_Packet_Ext_Integer(zero_extend(0x0)); // magic = "int-data" -> 0x617461642d746e69 (big-endian) rvfi_int_data = update_magic(rvfi_int_data, 0x617461642d746e69); rvfi_int_data_present = false; - rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(EXTZ(0x0)); + rvfi_mem_data = Mk_RVFI_DII_Execution_Packet_Ext_MemAccess(zero_extend(0x0)); // magic = "mem-data" -> 0x617461642d6d656d (big-endian) rvfi_mem_data = update_magic(rvfi_mem_data, 0x617461642d6d656d); rvfi_mem_data_present = false; @@ -285,7 +285,7 @@ function rvfi_halt_exec_packet () = val rvfi_get_v2_support_packet : unit -> bits(704) function rvfi_get_v2_support_packet () = { - let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(EXTZ(0b0)); + let rvfi_exec = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); // Returning 0x3 (using the unused high bits) in halt instead of 0x1 means // that we support the version 2 wire format. This is required to keep // backwards compatibility with old implementations that do not support @@ -296,7 +296,7 @@ function rvfi_get_v2_support_packet () = { val rvfi_get_exec_packet_v1 : unit -> bits(704) effect {rreg} function rvfi_get_exec_packet_v1 () = { - let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(EXTZ(0b0)); + let v1_packet = Mk_RVFI_DII_Execution_Packet_V1(zero_extend(0b0)); // Convert the v2 packet to a v1 packet let v1_packet = update_rvfi_intr(v1_packet, rvfi_inst_data.rvfi_intr()); let v1_packet = update_rvfi_halt(v1_packet, rvfi_inst_data.rvfi_halt()); @@ -335,7 +335,7 @@ val rvfi_get_exec_packet_v2 : unit -> bits(512) effect {rreg} function rvfi_get_exec_packet_v2 () = { // TODO: add the other data // TODO: find a way to return a variable-length bitvector - let packet = Mk_RVFI_DII_Execution_PacketV2(EXTZ(0b0)); + let packet = Mk_RVFI_DII_Execution_PacketV2(zero_extend(0b0)); let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE) let packet = update_basic_data(packet, rvfi_inst_data.bits()); let packet = update_pc_data(packet, rvfi_pc_data.bits());