Skip to content

Commit

Permalink
Add unratified Smclic, Ssclic, Smclicshv extensions
Browse files Browse the repository at this point in the history
  • Loading branch information
dansmathers authored Mar 1, 2024
1 parent 0224391 commit 0edd11e
Show file tree
Hide file tree
Showing 12 changed files with 1,090 additions and 63 deletions.
528 changes: 528 additions & 0 deletions model/riscv_clic_control.sail

Large diffs are not rendered by default.

21 changes: 21 additions & 0 deletions model/riscv_clic_mem.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

val vector_table_fetch : xlenbits -> VectorTableFetchResult
function vector_table_fetch(table_addr) -> VectorTableFetchResult =
if sizeof(xlen) == 32 then {
match mem_read(Execute(), table_addr, 4, false, false, false) {
MemException(e) => F_TableError(e, table_addr),
MemValue(table_entry) => F_TableEntry(table_entry)
}
} else { /* xlen == 64 */
match mem_read(Execute(), table_addr, 8, false, false, false) {
MemException(e) => F_TableError(e, table_addr),
MemValue(table_entry) => F_TableEntry(table_entry)
}
}
95 changes: 95 additions & 0 deletions model/riscv_clic_regs.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

/* Architectural state for the 'Smclic' fast interrupts extension. */

/* Smclic csrs */
mapping clause csr_name_map = 0x307 <-> "mtvt"
mapping clause csr_name_map = 0x345 <-> "mnxti"
mapping clause csr_name_map = 0xFB1 <-> "mintstatus"
mapping clause csr_name_map = 0x347 <-> "mintthresh"
mapping clause csr_name_map = 0x348 <-> "mscratchcsw"
mapping clause csr_name_map = 0x349 <-> "mscratchcswl"
/* Ssclic csrs */
mapping clause csr_name_map = 0x107 <-> "stvt"
mapping clause csr_name_map = 0x145 <-> "snxti"
mapping clause csr_name_map = 0xDB1 <-> "sintstatus"
mapping clause csr_name_map = 0x147 <-> "sintthresh"
mapping clause csr_name_map = 0x148 <-> "sscratchcsw"
mapping clause csr_name_map = 0x149 <-> "sscratchcswl"
/* Suclic csrs */
mapping clause csr_name_map = 0x107 <-> "utvt"
mapping clause csr_name_map = 0x145 <-> "unxti"
mapping clause csr_name_map = 0xDB1 <-> "uintstatus"
mapping clause csr_name_map = 0x147 <-> "uintthresh"
mapping clause csr_name_map = 0x148 <-> "sscratchcsw"
mapping clause csr_name_map = 0x149 <-> "sscratchcswl"

register inhv : bits(1) /* internal state of accessing vector table, exception handler will decide which xinhv to set */

register mtvt : xlenbits
register mintthresh : ilbits
register mil : ilbits
register mpil : ilbits
register minhv : bits(1)

register stvt : xlenbits
register sintthresh : ilbits
register sil : ilbits
register spil : ilbits
register sinhv : bits(1)

register utvt : xlenbits
register uintthresh : ilbits
register uil : ilbits
register upil : ilbits
register uinhv : bits(1)

register clicintip_raw : vector(4096, dec, bits(1))
register clicintip_raw_prev : vector(4096, dec, bits(1))
register clicintip : vector(4096, dec, bits(1))
register clicintie : vector(4096, dec, bits(1))
register clicintctl : vector(4096, dec, ilbits)
register clicintattr : vector(4096, dec, clicintattr_layout)

bitfield ClicMcause : xlenbits = {
IsInterrupt : xlen - 1,
Minhv : 30,
ClicMcauseMpp : 29 .. 28,
ClicMcauseMpie: 27,
Mpil : 23 .. 16,
Exccode : 11 .. 0
}
register clicmcause : ClicMcause
register clicmstatus : Mstatus

bitfield ClicScause : xlenbits = {
IsInterrupt : xlen - 1,
Sinhv : 30,
ClicScauseSpp : 28,
ClicScauseSpie: 27,
Spil : 23 .. 16,
Exccode : 11 .. 0
}
register clicscause : ClicScause

bitfield ClicUcause : xlenbits = {
IsInterrupt : xlen - 1,
Uinhv : 30,
ClicUcauseUpie: 27,
Upil : 23 .. 16,
Exccode : 11 .. 0
}
register clicucause : ClicUcause

bitfield Mintstatus : xlenbits = {
mil : 31 .. 24,
sil : 15 .. 8,
uil : 7 .. 0
}
register mintstatus : Mintstatus
36 changes: 36 additions & 0 deletions model/riscv_clic_type.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
/*=======================================================================================*/
/* This Sail RISC-V architecture model, comprising all files and */
/* directories except where otherwise noted is subject the BSD */
/* two-clause license in the LICENSE file. */
/* */
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

/* Definitions for fast interrupt (Smclic extensions) */

/* default register type */
type ilbits = bits(8)

bitfield clicintattr_layout : bits(8) = {
MODE : 7 .. 6, /* privilege mode */
TRIG : 2 .. 1, /* 11 - negedge triggered */
/* 10 - active low */
/* 01 - posedge triggered */
/* 00 - active high */
SHV : 0 /* hardware vectored interrupt */
}

val is_shv : bitvector(1) -> bool
function is_shv (shv) =
match (shv) {
0b0 => false,
0b1 => true
}

let CLIC_MTI = 7
let CLIC_MSI = 3

union VectorTableFetchResult = {
F_TableEntry : xlenbits, /* Entry in vector table */
F_TableError : (ExceptionType, xlenbits) /* standard exception and table entry addr */
}
97 changes: 74 additions & 23 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ function readCSR csr : csreg -> xlenbits = {
(0x301, _) => misa.bits,
(0x302, _) => medeleg.bits,
(0x303, _) => mideleg.bits,
(0x304, _) => mie.bits,
(0x304, _) => if haveSmclic() then { zero_extend(0b0) } else mie.bits,
(0x305, _) => get_mtvec(),
(0x306, _) => zero_extend(mcounteren.bits),
(0x30A, _) => menvcfg.bits[sizeof(xlen) - 1 .. 0],
Expand All @@ -43,9 +43,17 @@ function readCSR csr : csreg -> xlenbits = {

(0x340, _) => mscratch,
(0x341, _) => get_xret_target(Machine) & pc_alignment_mask(),
(0x342, _) => mcause.bits,
(0x342, _) => if haveSmclic() then {
clicmcause.bits = mcause.bits;
clicmcause[Minhv] = minhv;
clicmcause[ClicMcauseMpp] = mstatus[MPP];
clicmcause[ClicMcauseMpie] = mstatus[MPIE];
clicmcause[Mpil] = mpil;
clicmcause.bits
} else
mcause.bits,
(0x343, _) => mtval,
(0x344, _) => mip.bits,
(0x344, _) => if haveSmclic() then { zero_extend(0b0) } else mip.bits,

// pmpcfgN
(0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => pmpReadCfgReg(unsigned(idx)),
Expand Down Expand Up @@ -77,15 +85,23 @@ function readCSR csr : csreg -> xlenbits = {
(0x100, _) => lower_mstatus(mstatus).bits,
(0x102, _) => sedeleg.bits,
(0x103, _) => sideleg.bits,
(0x104, _) => lower_mie(mie, mideleg).bits,
(0x104, _) => if haveSmclic() then { zero_extend(0b0) } else 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,
(0x142, _) => if haveSmclic() then {
clicscause.bits = scause.bits;
clicscause[Sinhv] = sinhv;
clicscause[ClicScauseSpp] = mstatus[SPP];
clicscause[ClicScauseSpie] = mstatus[SPIE];
clicscause[Spil] = mpil;
clicscause.bits
} else
scause.bits,
(0x143, _) => stval,
(0x144, _) => lower_mip(mip, mideleg).bits,
(0x144, _) => if haveSmclic() then { zero_extend(0b0) } else lower_mip(mip, mideleg).bits,
(0x180, _) => satp,

/* user mode counters */
Expand Down Expand Up @@ -119,7 +135,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(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) },
(0x304, _) => { if haveSmclic() then { mie = mie; Some(mie.bits) } else { 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]) },
Expand All @@ -129,9 +145,19 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(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) },
(0x342, _) => { if haveSmclic() then {
clicmcause.bits = value;
minhv = clicmcause[Minhv];
mstatus[MPP] = clicmcause[ClicMcauseMpp];
mstatus[MPIE] = clicmcause[ClicMcauseMpie];
mpil = clicmcause[Mpil];
Some(clicmcause.bits)
} else {
mcause.bits = value; Some(mcause.bits)
}
},
(0x343, _) => { mtval = value; Some(mtval) },
(0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits) },
(0x344, _) => { if haveSmclic() then { mip = mip; Some(mip.bits) } else { mip = legalize_mip(mip, value); Some(mip.bits) } },

// pmpcfgN
(0x3A @ idx : bits(4), _) if idx[0] == bitzero | sizeof(xlen) == 32 => {
Expand All @@ -158,15 +184,25 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
(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) },
(0x104, _) => { if haveSmclic() then { mie = mie; Some(mie.bits) } else { 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]) },
(0x140, _) => { sscratch = value; Some(sscratch) },
(0x141, _) => { Some(set_xret_target(Supervisor, value)) },
(0x142, _) => { scause.bits = value; Some(scause.bits) },
(0x142, _) => { if haveSmclic() then {
clicscause.bits = value;
sinhv = clicscause[Sinhv];
mstatus[SPP] = clicscause[ClicScauseSpp];
mstatus[SPIE] = clicscause[ClicScauseSpie];
spil = clicscause[Spil];
Some(clicscause.bits)
} else {
scause.bits = value; Some(scause.bits)
}
},
(0x143, _) => { stval = value; Some(stval) },
(0x144, _) => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits) },
(0x144, _) => { if haveSmclic() then { mip = mip; Some(mip.bits) } else { 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 */
Expand Down Expand Up @@ -201,17 +237,32 @@ 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 */
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)
};
X(rd) = csr_val;
RETIRE_SUCCESS
let cond_writeCSR : bool = isWrite & (op == CSRRW) & is_imm == false;
match (csr, sizeof(xlen)) {
/* special conditional write CSRs, CSRRS/C/I/read behavior reserved */
(0x348, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}},
(0x349, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}},
(0x148, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}},
(0x149, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}},
(0x049, _) => {if cond_writeCSR then {match ext_write_CSR(csr, rs1_val) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};}else{ext_check_CSR_fail(); RETIRE_FAIL}},
/* special Smclic nxti CSRs */
(0x345, _) => {match access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, Machine) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};},
(0x145, _) => {match access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, Supervisor) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};},
(0x045, _) => {match access_nxti_CSR(csr, rs1_val, rd, is_imm, op, isWrite, User) {Some(res) => {X(rd) = res; RETIRE_SUCCESS},None()=>RETIRE_FAIL};},
_ => { /* standard CSRs */
let csr_val = readCSR(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)
};
X(rd) = csr_val;
RETIRE_SUCCESS
}
}
}
}

Expand Down
26 changes: 22 additions & 4 deletions model/riscv_next_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,21 @@ function clause ext_is_CSR_defined(0x043, _) = haveUsrMode() & haveNExt() // utv
function clause ext_is_CSR_defined(0x044, _) = haveUsrMode() & haveNExt() // 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(0x004) = if haveSmclic() then { Some(zero_extend(0b0)) } else 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(0x042) = if haveSmclic() then {
clicucause.bits = ucause.bits;
clicucause[Uinhv] = uinhv;
clicucause[ClicUcauseUpie] = mstatus[UPIE];
clicucause[Upil] = upil;
Some(clicucause.bits)
} else
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 ext_read_CSR(0x044) = if haveSmclic() then { Some(zero_extend(0b0)) } else Some(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);
Expand All @@ -33,7 +41,17 @@ function clause ext_write_CSR(0x004, value) = { let sie = legalize_uie(lower_mie
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(0x042, value) = { if haveSmclic() then {
clicucause.bits = value;
uinhv = clicucause[Uinhv];
mstatus[UPIE] = clicucause[ClicUcauseUpie];
upil = clicucause[Upil];
Some(clicucause.bits)
} else {
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);
mip = lift_sip(mip, mideleg, sip);
Expand Down
Loading

0 comments on commit 0edd11e

Please sign in to comment.