diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 22cffd5a6..08ec8f521 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -49,6 +49,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" /* supervisor envcfg */ @@ -76,6 +81,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 f2980fb9e..2ea067d84 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -87,6 +87,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 */ @@ -168,6 +170,8 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (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 19e3d30ae..0ac5b4cdf 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -211,7 +211,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 95ed4d6a5..51918d4ca 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -73,6 +73,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 @@ -106,7 +109,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 65d141923..1a5654507 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -78,6 +78,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 */ @@ -168,6 +192,9 @@ function haveZalrsc() -> bool = haveAtomics() /* Zicond extension support */ function haveZicond() -> bool = true +/* Sstc extension support */ +function haveSstc() -> bool = true + /* * Illegal values legalized to least privileged mode supported. * Note: the only valid combinations of supported modes are M, M+U, M+S+U. @@ -369,7 +396,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()) | 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 @@ -673,7 +706,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()) | 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; @@ -799,6 +838,7 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() +<<<<<<< HEAD bitfield MEnvcfg : bits(64) = { // Supervisor TimeCmp Extension STCE : 63, @@ -843,11 +883,22 @@ function legalize_menvcfg(o : MEnvcfg, v : bits(64)) -> MEnvcfg = { function legalize_senvcfg(o : SEnvcfg, v : xlenbits) -> SEnvcfg = { let v = Mk_SEnvcfg(v); +======= +function legalize_senvcfg(o : Envcfg, v : bits(64)) -> Envcfg = { + let v = Mk_Envcfg(v); +>>>>>>> 1d0f240 (add Sstc extension) 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. @@ -941,4 +992,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)