diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index dcc865117..e6e86cb4a 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -111,6 +111,11 @@ mapping clause csr_name_map = 0x141 <-> "sepc" mapping clause csr_name_map = 0x142 <-> "scause" mapping clause csr_name_map = 0x143 <-> "stval" mapping clause csr_name_map = 0x144 <-> "sip" +/* supervisor environment configuration */ +mapping clause csr_name_map = 0x10A <-> "senvcfg" +/* Sstc - Supervisor Timer Register */ +mapping clause csr_name_map = 0x14D <-> "stimecmp" +mapping clause csr_name_map = 0x15D <-> "stimecmph" /* supervisor protection and translation */ mapping clause csr_name_map = 0x180 <-> "satp" /* machine information registers */ @@ -133,6 +138,9 @@ mapping clause csr_name_map = 0x341 <-> "mepc" mapping clause csr_name_map = 0x342 <-> "mcause" mapping clause csr_name_map = 0x343 <-> "mtval" mapping clause csr_name_map = 0x344 <-> "mip" +/* machine environment configuration */ +mapping clause csr_name_map = 0x30A <-> "menvcfg" +mapping clause csr_name_map = 0x31A <-> "menvcfgh" /* machine protection and translation */ mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0" mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1" diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 6aa512ea2..03bbd1b09 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -148,6 +148,8 @@ function readCSR csr : csreg -> xlenbits = { (0x142, _) => scause.bits, (0x143, _) => stval, (0x144, _) => lower_mip(mip, mideleg).bits, + (0x14D, _) => stimecmp[sizeof(xlen) - 1 .. 0], + (0x15D, 32) => stimecmp[63 .. 32], (0x180, _) => satp, /* user mode counters */ @@ -184,10 +186,10 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (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_envcfg(menvcfg, menvcfg.bits[63 .. 32] @ value); Some(menvcfg.bits[31 .. 0]) }, - (0x30A, 64) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.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_envcfg(menvcfg, value @ menvcfg.bits[31 .. 0]); Some(menvcfg.bits[63 .. 32]) }, + (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)) }, @@ -223,12 +225,14 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (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_envcfg(senvcfg, zero_extend(value)); Some(senvcfg.bits[sizeof(xlen) - 1 .. 0]) }, + (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) }, + (0x14D, _) => { stimecmp[(sizeof(xlen) - 1) .. 0] = value; Some(stimecmp[sizeof(xlen) - 1 ..0]) }, + (0x15D, 32) => { stimecmp[63 ..32] = value; Some(stimecmp[63 .. 32]) }, (0x180, _) => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) }, /* user mode: seed (entropy source). writes are ignored */ diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 15b0d4c46..6b16512ff 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -273,7 +273,16 @@ function clint_dispatch() -> unit = { if mtimecmp <=_u mtime then { if get_config_print_platform() then print_platform(" clint timer pending at mtime " ^ BitStr(mtime)); - mip[MTI] = 0b1 + mip[MTI] = 0b1; + }; + /* Sstc - supervisor Timer Register */ + if haveSstc() & menvcfg[STCE] == 0b1 then { + mip[STI] = 0b0; + if stimecmp <=_u mtime then { + if get_config_print_platform() + then print_platform(" supervisor timer pending at mtime " ^ BitStr(mtime)); + mip[STI] = 0b1; + } } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 4dfe36539..96c40e90e 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -134,6 +134,9 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x142 => haveSupMode() & (p == Machine | p == Supervisor), // scause 0x143 => haveSupMode() & (p == Machine | p == Supervisor), // stval 0x144 => haveSupMode() & (p == Machine | p == Supervisor), // sip + /* Sstc : Supervisor Timer Register */ + 0x14D => haveSupMode() & haveSstc() & (p == Machine | (p == Supervisor & (menvcfg.STCE() == 0b1))), // stimecmp + 0x15D => haveSupMode() & haveSstc() & (p == Machine | (p == Supervisor & (menvcfg.STCE() == 0b1))), // stimecmph /* supervisor mode: address translation */ 0x180 => haveSupMode() & (p == Machine | p == Supervisor), // satp @@ -167,7 +170,9 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool = (0xC00, Supervisor) => mcounteren[CY] == 0b1, (0xC01, Supervisor) => mcounteren[TM] == 0b1, (0xC02, Supervisor) => mcounteren[IR] == 0b1, - + /* Sstc extension */ + (0x14D, Supervisor) => mcounteren[TM] == 0b1, + (0x15D, Supervisor) => mcounteren[TM] == 0b1, (0xC00, User) => mcounteren[CY] == 0b1 & (not(haveSupMode()) | scounteren[CY] == 0b1), (0xC01, User) => mcounteren[TM] == 0b1 & (not(haveSupMode()) | scounteren[TM] == 0b1), (0xC02, User) => mcounteren[IR] == 0b1 & (not(haveSupMode()) | scounteren[IR] == 0b1), diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index c98584bc0..603b0005d 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -140,6 +140,30 @@ bitfield Misa : xlenbits = { } register misa : Misa +// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two +// upper fields so for simplicity we can use the same type. +bitfield Envcfg : bits(64) = { + // Supervisor TimeCmp Extension + STCE : 63, + // Page Based Memory Types Extension + PBMTE : 62, + // Reserved WPRI bits. + wpri_1 : 61 .. 8, + // Cache Block Zero instruction Enable + CBZE : 7, + // Cache Block Clean and Flush instruction Enable + CBCFE : 6, + // Cache Block Invalidate instruction Enable + CBIE : 5 .. 4, + // Reserved WPRI bits. + wpri_0 : 3 .. 1, + // Fence of I/O implies Memory + FIOM : 0, +} + +register menvcfg : Envcfg +register senvcfg : Envcfg + /* whether misa is R/W */ val sys_enable_writable_misa = {c: "sys_enable_writable_misa", ocaml: "Platform.enable_writable_misa", _: "sys_enable_writable_misa"} : unit -> bool /* whether misa.c was enabled at boot */ @@ -222,6 +246,9 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Sstc extension support */ +function haveSstc() -> bool = true + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -399,7 +426,13 @@ function legalize_mip(o : Minterrupts, v : xlenbits) -> Minterrupts = { /* The only writable bits are the S-mode bits, and with the 'N' * extension, the U-mode bits. */ let v = Mk_Minterrupts(v); - let m = [o with SEI = v[SEI], STI = v[STI], SSI = v[SSI]]; + + let m = [o with SEI = v[SEI], SSI = v[SSI]]; + + let m = if ( not(haveSstc()) | (haveSstc() & (menvcfg[STCE] == 0b0)) ) then { + [m with STI = v[STI]]; + } else m; + if haveUsrMode() & haveNExt() then { [m with UEI = v[UEI], UTI = v[UTI], USI = v[USI]] } else m @@ -702,7 +735,13 @@ function lower_mie(m : Minterrupts, d : Minterrupts) -> Sinterrupts = { /* Returns the new value of mip from the previous mip (o) and the written sip (s) as delegated by mideleg (d). */ function lift_sip(o : Minterrupts, d : Minterrupts, s : Sinterrupts) -> Minterrupts = { let m : Minterrupts = o; + let m = if d[SSI] == 0b1 then [m with SSI = s[SSI]] else m; + + let m = if d[STI] == 0b1 & (not(haveSstc()) | (haveSstc() & menvcfg[STCE] == 0b0)) then { + [m with STI = s[STI]] + } else m; + if haveNExt() then { let m = if d[UEI] == 0b1 then [m with UEI = s[UEI]] else m; let m = if d[USI] == 0b1 then [m with USI = s[USI]] else m; @@ -828,37 +867,20 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() -// menvcfg is 64 bits. senvcfg is SXLEN bits and does not have the two -// upper fields so for simplicity we can use the same type. -bitfield Envcfg : bits(64) = { - // Supervisor TimeCmp Extension - STCE : 63, - // Page Based Memory Types Extension - PBMTE : 62, - // Reserved WPRI bits. - wpri_1 : 61 .. 8, - // Cache Block Zero instruction Enable - CBZE : 7, - // Cache Block Clean and Flush instruction Enable - CBCFE : 6, - // Cache Block Invalidate instruction Enable - CBIE : 5 .. 4, - // Reserved WPRI bits. - wpri_0 : 3 .. 1, - // Fence of I/O implies Memory - FIOM : 0, -} - -register menvcfg : Envcfg -register senvcfg : Envcfg - -function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { +function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { let v = Mk_Envcfg(v); let o = [o with FIOM = if sys_enable_writable_fiom() then v[FIOM] else 0b0]; // Other extensions are not implemented yet so all other fields are read only zero. o } +function legalize_menvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { + let v = Mk_Envcfg(v); + let o = update_FIOM(o, if sys_enable_writable_fiom() then v.FIOM() else 0b0); + let o = update_STCE(o, if haveSstc() then v.STCE() else 0b0); + // Other extensions are not implemented yet so all other fields are read only zero. + o +} // Return whether or not FIOM is currently active, based on the current // privilege and the menvcfg/senvcfg settings. This means that I/O fences // imply memory fence. @@ -950,4 +972,8 @@ val get_vtype_vma : unit -> agtype function get_vtype_vma() = decode_agtype(vtype[vma]) val get_vtype_vta : unit -> agtype + function get_vtype_vta() = decode_agtype(vtype[vta]) + +/* Sstc : Supervisor Timer Register */ +register stimecmp : bits(64)