From 58cac61d9ddde591902c933a9dfa5d8ba3fca6da Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 29 Jun 2023 13:30:11 +0100 Subject: [PATCH 1/5] Rename EXTZ and EXTS Rename EXTZ to zero_extend and EXTS to sign_extend. Two main reasons for doing this - it means that the source more closely follows the descriptions in the documentation with more readable names, and EXTS and EXTZ are visually very close to each other with just the S and Z. They are also following an odd convention where they are ALLCAPS rather than snake_case like other functions in the spec. I think this convention comes from early Power specs in Sail, which influenced Sail MIPS and CHERI-MIPS, but I don't think it's a very good convention we should be keeping in sail-riscv --- model/prelude.sail | 12 ++++----- model/riscv_analysis.sail | 12 ++++----- model/riscv_fdext_control.sail | 12 ++++----- model/riscv_fdext_regs.sail | 6 ++--- model/riscv_fetch_rvfi.sail | 8 +++--- model/riscv_freg_type.sail | 2 +- model/riscv_insts_aext.sail | 20 +++++++-------- model/riscv_insts_base.sail | 32 +++++++++++------------ model/riscv_insts_cdext.sail | 8 +++--- model/riscv_insts_cext.sail | 40 ++++++++++++++--------------- model/riscv_insts_cfext.sail | 8 +++--- model/riscv_insts_dext.sail | 18 ++++++------- model/riscv_insts_fext.sail | 22 ++++++++-------- model/riscv_insts_mext.sail | 6 ++--- model/riscv_insts_zba.sail | 4 +-- model/riscv_insts_zbb.sail | 10 ++++---- model/riscv_insts_zbkb.sail | 4 +-- model/riscv_insts_zbs.sail | 12 ++++----- model/riscv_insts_zfa.sail | 18 ++++++------- model/riscv_insts_zfh.sail | 18 ++++++------- model/riscv_insts_zicsr.sail | 18 ++++++------- model/riscv_insts_zkn.sail | 28 ++++++++++----------- model/riscv_insts_zks.sail | 8 +++--- model/riscv_jalr_rmem.sail | 2 +- model/riscv_jalr_seq.sail | 2 +- model/riscv_mem.sail | 4 +-- model/riscv_next_regs.sail | 6 ++--- model/riscv_platform.sail | 22 ++++++++-------- model/riscv_pmp_regs.sail | 2 +- model/riscv_reg_type.sail | 2 +- model/riscv_regs.sail | 2 +- model/riscv_step.sail | 4 +-- model/riscv_step_rvfi.sail | 2 +- model/riscv_sys_control.sail | 46 +++++++++++++++++----------------- model/riscv_sys_regs.sail | 18 ++++++------- model/riscv_vmem_common.sail | 4 +-- model/riscv_vmem_rv64.sail | 4 +-- model/riscv_vmem_sv32.sail | 16 ++++++------ model/riscv_vmem_sv39.sail | 20 +++++++-------- model/riscv_vmem_sv48.sail | 14 +++++------ model/riscv_vmem_tlb.sail | 2 +- model/rvfi_dii.sail | 14 +++++------ 42 files changed, 256 insertions(+), 256 deletions(-) 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()); From 5725f3fe08a2c1b8588b9a4416d91c297e1e5c00 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 26 May 2023 07:17:39 -0700 Subject: [PATCH 2/5] csim: Allow redirecting trace output to a file using command line flag This is useful when booting an operating system with tracing enabled as it allows showing the printed messages on the terminal and storing the trace log to a separate file. All categorized trace messages are now redirected to the --trace-output file when passed. If this option is not gived, the current behaviour of using stdout is retained. Example usage: `./c_emulator/riscv_sim_RV64 -b os-boot/rv64-64mb.dtb --trace-output /dev/stderr os-boot/linux-rv64-64mb.bbl --trace-output /tmp/linux.log` --- c_emulator/riscv_platform_impl.h | 2 + c_emulator/riscv_prelude.c | 9 ++-- c_emulator/riscv_sim.c | 70 ++++++++++++++++++++------------ 3 files changed, 52 insertions(+), 29 deletions(-) diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index d24ecc8fb..aa8d391de 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -2,6 +2,7 @@ #include #include +#include /* Settings of the platform implementation. */ @@ -32,5 +33,6 @@ extern uint64_t rv_clint_size; extern uint64_t rv_htif_tohost; extern uint64_t rv_insns_per_tick; +extern FILE *trace_log; extern int term_fd; void plat_term_write_impl(char c); diff --git a/c_emulator/riscv_prelude.c b/c_emulator/riscv_prelude.c index cd2ab70cd..143a1521b 100644 --- a/c_emulator/riscv_prelude.c +++ b/c_emulator/riscv_prelude.c @@ -1,5 +1,6 @@ #include "riscv_prelude.h" #include "riscv_config.h" +#include "riscv_platform_impl.h" unit print_string(sail_string prefix, sail_string msg) { @@ -10,28 +11,28 @@ unit print_string(sail_string prefix, sail_string msg) unit print_instr(sail_string s) { if (config_print_instr) - printf("%s\n", s); + fprintf(trace_log, "%s\n", s); return UNIT; } unit print_reg(sail_string s) { if (config_print_reg) - printf("%s\n", s); + fprintf(trace_log, "%s\n", s); return UNIT; } unit print_mem_access(sail_string s) { if (config_print_mem_access) - printf("%s\n", s); + fprintf(trace_log, "%s\n", s); return UNIT; } unit print_platform(sail_string s) { if (config_print_platform) - printf("%s\n", s); + fprintf(trace_log, "%s\n", s); return UNIT; } diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index fdb9ce01d..5a73896ba 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -48,10 +48,14 @@ const char *RV32ISA = "RV32IMAC"; #define CSR_MTVAL 0x343 #define CSR_MIP 0x344 +#define OPT_TRACE_OUTPUT 1000 + static bool do_dump_dts = false; static bool do_show_times = false; struct tv_spike_t *s = NULL; char *term_log = NULL; +static const char *trace_log_path = NULL; +FILE *trace_log = NULL; char *dtb_file = NULL; unsigned char *dtb = NULL; size_t dtb_len = 0; @@ -111,33 +115,34 @@ char *sailcov_file = NULL; #endif static struct option options[] = { - {"enable-dirty-update", no_argument, 0, 'd'}, - {"enable-misaligned", no_argument, 0, 'm'}, - {"enable-pmp", no_argument, 0, 'P'}, - {"enable-next", no_argument, 0, 'N'}, - {"ram-size", required_argument, 0, 'z'}, - {"disable-compressed", no_argument, 0, 'C'}, - {"disable-writable-misa", no_argument, 0, 'I'}, - {"disable-fdext", no_argument, 0, 'F'}, - {"mtval-has-illegal-inst-bits", no_argument, 0, 'i'}, - {"device-tree-blob", required_argument, 0, 'b'}, - {"terminal-log", required_argument, 0, 't'}, - {"show-times", required_argument, 0, 'p'}, - {"report-arch", no_argument, 0, 'a'}, - {"test-signature", required_argument, 0, 'T'}, - {"signature-granularity", required_argument, 0, 'g'}, + {"enable-dirty-update", no_argument, 0, 'd' }, + {"enable-misaligned", no_argument, 0, 'm' }, + {"enable-pmp", no_argument, 0, 'P' }, + {"enable-next", no_argument, 0, 'N' }, + {"ram-size", required_argument, 0, 'z' }, + {"disable-compressed", no_argument, 0, 'C' }, + {"disable-writable-misa", no_argument, 0, 'I' }, + {"disable-fdext", no_argument, 0, 'F' }, + {"mtval-has-illegal-inst-bits", no_argument, 0, 'i' }, + {"device-tree-blob", required_argument, 0, 'b' }, + {"terminal-log", required_argument, 0, 't' }, + {"show-times", required_argument, 0, 'p' }, + {"report-arch", no_argument, 0, 'a' }, + {"test-signature", required_argument, 0, 'T' }, + {"signature-granularity", required_argument, 0, 'g' }, #ifdef RVFI_DII - {"rvfi-dii", required_argument, 0, 'r'}, + {"rvfi-dii", required_argument, 0, 'r' }, #endif - {"help", no_argument, 0, 'h'}, - {"trace", optional_argument, 0, 'v'}, - {"no-trace", optional_argument, 0, 'V'}, - {"inst-limit", required_argument, 0, 'l'}, - {"enable-zfinx", no_argument, 0, 'x'}, + {"help", no_argument, 0, 'h' }, + {"trace", optional_argument, 0, 'v' }, + {"no-trace", optional_argument, 0, 'V' }, + {"trace-output", required_argument, 0, OPT_TRACE_OUTPUT}, + {"inst-limit", required_argument, 0, 'l' }, + {"enable-zfinx", no_argument, 0, 'x' }, #ifdef SAILCOV - {"sailcov-file", required_argument, 0, 'c'}, + {"sailcov-file", required_argument, 0, 'c' }, #endif - {0, 0, 0, 0 } + {0, 0, 0, 0 } }; static void print_usage(const char *argv0, int ec) @@ -352,6 +357,10 @@ char *process_args(int argc, char **argv) sailcov_file = strdup(optarg); break; #endif + case OPT_TRACE_OUTPUT: + trace_log_path = optarg; + fprintf(stderr, "using %s for trace output.\n", trace_log_path); + break; case '?': print_usage(argv[0], 1); break; @@ -626,6 +635,9 @@ void close_logs(void) exit(EXIT_FAILURE); } #endif + if (trace_log != stdout) { + fclose(trace_log); + } } void finish(int ec) @@ -726,8 +738,8 @@ void flush_logs(void) if (config_print_instr) { fprintf(stderr, "\n"); fflush(stderr); - fprintf(stdout, "\n"); - fflush(stdout); + fprintf(trace_log, "\n"); + fflush(trace_log); } } @@ -1010,6 +1022,14 @@ void init_logs() exit(1); } + if (trace_log_path == NULL) { + trace_log = stdout; + } else if ((trace_log = fopen(trace_log_path, "w+")) < 0) { + fprintf(stderr, "Cannot create trace log '%s': %s\n", trace_log, + strerror(errno)); + exit(1); + } + #ifdef SAILCOV if (sailcov_file != NULL) { sail_set_coverage_file(sailcov_file); From 34a32a2d7f0fb5aa826573e42052342a59d6f2fa Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 28 Apr 2023 12:28:06 -0700 Subject: [PATCH 3/5] Fix --help output for options without a short flag MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Previously --help printed the following: ``` -V --no-trace -� --trace-output -l --inst-limit ``` With the new change it is: ``` -V --no-trace --trace-output -l --inst-limit ``` --- c_emulator/riscv_sim.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 5a73896ba..84ee04d3f 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -1,3 +1,4 @@ +#include #include #include #include @@ -156,7 +157,10 @@ static void print_usage(const char *argv0, int ec) #endif struct option *opt = options; while (opt->name) { - fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name); + if (isprint(opt->val)) + fprintf(stdout, "\t -%c\t --%s\n", (char)opt->val, opt->name); + else + fprintf(stdout, "\t \t --%s\n", opt->name); opt++; } exit(ec); From ec6a6a9601b2efe3890c1f23c7753ad9129ec868 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Thu, 3 Aug 2023 09:18:35 -0700 Subject: [PATCH 4/5] Avoid unnecessary empty lines when instruction tracing is on These empty lines don't add to the readability of the trace and in fact when trace redirection is enabled they result in lots of empty lines being printed to stderr which makes it impossible to read the OS boot messages. --- c_emulator/riscv_sim.c | 2 -- 1 file changed, 2 deletions(-) diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 84ee04d3f..93609b433 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -740,9 +740,7 @@ int compare_states(struct tv_spike_t *s) void flush_logs(void) { if (config_print_instr) { - fprintf(stderr, "\n"); fflush(stderr); - fprintf(trace_log, "\n"); fflush(trace_log); } } From 861bd6f65593013381c905d7a54e538e5382bf31 Mon Sep 17 00:00:00 2001 From: ahadali5000 Date: Mon, 3 Jul 2023 11:14:23 +0500 Subject: [PATCH 5/5] If C cannot be disabled, all changes to misa must be suppressed --- model/riscv_sys_regs.sail | 27 ++++++++++++--------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index fedb02e9e..251df5a65 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -156,22 +156,19 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: " unsetting C. If it returns true the write will have no effect. */ val ext_veto_disable_C : unit -> bool effect {rreg} -/* We currently only support dynamic changes for the C extension. */ function legalize_misa(m : Misa, v : xlenbits) -> Misa = { - if sys_enable_writable_misa () - then { /* Handle modifications to C. */ - let v = Mk_Misa(v); - /* Suppress changing C if nextPC would become misaligned or an extension vetoes or C was disabled at boot (i.e. not supported). */ - let m = - if (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) | not(sys_enable_rvc()) - then m - else update_C(m, v.C()); - /* Handle updates for F/D. */ - if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) - then m - else update_D(update_F(m, v.F()), v.D()) - } - else m + let v = Mk_Misa(v); + /* Suppress updates to MISA if MISA is not writable or if by disabling C next PC would become misaligned or an extension vetoes */ + if not(sys_enable_writable_misa()) | (v.C() == 0b0 & (nextPC[1] == bitone | ext_veto_disable_C())) + then m + else { + /* Suppress enabling C if C was disabled at boot (i.e. not supported) */ + let m = if not(sys_enable_rvc()) then m else update_C(m, v.C()); + /* Handle updates for F/D. */ + if not(sys_enable_fdext()) | (v.D() == 0b1 & v.F() == 0b0) + then m + else update_D(update_F(m, v.F()), v.D()) + } } /* helpers to check support for various extensions. */