diff options
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | model/riscv_csr_begin.sail (renamed from model/riscv_csr_map.sail) | 15 | ||||
| -rw-r--r-- | model/riscv_csr_end.sail (renamed from model/riscv_csr_ext.sail) | 18 | ||||
| -rw-r--r-- | model/riscv_fdext_control.sail | 20 | ||||
| -rw-r--r-- | model/riscv_insts_zicsr.sail | 374 | ||||
| -rw-r--r-- | model/riscv_next_control.sail | 52 | ||||
| -rw-r--r-- | model/riscv_sys_control.sail | 180 | ||||
| -rw-r--r-- | model/riscv_sys_regs.sail | 2 | ||||
| -rwxr-xr-x | model/riscv_vext_control.sail | 32 |
9 files changed, 347 insertions, 355 deletions
@@ -67,18 +67,19 @@ SAIL_DEFAULT_INST += riscv_insts_zicboz.sail SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail -SAIL_SEQ_INST_SRCS = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail -SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail +# TODO: riscv_csr_end.sail here temporarily until the scattered definitions +# are moved from riscv_insts_zicsr.sail to more appropriate places. +SAIL_SEQ_INST_SRCS = riscv_insts_begin.sail $(SAIL_SEQ_INST) riscv_insts_end.sail riscv_csr_end.sail +SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.sail riscv_csr_end.sail # System and platform sources -SAIL_SYS_SRCS = riscv_csr_map.sail +SAIL_SYS_SRCS = riscv_csr_begin.sail # Start of CSR scattered definitions. SAIL_SYS_SRCS += riscv_vext_control.sail # helpers for the 'V' extension SAIL_SYS_SRCS += riscv_next_regs.sail SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdext_control.sail -SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling # SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_begin.sail index 520d7e7..29ff4ee 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_begin.sail @@ -12,6 +12,9 @@ val csr_name_map : csreg <-> string scattered mapping csr_name_map +// TODO: These csr_name_map definitions should be moved to the files +// corresponding to their extensions rather than all be here. + /* user trap setup */ mapping clause csr_name_map = 0x000 <-> "ustatus" mapping clause csr_name_map = 0x004 <-> "uie" @@ -336,13 +339,13 @@ overload to_str = {csr_name} /* returns whether a CSR exists */ -val ext_is_CSR_defined : (csreg) -> bool -scattered function ext_is_CSR_defined +val is_CSR_defined : (csreg) -> bool +scattered function is_CSR_defined /* returns the value of the CSR if it is defined */ -val ext_read_CSR : csreg -> option(xlenbits) -scattered function ext_read_CSR +val read_CSR : csreg -> xlenbits +scattered function read_CSR /* returns new value (after legalisation) if the CSR is defined */ -val ext_write_CSR : (csreg, xlenbits) -> option(xlenbits) -scattered function ext_write_CSR +val write_CSR : (csreg, xlenbits) -> xlenbits +scattered function write_CSR diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_end.sail index f034460..5075e2b 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_end.sail @@ -14,11 +14,17 @@ end csr_name_map previously. */ function csr_name(csr) = csr_name_map(csr) -function clause ext_is_CSR_defined(_) = false -end ext_is_CSR_defined +function clause is_CSR_defined(_) = false +end is_CSR_defined -function clause ext_read_CSR _ = None() -end ext_read_CSR +function clause read_CSR(csr) = { + // This should be impossible because is_CSR_defined() should have returned false. + internal_error(__FILE__, __LINE__, "Read from CSR that does not exist: " ^ bits_str(csr)); +} +end read_CSR -function clause ext_write_CSR (_, _) = None() -end ext_write_CSR +function clause write_CSR(csr, _) = { + // This should be impossible because is_CSR_defined() should have returned false. + internal_error(__FILE__, __LINE__, "Write to CSR that does not exist: " ^ bits_str(csr)); +} +end write_CSR diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 11b8e42..ef4069a 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -24,18 +24,18 @@ function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b0 enum clause extension = Ext_Zfinx function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx() -/* val clause ext_is_CSR_defined : (csreg) -> bool */ +/* val clause is_CSR_defined : (csreg) -> bool */ -function clause ext_is_CSR_defined (0x001) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx) -function clause ext_is_CSR_defined (0x002) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx) -function clause ext_is_CSR_defined (0x003) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx) +function clause is_CSR_defined (0x001) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx) +function clause is_CSR_defined (0x002) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx) +function clause is_CSR_defined (0x003) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx) -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 read_CSR (0x001) = zero_extend(fcsr[FFLAGS]) +function clause read_CSR (0x002) = zero_extend(fcsr[FRM]) +function clause read_CSR (0x003) = zero_extend(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)) } +function clause write_CSR (0x001, value) = { ext_write_fcsr(fcsr[FRM], value[4..0]); zero_extend(fcsr[FFLAGS]) } +function clause write_CSR (0x002, value) = { ext_write_fcsr(value[2..0], fcsr[FFLAGS]); zero_extend(fcsr[FRM]) } +function clause write_CSR (0x003, value) = { ext_write_fcsr(value[7..5], value[4..0]); zero_extend(fcsr.bits) } /* **************************************************************** */ diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index fb28696..c96d31a 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -21,203 +21,180 @@ mapping encdec_csrop : csrop <-> bits(2) = { mapping clause encdec = CSR(csr, rs1, rd, is_imm, op) <-> csr @ rs1 @ bool_bits(is_imm) @ encdec_csrop(op) @ rd @ 0b1110011 -function readCSR csr : csreg -> xlenbits = { - let res : xlenbits = - match (csr, sizeof(xlen)) { - /* machine mode */ - (0xF11, _) => zero_extend(mvendorid), - (0xF12, _) => marchid, - (0xF13, _) => mimpid, - (0xF14, _) => mhartid, - (0xF15, _) => mconfigptr, - (0x300, _) => mstatus.bits, - (0x301, _) => misa.bits, - (0x302, _) => medeleg.bits, - (0x303, _) => mideleg.bits, - (0x304, _) => mie.bits, - (0x305, _) => get_mtvec(), - (0x306, _) => zero_extend(mcounteren.bits), - (0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0], - (0x310, 32) => mstatush.bits, - (0x31A, 32) => menvcfg.bits[63 .. 32], - (0x320, _) => zero_extend(mcountinhibit.bits), - - /* Hardware Performance Monitoring event selection */ - (0b0011001 /* 0x320 */ @ index : bits(5), _) if unsigned(index) >= 3 => read_mhpmevent(hpmidx_from_bits(index)), - - (0x340, _) => mscratch, - (0x341, _) => get_xret_target(Machine) & pc_alignment_mask(), - (0x342, _) => mcause.bits, - (0x343, _) => mtval, - (0x344, _) => mip.bits, - - // pmpcfgN - (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)), - // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. - (0x3B @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b00 @ idx)), - (0x3C @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b01 @ idx)), - (0x3D @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b10 @ idx)), - (0x3E @ idx : bits(4), _) => pmpReadAddrReg(unsigned(0b11 @ idx)), - - /* machine mode counters */ - (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], - (0xB02, _) => minstret[(sizeof(xlen) - 1) .. 0], - (0xB80, 32) => mcycle[63 .. 32], - (0xB82, 32) => minstret[63 .. 32], - - /* Hardware Performance Monitoring machine mode counters */ - (0b1011000 /* 0xB00 */ @ index : bits(5), _) if unsigned(index) >= 3 => read_mhpmcounter(hpmidx_from_bits(index)), - (0b1011100 /* 0xB80 */ @ index : bits(5), 32) if unsigned(index) >= 3 => read_mhpmcounterh(hpmidx_from_bits(index)), - - /* vector */ - (0x008, _) => zero_extend(vstart), - (0x009, _) => zero_extend(vxsat), - (0x00A, _) => zero_extend(vxrm), - (0x00F, _) => zero_extend(vcsr.bits), - (0xC20, _) => vl, - (0xC21, _) => vtype.bits, - (0xC22, _) => vlenb, - - /* trigger/debug */ - (0x7a0, _) => ~(tselect), /* this indicates we don't have any trigger support */ - - /* supervisor mode */ - (0x100, _) => lower_mstatus(mstatus).bits, - (0x102, _) => sedeleg.bits, - (0x103, _) => sideleg.bits, - (0x104, _) => lower_mie(mie, mideleg).bits, - (0x105, _) => get_stvec(), - (0x106, _) => zero_extend(scounteren.bits), - (0x10A, _) => senvcfg.bits[sizeof(xlen) - 1 .. 0], - (0x140, _) => sscratch, - (0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(), - (0x142, _) => scause.bits, - (0x143, _) => stval, - (0x144, _) => lower_mip(mip, mideleg).bits, - (0x180, _) => satp, - - /* user mode counters */ - (0xC00, _) => mcycle[(sizeof(xlen) - 1) .. 0], - (0xC01, _) => mtime[(sizeof(xlen) - 1) .. 0], - (0xC02, _) => minstret[(sizeof(xlen) - 1) .. 0], - (0xC80, 32) => mcycle[63 .. 32], - (0xC81, 32) => mtime[63 .. 32], - (0xC82, 32) => minstret[63 .. 32], - - /* Hardware Performance Monitoring user mode counters */ - (0b1100000 /* 0xC00 */ @ index : bits(5), _) if unsigned(index) >= 3 => read_mhpmcounter(hpmidx_from_bits(index)), - (0b1100100 /* 0xC80 */ @ index : bits(5), 32) if unsigned(index) >= 3 => read_mhpmcounterh(hpmidx_from_bits(index)), - - /* user mode: Zkr */ - (0x015, _) => read_seed_csr(), - - _ => /* check extensions */ - match ext_read_CSR(csr) { - Some(res) => res, - None() => { print_bits("unhandled read to CSR ", csr); - zero_extend(0x0) } - } - }; - if get_config_print_reg() - then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res)); - res +// TODO: These read/write_CSR definitions should be moved to the files +// corresponding to their extensions rather than all be here. + +/* machine mode */ +function clause read_CSR(0xF11) = zero_extend(mvendorid) +function clause read_CSR(0xF12) = marchid +function clause read_CSR(0xF13) = mimpid +function clause read_CSR(0xF14) = mhartid +function clause read_CSR(0xF15) = mconfigptr +function clause read_CSR(0x300) = mstatus.bits +function clause read_CSR(0x301) = misa.bits +function clause read_CSR(0x302) = medeleg.bits +function clause read_CSR(0x303) = mideleg.bits +function clause read_CSR(0x304) = mie.bits +function clause read_CSR(0x305) = get_mtvec() +function clause read_CSR(0x306) = zero_extend(mcounteren.bits) +function clause read_CSR(0x30A) = menvcfg.bits[sizeof(xlen) - 1 .. 0] +function clause read_CSR(0x310 if sizeof(xlen) == 32) = mstatush.bits +function clause read_CSR(0x31A if sizeof(xlen) == 32) = menvcfg.bits[63 .. 32] +function clause read_CSR(0x320) = zero_extend(mcountinhibit.bits) + +/* Hardware Performance Monitoring event selection */ +function clause read_CSR(0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmevent(hpmidx_from_bits(index)) + +function clause read_CSR(0x340) = mscratch +function clause read_CSR(0x341) = get_xret_target(Machine) & pc_alignment_mask() +function clause read_CSR(0x342) = mcause.bits +function clause read_CSR(0x343) = mtval +function clause read_CSR(0x344) = mip.bits + +// pmpcfgN +function clause read_CSR(0x3A @ idx : bits(4) if idx[0] == bitzero | sizeof(xlen) == 32) = pmpReadCfgReg(unsigned(idx)) +// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. +function clause read_CSR(0x3B @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b00 @ idx)) +function clause read_CSR(0x3C @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b01 @ idx)) +function clause read_CSR(0x3D @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b10 @ idx)) +function clause read_CSR(0x3E @ idx : bits(4)) = pmpReadAddrReg(unsigned(0b11 @ idx)) + +/* machine mode counters */ +function clause read_CSR(0xB00) = mcycle[(sizeof(xlen) - 1) .. 0] +function clause read_CSR(0xB02) = minstret[(sizeof(xlen) - 1) .. 0] +function clause read_CSR(0xB80 if sizeof(xlen) == 32)= mcycle[63 .. 32] +function clause read_CSR(0xB82 if sizeof(xlen) == 32) = minstret[63 .. 32] + +/* Hardware Performance Monitoring machine mode counters */ +function clause read_CSR(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index)) +function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if sizeof(xlen) == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) + +/* vector */ +function clause read_CSR(0x008) = zero_extend(vstart) +function clause read_CSR(0x009) = zero_extend(vxsat) +function clause read_CSR(0x00A) = zero_extend(vxrm) +function clause read_CSR(0x00F) = zero_extend(vcsr.bits) +function clause read_CSR(0xC20) = vl +function clause read_CSR(0xC21) = vtype.bits +function clause read_CSR(0xC22) = vlenb + +/* trigger/debug */ +function clause read_CSR(0x7a0) = ~(tselect) /* this indicates we don't have any trigger support */ + +/* supervisor mode */ +function clause read_CSR(0x100) = lower_mstatus(mstatus).bits +function clause read_CSR(0x102) = sedeleg.bits +function clause read_CSR(0x103) = sideleg.bits +function clause read_CSR(0x104) = lower_mie(mie, mideleg).bits +function clause read_CSR(0x105) = get_stvec() +function clause read_CSR(0x106) = zero_extend(scounteren.bits) +function clause read_CSR(0x10A) = senvcfg.bits[sizeof(xlen) - 1 .. 0] +function clause read_CSR(0x140) = sscratch +function clause read_CSR(0x141) = get_xret_target(Supervisor) & pc_alignment_mask() +function clause read_CSR(0x142) = scause.bits +function clause read_CSR(0x143) = stval +function clause read_CSR(0x144) = lower_mip(mip, mideleg).bits +function clause read_CSR(0x180) = satp + +/* user mode counters */ +function clause read_CSR(0xC00) = mcycle[(sizeof(xlen) - 1) .. 0] +function clause read_CSR(0xC01) = mtime[(sizeof(xlen) - 1) .. 0] +function clause read_CSR(0xC02) = minstret[(sizeof(xlen) - 1) .. 0] +function clause read_CSR(0xC80 if sizeof(xlen) == 32) = mcycle[63 .. 32] +function clause read_CSR(0xC81 if sizeof(xlen) == 32) = mtime[63 .. 32] +function clause read_CSR(0xC82 if sizeof(xlen) == 32) = minstret[63 .. 32] + +/* Hardware Performance Monitoring user mode counters */ +function clause read_CSR(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index)) +function clause read_CSR(0b1100100 /* 0xC80 */ @ index : bits(5) if sizeof(xlen) == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index)) + +/* user mode: Zkr */ +function clause read_CSR(0x015) = read_seed_csr() + +/* machine mode */ +function clause write_CSR(0x300, value) = { mstatus = legalize_mstatus(mstatus, value); mstatus.bits } +function clause write_CSR(0x301, value) = { misa = legalize_misa(misa, value); misa.bits } +function clause write_CSR(0x302, value) = { medeleg = legalize_medeleg(medeleg, value); medeleg.bits } +function clause write_CSR(0x303, value) = { mideleg = legalize_mideleg(mideleg, value); mideleg.bits } +function clause write_CSR(0x304, value) = { mie = legalize_mie(mie, value); mie.bits } +function clause write_CSR(0x305, value) = { set_mtvec(value) } +function clause write_CSR(0x306, value) = { mcounteren = legalize_mcounteren(mcounteren, value); zero_extend(mcounteren.bits) } +function clause write_CSR((0x30A, value) if sizeof(xlen) == 32) = { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); menvcfg.bits[31 .. 0] } +function clause write_CSR((0x30A, value) if sizeof(xlen) == 64) = { menvcfg = legalize_menvcfg(menvcfg, value); menvcfg.bits } +function clause write_CSR((0x310, value) if sizeof(xlen) == 32) = { mstatush.bits } // ignore writes for now +function clause write_CSR((0x31A, value) if sizeof(xlen) == 32) = { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); menvcfg.bits[63 .. 32] } +function clause write_CSR(0x320, value) = { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); zero_extend(mcountinhibit.bits) } +function clause write_CSR(0x340, value) = { mscratch = value; mscratch } +function clause write_CSR(0x341, value) = { set_xret_target(Machine, value) } +function clause write_CSR(0x342, value) = { mcause.bits = value; mcause.bits } +function clause write_CSR(0x343, value) = { mtval = value; mtval } +function clause write_CSR(0x344, value) = { mip = legalize_mip(mip, value); mip.bits } + +// pmpcfgN +function clause write_CSR((0x3A @ idx : bits(4), value) if idx[0] == bitzero | sizeof(xlen) == 32) = { + let idx = unsigned(idx); + pmpWriteCfgReg(idx, value); + pmpReadCfgReg(idx) } -function writeCSR (csr : csreg, value : xlenbits) -> unit = { - let res : option(xlenbits) = - match (csr, sizeof(xlen)) { - /* machine mode */ - (0x300, _) => { mstatus = legalize_mstatus(mstatus, value); Some(mstatus.bits) }, - (0x301, _) => { misa = legalize_misa(misa, value); Some(misa.bits) }, - (0x302, _) => { medeleg = legalize_medeleg(medeleg, value); Some(medeleg.bits) }, - (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(zero_extend(mcounteren.bits)) }, - (0x30A, 32) => { menvcfg = legalize_menvcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_menvcfg(menvcfg, value); Some(menvcfg.bits) }, - (0x310, 32) => { Some(mstatush.bits) }, // ignore writes for now - (0x31A, 32) => { menvcfg = legalize_menvcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) }, - (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) }, - (0x343, _) => { mtval = value; Some(mtval) }, - (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) }, - - // pmpcfgN - (0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => { - let idx = unsigned(idx); - pmpWriteCfgReg(idx, value); Some(pmpReadCfgReg(idx)) - }, - - // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. - (0x3B @ idx : bits(4), _) => { let idx = unsigned(0b00 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, - (0x3C @ idx : bits(4), _) => { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, - (0x3D @ idx : bits(4), _) => { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, - (0x3E @ idx : bits(4), _) => { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); Some(pmpReadAddrReg(idx)) }, - - /* machine mode counters */ - (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, - (0xB02, _) => { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; Some(value) }, - (0xB80, 32) => { mcycle[63 .. 32] = value; Some(value) }, - (0xB82, 32) => { minstret[63 .. 32] = value; minstret_increment = false; Some(value) }, - - /* Hardware Performance Monitoring machine mode counters */ - (0b0011001 /* 0x320 */ @ index : bits(5), _) if unsigned(index) >= 3 => { - let index = hpmidx_from_bits(index); - write_mhpmevent(index, value); - Some(read_mhpmevent(index)) - }, - (0b1011000 /* 0xB00 */ @ index : bits(5), _) if unsigned(index) >= 3 => { - let index = hpmidx_from_bits(index); - write_mhpmcounter(index, value); - Some(read_mhpmcounter(index)) - }, - (0b1011100 /* 0xB80 */ @ index : bits(5), 32) if unsigned(index) >= 3 => { - let index = hpmidx_from_bits(index); - write_mhpmcounterh(index, value); - Some(read_mhpmcounterh(index)) - }, - - /* trigger/debug */ - (0x7a0, _) => { tselect = value; Some(tselect) }, - - /* supervisor mode */ - (0x100, _) => { mstatus = legalize_sstatus(mstatus, value); Some(mstatus.bits) }, - (0x102, _) => { sedeleg = legalize_sedeleg(sedeleg, value); Some(sedeleg.bits) }, - (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(zero_extend(scounteren.bits)) }, - (0x10A, _) => { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) }, - (0x140, _) => { sscratch = value; Some(sscratch) }, - (0x141, _) => { Some(set_xret_target(Supervisor, value)) }, - (0x142, _) => { scause.bits = value; Some(scause.bits) }, - (0x143, _) => { stval = value; Some(stval) }, - (0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) }, - (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, - - /* user mode: seed (entropy source). writes are ignored */ - (0x015, _) => write_seed_csr(), - - /* vector */ - (0x008, _) => { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); Some(zero_extend(vstart)) }, - (0x009, _) => { vxsat = value[0 .. 0]; Some(zero_extend(vxsat)) }, - (0x00A, _) => { vxrm = value[1 .. 0]; Some(zero_extend(vxrm)) }, - (0x00F, _) => { vcsr.bits = value[2 ..0]; Some(zero_extend(vcsr.bits)) }, - (0xC20, _) => { vl = value; Some(vl) }, - (0xC21, _) => { vtype.bits = value; Some(vtype.bits) }, - (0xC22, _) => { vlenb = value; Some(vlenb) }, - - _ => ext_write_CSR(csr, value) - }; - match res { - Some(v) => if get_config_print_reg() - then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ BitStr(v) ^ " (input: " ^ BitStr(value) ^ ")"), - None() => print_bits("unhandled write to CSR ", csr) - } +// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. +function clause write_CSR(0x3B @ idx : bits(4), value) = { let idx = unsigned(0b00 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) } +function clause write_CSR(0x3C @ idx : bits(4), value) = { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) } +function clause write_CSR(0x3D @ idx : bits(4), value) = { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) } +function clause write_CSR(0x3E @ idx : bits(4), value) = { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) } + +/* machine mode counters */ +function clause write_CSR(0xB00, value) = { mcycle[(sizeof(xlen) - 1) .. 0] = value; value } +function clause write_CSR(0xB02, value) = { minstret[(sizeof(xlen) - 1) .. 0] = value; minstret_increment = false; value } +function clause write_CSR((0xB80, value) if sizeof(xlen) == 32) = { mcycle[63 .. 32] = value; value } +function clause write_CSR((0xB82, value) if sizeof(xlen) == 32) = { minstret[63 .. 32] = value; minstret_increment = false; value } + +/* Hardware Performance Monitoring machine mode counters */ +function clause write_CSR((0b0011001 /* 0x320 */ @ index : bits(5), value) if unsigned(index) >= 3) = { + let index = hpmidx_from_bits(index); + write_mhpmevent(index, value); + read_mhpmevent(index) } +function clause write_CSR((0b1011000 /* 0xB00 */ @ index : bits(5), value) if unsigned(index) >= 3) = { + let index = hpmidx_from_bits(index); + write_mhpmcounter(index, value); + read_mhpmcounter(index) +} +function clause write_CSR((0b1011100 /* 0xB80 */ @ index : bits(5), value) if sizeof(xlen) == 32 & unsigned(index) >= 3) = { + let index = hpmidx_from_bits(index); + write_mhpmcounterh(index, value); + read_mhpmcounterh(index) +} + +/* trigger/debug */ +function clause write_CSR(0x7a0, value) = { tselect = value; tselect } + +/* supervisor mode */ +function clause write_CSR(0x100, value) = { mstatus = legalize_sstatus(mstatus, value); mstatus.bits } +function clause write_CSR(0x102, value) = { sedeleg = legalize_sedeleg(sedeleg, value); sedeleg.bits } +function clause write_CSR(0x103, value) = { sideleg.bits = value; sideleg.bits } /* TODO: does this need legalization? */ +function clause write_CSR(0x104, value) = { mie = legalize_sie(mie, mideleg, value); mie.bits } +function clause write_CSR(0x105, value) = { set_stvec(value) } +function clause write_CSR(0x106, value) = { scounteren = legalize_scounteren(scounteren, value); zero_extend(scounteren.bits) } +function clause write_CSR(0x10A, value) = { senvcfg = legalize_senvcfg(senvcfg, zero_extend(value)); senvcfg.bits[sizeof(xlen) - 1 .. 0] } +function clause write_CSR(0x140, value) = { sscratch = value; sscratch } +function clause write_CSR(0x141, value) = { set_xret_target(Supervisor, value) } +function clause write_CSR(0x142, value) = { scause.bits = value; scause.bits } +function clause write_CSR(0x143, value) = { stval = value; stval } +function clause write_CSR(0x144, value) = { mip = legalize_sip(mip, mideleg, value); mip.bits } +function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_Architecture(), satp, value); satp } + +/* user mode: seed (entropy source). writes are ignored */ +function clause write_CSR(0x015, value) = write_seed_csr() + +/* vector */ +function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) } +function clause write_CSR(0x009, value) = { vxsat = value[0 .. 0]; zero_extend(vxsat) } +function clause write_CSR(0x00A, value) = { vxrm = value[1 .. 0]; zero_extend(vxrm) } +function clause write_CSR(0x00F, value) = { vcsr.bits = value[2 ..0]; zero_extend(vcsr.bits) } +function clause write_CSR(0xC20, value) = { vl = value; vl } +function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits } +function clause write_CSR(0xC22, value) = { vlenb = value; vlenb } function clause execute CSR(csr, rs1, rd, is_imm, op) = { let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1); @@ -230,14 +207,19 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) = { else if not(ext_check_CSR(csr, cur_privilege, isWrite)) then { ext_check_CSR_fail(); RETIRE_FAIL } else { - let csr_val = readCSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ + let csr_val = read_CSR(csr); /* could have side-effects, so technically shouldn't perform for CSRW[I] with rd == 0 */ if isWrite then { let new_val : xlenbits = match op { CSRRW => rs1_val, CSRRS => csr_val | rs1_val, CSRRC => csr_val & ~(rs1_val) }; - writeCSR(csr, new_val) + let final_val = write_CSR(csr, new_val); + if get_config_print_reg() + then print_reg("CSR " ^ to_str(csr) ^ " <- " ^ bits_str(final_val) ^ " (input: " ^ bits_str(new_val) ^ ")") + } else { + if get_config_print_reg() + then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ bits_str(csr_val)); }; X(rd) = csr_val; RETIRE_SUCCESS diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 2f83a0a..aa10bad 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -8,33 +8,33 @@ /* Functional specification for the 'N' user-level interrupts standard extension. */ -function clause ext_is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus -function clause ext_is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie -function clause ext_is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec -function clause ext_is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch -function clause ext_is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc -function clause ext_is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause -function clause ext_is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval -function clause ext_is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip +function clause is_CSR_defined(0x000) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ustatus +function clause is_CSR_defined(0x004) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uie +function clause is_CSR_defined(0x005) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utvec +function clause is_CSR_defined(0x040) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uscratch +function clause is_CSR_defined(0x041) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uepc +function clause is_CSR_defined(0x042) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // ucause +function clause is_CSR_defined(0x043) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // utval +function clause is_CSR_defined(0x044) = extensionEnabled(Ext_U) & extensionEnabled(Ext_N) // uip -function clause ext_read_CSR(0x000) = Some(lower_sstatus(lower_mstatus(mstatus)).bits) -function clause ext_read_CSR(0x004) = Some(lower_sie(lower_mie(mie, mideleg), sideleg).bits) -function clause ext_read_CSR(0x005) = Some(get_utvec()) -function clause ext_read_CSR(0x040) = Some(uscratch) -function clause ext_read_CSR(0x041) = Some(get_xret_target(User) & pc_alignment_mask()) -function clause ext_read_CSR(0x042) = Some(ucause.bits) -function clause ext_read_CSR(0x043) = Some(utval) -function clause ext_read_CSR(0x044) = Some(lower_sip(lower_mip(mip, mideleg), sideleg).bits) +function clause read_CSR(0x000) = lower_sstatus(lower_mstatus(mstatus)).bits +function clause read_CSR(0x004) = lower_sie(lower_mie(mie, mideleg), sideleg).bits +function clause read_CSR(0x005) = get_utvec() +function clause read_CSR(0x040) = uscratch +function clause read_CSR(0x041) = get_xret_target(User) & pc_alignment_mask() +function clause read_CSR(0x042) = ucause.bits +function clause read_CSR(0x043) = utval +function clause read_CSR(0x044) = lower_sip(lower_mip(mip, mideleg), sideleg).bits -function clause ext_write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); Some(mstatus.bits) } -function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value); +function clause write_CSR(0x000, value) = { mstatus = legalize_ustatus(mstatus, value); mstatus.bits } +function clause write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie(mie, mideleg), sideleg, value); mie = lift_sie(mie, mideleg, sie); - Some(mie.bits) } -function clause ext_write_CSR(0x005, value) = { Some(set_utvec(value)) } -function clause ext_write_CSR(0x040, value) = { uscratch = value; Some(uscratch) } -function clause ext_write_CSR(0x041, value) = { Some(set_xret_target(User, value)) } -function clause ext_write_CSR(0x042, value) = { ucause.bits = value; Some(ucause.bits) } -function clause ext_write_CSR(0x043, value) = { utval = value; Some(utval) } -function clause ext_write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value); + mie.bits } +function clause write_CSR(0x005, value) = { set_utvec(value) } +function clause write_CSR(0x040, value) = { uscratch = value; uscratch } +function clause write_CSR(0x041, value) = { set_xret_target(User, value) } +function clause write_CSR(0x042, value) = { ucause.bits = value; ucause.bits } +function clause write_CSR(0x043, value) = { utval = value; utval } +function clause write_CSR(0x044, value) = { let sip = legalize_uip(lower_mip(mip, mideleg), sideleg, value); mip = lift_sip(mip, mideleg, sip); - Some(mip.bits) } + mip.bits } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 406525f..8a8c9da 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -16,96 +16,96 @@ function clause extensionEnabled(Ext_Zkr) = true function csrAccess(csr : csreg) -> csrRW = csr[11..10] function csrPriv(csr : csreg) -> priv_level = csr[9..8] -function is_CSR_defined (csr : csreg) -> bool = - match (csr) { - /* machine mode: informational */ - 0xf11 => true, // mvendorid - 0xf12 => true, // marchdid - 0xf13 => true, // mimpid - 0xf14 => true, // mhartid - 0xf15 => true, // mconfigptr - /* machine mode: trap setup */ - 0x300 => true, // mstatus - 0x301 => true, // misa - 0x302 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // medeleg - 0x303 => extensionEnabled(Ext_S) | extensionEnabled(Ext_N), // mideleg - 0x304 => true, // mie - 0x305 => true, // mtvec - 0x306 => extensionEnabled(Ext_U), // mcounteren - 0x30A => extensionEnabled(Ext_U), // menvcfg - 0x310 => sizeof(xlen) == 32, // mstatush - 0x31A => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // menvcfgh - 0x320 => true, // mcountinhibit - /* machine mode: trap handling */ - 0x340 => true, // mscratch - 0x341 => true, // mepc - 0x342 => true, // mcause - 0x343 => true, // mtval - 0x344 => true, // mip - - // pmpcfgN - 0x3A @ idx : bits(4) => sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32), - - // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. - 0x3B @ idx : bits(4) => sys_pmp_count() > unsigned(0b00 @ idx), - 0x3C @ idx : bits(4) => sys_pmp_count() > unsigned(0b01 @ idx), - 0x3D @ idx : bits(4) => sys_pmp_count() > unsigned(0b10 @ idx), - 0x3E @ idx : bits(4) => sys_pmp_count() > unsigned(0b11 @ idx), - - /* counters */ - 0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm), // mhpmevent3..31 - - 0xB00 => true, // mcycle - 0xB02 => true, // minstret - - 0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm), // mhpmcounter3..31 - - 0xB80 => sizeof(xlen) == 32, // mcycleh - 0xB82 => sizeof(xlen) == 32, // minstreth - - 0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm) & (sizeof(xlen) == 32), // mhpmcounterh3..31 - - /* disabled trigger/debug module */ - 0x7a0 => true, - - /* supervisor mode: trap setup */ - 0x100 => extensionEnabled(Ext_S), // sstatus - 0x102 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sedeleg - 0x103 => extensionEnabled(Ext_S) & extensionEnabled(Ext_N), // sideleg - 0x104 => extensionEnabled(Ext_S), // sie - 0x105 => extensionEnabled(Ext_S), // stvec - 0x106 => extensionEnabled(Ext_S), // scounteren - 0x10A => extensionEnabled(Ext_S), // senvcfg - - /* supervisor mode: trap handling */ - 0x140 => extensionEnabled(Ext_S), // sscratch - 0x141 => extensionEnabled(Ext_S), // sepc - 0x142 => extensionEnabled(Ext_S), // scause - 0x143 => extensionEnabled(Ext_S), // stval - 0x144 => extensionEnabled(Ext_S), // sip - - /* supervisor mode: address translation */ - 0x180 => extensionEnabled(Ext_S), // satp - - /* user mode: counters */ - 0xC00 => extensionEnabled(Ext_U), // cycle - 0xC01 => extensionEnabled(Ext_U), // time - 0xC02 => extensionEnabled(Ext_U), // instret - - 0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U), // hpmcounter3..31 - - 0xC80 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // cycleh - 0xC81 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // timeh - 0xC82 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // instreth - - 0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3 => extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // hpmcounterh3..31 - - /* user mode: Zkr */ - 0x015 => extensionEnabled(Ext_Zkr), - - /* check extensions */ - _ => ext_is_CSR_defined(csr) - } +// TODO: These is_CSR_defined definitions should be moved to the files +// corresponding to their extensions rather than all be here. + +/* machine mode: informational */ +function clause is_CSR_defined(0xf11) = true // mvendorid +function clause is_CSR_defined(0xf12) = true // marchdid +function clause is_CSR_defined(0xf13) = true // mimpid +function clause is_CSR_defined(0xf14) = true // mhartid +function clause is_CSR_defined(0xf15) = true // mconfigptr +/* machine mode: trap setup */ +function clause is_CSR_defined(0x300) = true // mstatus +function clause is_CSR_defined(0x301) = true // misa +function clause is_CSR_defined(0x302) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // medeleg +function clause is_CSR_defined(0x303) = extensionEnabled(Ext_S) | extensionEnabled(Ext_N) // mideleg +function clause is_CSR_defined(0x304) = true // mie +function clause is_CSR_defined(0x305) = true // mtvec +function clause is_CSR_defined(0x306) = extensionEnabled(Ext_U) // mcounteren +function clause is_CSR_defined(0x30A) = extensionEnabled(Ext_U) // menvcfg +function clause is_CSR_defined(0x310) = sizeof(xlen) == 32 // mstatush +function clause is_CSR_defined(0x31A) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // menvcfgh +function clause is_CSR_defined(0x320) = true // mcountinhibit + + +/* machine mode: trap handling */ +function clause is_CSR_defined(0x340) = true // mscratch +function clause is_CSR_defined(0x341) = true // mepc +function clause is_CSR_defined(0x342) = true // mcause +function clause is_CSR_defined(0x343) = true // mtval +function clause is_CSR_defined(0x344) = true // mip + +// pmpcfgN +function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | sizeof(xlen) == 32) + +// pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. +function clause is_CSR_defined(0x3B) @ idx : bits(4) = sys_pmp_count() > unsigned(0b00 @ idx) +function clause is_CSR_defined(0x3C) @ idx : bits(4) = sys_pmp_count() > unsigned(0b01 @ idx) +function clause is_CSR_defined(0x3D) @ idx : bits(4) = sys_pmp_count() > unsigned(0b10 @ idx) +function clause is_CSR_defined(0x3E) @ idx : bits(4) = sys_pmp_count() > unsigned(0b11 @ idx) + +/* counters */ +function clause is_CSR_defined(0b0011001 /* 0x320 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmevent3..31 + +function clause is_CSR_defined(0xB00) = true // mcycle +function clause is_CSR_defined(0xB02) = true // minstret + +function clause is_CSR_defined(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) // mhpmcounter3..31 + +function clause is_CSR_defined(0xB80) = sizeof(xlen) == 32 // mcycleh +function clause is_CSR_defined(0xB82) = sizeof(xlen) == 32 // minstreth + +function clause is_CSR_defined(0b1011100 /* 0xB80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & (sizeof(xlen) == 32) // mhpmcounterh3..31 + +/* disabled trigger/debug module */ +function clause is_CSR_defined(0x7a0) = true + +/* supervisor mode: trap setup */ +function clause is_CSR_defined(0x100) = extensionEnabled(Ext_S) // sstatus +function clause is_CSR_defined(0x102) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sedeleg +function clause is_CSR_defined(0x103) = extensionEnabled(Ext_S) & extensionEnabled(Ext_N) // sideleg +function clause is_CSR_defined(0x104) = extensionEnabled(Ext_S) // sie +function clause is_CSR_defined(0x105) = extensionEnabled(Ext_S) // stvec +function clause is_CSR_defined(0x106) = extensionEnabled(Ext_S) // scounteren +function clause is_CSR_defined(0x10A) = extensionEnabled(Ext_S) // senvcfg + +/* supervisor mode: trap handling */ +function clause is_CSR_defined(0x140) = extensionEnabled(Ext_S) // sscratch +function clause is_CSR_defined(0x141) = extensionEnabled(Ext_S) // sepc +function clause is_CSR_defined(0x142) = extensionEnabled(Ext_S) // scause +function clause is_CSR_defined(0x143) = extensionEnabled(Ext_S) // stval +function clause is_CSR_defined(0x144) = extensionEnabled(Ext_S) // sip + +/* supervisor mode: address translation */ +function clause is_CSR_defined(0x180) = extensionEnabled(Ext_S) // satp + +/* user mode: counters */ +function clause is_CSR_defined(0xC00) = extensionEnabled(Ext_U) // cycle +function clause is_CSR_defined(0xC01) = extensionEnabled(Ext_U) // time +function clause is_CSR_defined(0xC02) = extensionEnabled(Ext_U) // instret + +function clause is_CSR_defined(0b1100000 /* 0xC00 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) // hpmcounter3..31 + +function clause is_CSR_defined(0xC80) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // cycleh +function clause is_CSR_defined(0xC81) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // timeh +function clause is_CSR_defined(0xC82) = extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // instreth + +function clause is_CSR_defined(0b1100100 /* 0xC80 */ @ index : bits(5) if unsigned(index) >= 3) = extensionEnabled(Ext_Zihpm) & extensionEnabled(Ext_U) & (sizeof(xlen) == 32) // hpmcounterh3..31 + +/* user mode: Zkr */ +function clause is_CSR_defined(0x015) = extensionEnabled(Ext_Zkr) + val check_CSR_access : (csrRW, priv_level, Privilege, bool) -> bool function check_CSR_access(csrrw, csrpr, p, isWrite) = diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 2291f2b..65336f2 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -793,7 +793,7 @@ function read_seed_csr() -> xlenbits = { } /* Writes to the seed CSR are ignored */ -function write_seed_csr () -> option(xlenbits) = None() +function write_seed_csr () -> xlenbits = zeros() bitfield MEnvcfg : bits(64) = { // Supervisor TimeCmp Extension diff --git a/model/riscv_vext_control.sail b/model/riscv_vext_control.sail index 3344d7c..38d0e0c 100755 --- a/model/riscv_vext_control.sail +++ b/model/riscv_vext_control.sail @@ -6,23 +6,23 @@ /* SPDX-License-Identifier: BSD-2-Clause */ /*=======================================================================================*/ -function clause ext_is_CSR_defined (0x008) = true -function clause ext_is_CSR_defined (0xC20) = true -function clause ext_is_CSR_defined (0xC21) = true -function clause ext_is_CSR_defined (0xC22) = true +function clause is_CSR_defined (0x008) = true +function clause is_CSR_defined (0xC20) = true +function clause is_CSR_defined (0xC21) = true +function clause is_CSR_defined (0xC22) = true -function clause ext_is_CSR_defined (0x009) = true -function clause ext_is_CSR_defined (0x00A) = true -function clause ext_is_CSR_defined (0x00F) = true +function clause is_CSR_defined (0x009) = true +function clause is_CSR_defined (0x00A) = true +function clause is_CSR_defined (0x00F) = true -function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) -function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm])) -function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits)) +function clause read_CSR (0x009) = zero_extend(vcsr[vxsat]) +function clause read_CSR (0x00A) = zero_extend(vcsr[vxrm]) +function clause read_CSR (0x00F) = zero_extend(vcsr.bits) -function clause ext_read_CSR (0x009) = Some (zero_extend(vcsr[vxsat])) -function clause ext_read_CSR (0x00A) = Some (zero_extend(vcsr[vxrm])) -function clause ext_read_CSR (0x00F) = Some (zero_extend(vcsr.bits)) +function clause read_CSR (0x009) = zero_extend(vcsr[vxsat]) +function clause read_CSR (0x00A) = zero_extend(vcsr[vxrm]) +function clause read_CSR (0x00F) = zero_extend(vcsr.bits) -function clause ext_write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); Some(zero_extend(vcsr[vxsat])) } -function clause ext_write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); Some(zero_extend(vcsr[vxrm])) } -function clause ext_write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); Some(zero_extend(vcsr.bits)) } +function clause write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) } +function clause write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); zero_extend(vcsr[vxrm]) } +function clause write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) } |