Skip to content

Commit

Permalink
add srmcfg CSR introduced by Ssqosid
Browse files Browse the repository at this point in the history
  • Loading branch information
ved-rivos committed Jul 18, 2024
1 parent db5f430 commit 6fe932e
Show file tree
Hide file tree
Showing 4 changed files with 71 additions and 1 deletion.
5 changes: 5 additions & 0 deletions model/riscv_csr_map.sail
Original file line number Diff line number Diff line change
Expand Up @@ -176,6 +176,11 @@ mapping clause csr_name_map = 0x00F <-> "vcsr"
mapping clause csr_name_map = 0xC20 <-> "vl"
mapping clause csr_name_map = 0xC21 <-> "vtype"
mapping clause csr_name_map = 0xC22 <-> "vlenb"
/* Sqosid csrs */
mapping clause csr_name_map = 0x181 <-> "srmcfg"
/* Smstateen csrs */
mapping clause csr_name_map = 0x30C <-> "mstateen0"
mapping clause csr_name_map = 0x31C <-> "mstateen0h"

val csr_name : csreg -> string
overload to_str = {csr_name}
Expand Down
7 changes: 7 additions & 0 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,10 @@ function readCSR csr : csreg -> xlenbits = {
(0x305, _) => get_mtvec(),
(0x306, _) => zero_extend(mcounteren.bits),
(0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0],
(0x30C, _) => mstateen0.bits[sizeof(xlen) - 1 .. 0],
(0x310, 32) => mstatush.bits,
(0x31A, 32) => menvcfg.bits[63 .. 32],
(0x31C, 32) => mstateen0.bits[63 .. 32],
(0x320, _) => zero_extend(mcountinhibit.bits),

(0x340, _) => mscratch,
Expand Down Expand Up @@ -88,6 +90,7 @@ function readCSR csr : csreg -> xlenbits = {
(0x143, _) => stval,
(0x144, _) => lower_mip(mip, mideleg).bits,
(0x180, _) => satp,
(0x181, _) => srmcfg.bits(),

/* user mode counters */
(0xC00, _) => mcycle[(sizeof(xlen) - 1) .. 0],
Expand Down Expand Up @@ -125,8 +128,11 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(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) },
(0x30C, 32) => { mstateen0 = legalize_mstateen0(mstateen0, mstateen0.bits()[63 .. 32] @ value); Some(mstateen0.bits()[31 .. 0]) },
(0x30C, 64) => { mstateen0 = legalize_mstateen0(mstateen0, value); Some(mstateen0.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]) },
(0x31C, 32) => { mstateen0 = legalize_mstateen0(mstateen0, value @ mstateen0.bits()[31 .. 0]); Some(mstateen0.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)) },
Expand Down Expand Up @@ -169,6 +175,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(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) },
(0x181, _) => { srmcfg = legalize_srmcfg(srmcfg, value); Some(srmcfg.bits()) },

/* user mode: seed (entropy source). writes are ignored */
(0x015, _) => write_seed_csr(),
Expand Down
16 changes: 15 additions & 1 deletion model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,10 @@ function is_CSR_defined (csr : csreg) -> bool =
0x305 => true, // mtvec
0x306 => haveUsrMode(), // mcounteren
0x30A => haveUsrMode(), // menvcfg
0x30C => haveSupMode() & haveSmstateen(), // mstateen0
0x310 => sizeof(xlen) == 32, // mstatush
0x31A => haveUsrMode() & (sizeof(xlen) == 32), // menvcfgh
0x31C => haveSupMode() & (sizeof(xlen) == 32) & haveSmstateen(), // mstateen0h
0x320 => true, // mcountinhibit
/* machine mode: trap handling */
0x340 => true, // mscratch
Expand Down Expand Up @@ -77,6 +79,9 @@ function is_CSR_defined (csr : csreg) -> bool =
/* supervisor mode: address translation */
0x180 => haveSupMode(), // satp

/* supervisor mode: resource management configurations */
0x181 => haveSsqosid(), // srmcfg

/* user mode: counters */
0xC00 => haveUsrMode(), // cycle
0xC01 => haveUsrMode(), // time
Expand Down Expand Up @@ -117,7 +122,6 @@ function check_Counteren(csr : csreg, p : Privilege) -> bool =
else true
}


/* Seed may only be accessed if we are doing a write, and access has been
* allowed in the current priv mode
*/
Expand All @@ -136,12 +140,18 @@ function check_seed_CSR (csr : csreg, p : Privilege, isWrite : bool) -> bool = {
}
}

function check_srmcfg(csr : csreg, p : Privilege) -> bool =
csr == 0x181
& p == Supervisor
& ((haveSmstateen() & mstateen0.PRIV_V1P14() == 0b1) | not(haveSmstateen()))

function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
is_CSR_defined(csr)
& check_CSR_access(csrAccess(csr), csrPriv(csr), p, isWrite)
& check_TVM_SATP(csr, p)
& check_Counteren(csr, p)
& check_seed_CSR(csr, p, isWrite)
& check_srmcfg(csr, p)

/* Reservation handling for LR/SC.
*
Expand Down Expand Up @@ -525,6 +535,8 @@ function init_sys() -> unit = {

menvcfg.bits = zero_extend(0b0);
senvcfg.bits = zero_extend(0b0);
mstateen0.bits = zero_extend(0b0);

/* initialize vector csrs */
elen = 0b1; /* ELEN=64 as the common case */
vlen = 0b0100; /* VLEN=512 as a default value */
Expand All @@ -548,6 +560,8 @@ function init_sys() -> unit = {
// PMP's L and A fields are set to 0 on reset.
init_pmp();

srmcfg->RCID() = 0b000000000000;

// log compatibility with spike
if get_config_print_reg()
then print_reg("CSR mstatus <- " ^ BitStr(mstatus.bits) ^ " (input: " ^ BitStr(zero_extend(0b0) : xlenbits) ^ ")")
Expand Down
44 changes: 44 additions & 0 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,12 @@ function haveZicond() -> bool = true
/* Zabha extension support */
function haveZabha() -> bool = true

/* Smstateen extension support */
function haveSmstateen() -> bool = true

/* Ssqosid extension support */
function haveSsqosid() -> 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.
Expand Down Expand Up @@ -865,6 +871,30 @@ function is_fiom_active() -> bool = {
User => (menvcfg[FIOM] | senvcfg[FIOM]) == 0b1,
}
}

bitfield Mstateen0 : bits(64) = {
// PRIV_V1P14 control access to various state added concurrent
// with Priv Specification version 1.14. The following is the
// list of state currently defined to be controlled by this bit:
// - CSR srmcfg introduced by Ssqosid extension
PRIV_V1P14 : 55
}

register mstateen0 : Mstateen0

// If any extension controlled by PRIV_V1P14 bit in mstateen0 are
// present then the PRIV_V1P14 bit in mstateen0 is present
function have_PRIV_V1P14_Extensions() -> bool = {
haveSsqosid()
}

function legalize_mstateen0(o : Mstateen0, v : bits(64)) -> Mstateen0 = {
let v = Mk_Mstateen0(v);
let o = [o with PRIV_V1P14 = if have_PRIV_V1P14_Extensions() then v[PRIV_V1P14] else 0b0];
// Other extensions are not implemented yet so all other fields are read only zero.
o
}

/* vector csrs */
register vstart : bits(16) /* use the largest possible length of vstart */
register vxsat : bits(1)
Expand Down Expand Up @@ -948,4 +978,18 @@ 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])

/* srmcfg CSR introduced by Ssqosid */
bitfield Srmcfg : xlenbits = {
MCID : 27 .. 16,
RCID : 11 .. 0
}

register srmcfg : Srmcfg

function legalize_srmcfg(s : Srmcfg, v : xlenbits) -> Srmcfg = {
let s = [s with MCID = v[27 .. 16], RCID = v[11 .. 0]];
s
}

0 comments on commit 6fe932e

Please sign in to comment.