diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index f034460d6..5075e2b2f 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.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_csr_map.sail b/model/riscv_csr_map.sail index 6478919ca..889022feb 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -190,13 +190,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_fdext_control.sail b/model/riscv_fdext_control.sail index 11b8e425e..ef4069aa2 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 f2980fb9e..b190d6602 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -21,175 +21,160 @@ 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), - - (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], - - /* 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], - - /* 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 +/* 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) + +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] + +/* 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] + +/* user mode: Zkr */ +function clause read_CSR(0x015) = read_seed_csr() + + // if get_config_print_reg() + // then print_reg("CSR " ^ to_str(csr) ^ " -> " ^ BitStr(res)); + // res + + +/* 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, value @ idx : bits(4)) 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) }, - - /* 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 } + +/* 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 } + + // 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) + // } function clause execute CSR(csr, rs1, rd, is_imm, op) = { let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1); @@ -202,14 +187,14 @@ 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 _ = write_CSR(csr, new_val); }; X(rd) = csr_val; RETIRE_SUCCESS diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 2f83a0abc..aa10bad98 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 6e8832738..58899bbac 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -16,84 +16,79 @@ 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), - 0xB00 => true, // mcycle - 0xB02 => true, // minstret - - 0xB80 => sizeof(xlen) == 32, // mcycleh - 0xB82 => sizeof(xlen) == 32, // minstreth - - /* 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 - - 0xC80 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // cycleh - 0xC81 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // timeh - 0xC82 => extensionEnabled(Ext_U) & (sizeof(xlen) == 32), // instreth - - /* user mode: Zkr */ - 0x015 => extensionEnabled(Ext_Zkr), - - /* check extensions */ - _ => ext_is_CSR_defined(csr) - } +/* 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) +function clause is_CSR_defined(0xB00) = true // mcycle +function clause is_CSR_defined(0xB02) = true // minstret + +function clause is_CSR_defined(0xB80) = sizeof(xlen) == 32 // mcycleh +function clause is_CSR_defined(0xB82) = sizeof(xlen) == 32 // minstreth + +/* 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(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 + +/* 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 1f34d2d3a..6530f1f03 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -752,7 +752,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 3344d7c5a..38d0e0caa 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) }