Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Ssqosid extension #379

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
}
ved-rivos marked this conversation as resolved.
Show resolved Hide resolved

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
}
Loading