Skip to content

Commit

Permalink
add support for cmo extension
Browse files Browse the repository at this point in the history
  • Loading branch information
liweiwei committed Jan 27, 2022
1 parent 4da2ab1 commit 54f4dc9
Show file tree
Hide file tree
Showing 22 changed files with 236 additions and 3 deletions.
3 changes: 3 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,9 @@ SAIL_DEFAULT_INST += riscv_insts_zks.sail
SAIL_DEFAULT_INST += riscv_insts_zbkb.sail
SAIL_DEFAULT_INST += riscv_insts_zbkx.sail

SAIL_DEFAULT_INST += riscv_insts_zicbom.sail
SAIL_DEFAULT_INST += riscv_insts_zicboz.sail

SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail

Expand Down
3 changes: 3 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,9 @@ mach_bits plat_rom_base(unit u)
mach_bits plat_rom_size(unit u)
{ return rv_rom_size; }

mach_bits plat_cache_block_size()
{ return rv_cache_block_size; }

// Provides entropy for the scalar cryptography extension.
mach_bits plat_get_16_random_bits()
{ return rv_16_random_bits(); }
Expand Down
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ bool within_phys_mem(mach_bits, sail_int);
mach_bits plat_rom_base(unit);
mach_bits plat_rom_size(unit);

mach_bits plat_cache_block_size(unit);

// Provides entropy for the scalar cryptography extension.
mach_bits plat_get_16_random_bits();

Expand Down
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
uint64_t rv_rom_base = UINT64_C(0x1000);
uint64_t rv_rom_size = UINT64_C(0x100);

uint64_t rv_cache_block_size = UINT64_C(0x40);

// Provides entropy for the scalar cryptography extension.
uint64_t rv_16_random_bits(void) {
// This function can be changed to support deterministic sequences of
Expand Down
2 changes: 2 additions & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ extern uint64_t rv_ram_size;
extern uint64_t rv_rom_base;
extern uint64_t rv_rom_size;

extern uint64_t rv_cache_block_size;

// Provides entropy for the scalar cryptography extension.
extern uint64_t rv_16_random_bits(void);

Expand Down
13 changes: 13 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -133,6 +133,7 @@ static struct option options[] = {
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c'},
#endif
{"cache-block-size", required_argument, 0, 'B'},
{0, 0, 0, 0}
};

Expand Down Expand Up @@ -215,6 +216,7 @@ char *process_args(int argc, char **argv)
{
int c;
uint64_t ram_size = 0;
uint64_t block_size = 0;
while(true) {
c = getopt_long(argc, argv,
"a"
Expand Down Expand Up @@ -244,6 +246,7 @@ char *process_args(int argc, char **argv)
#ifdef SAILCOV
"c:"
#endif
"B:"
, options, NULL);
if (c == -1) break;
switch (c) {
Expand Down Expand Up @@ -344,6 +347,16 @@ char *process_args(int argc, char **argv)
sailcov_file = strdup(optarg);
break;
#endif
case 'B':
block_size = atol(optarg);
if (((block_size & (block_size - 1)) == 0) && (block_size < 4096)) {
fprintf(stderr, "setting cache-block-size to %" PRIu64 " B\n", block_size);
rv_cache_block_size = block_size;
} else {
fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg);
exit(1);
}
break;
case '?':
print_usage(argv[0], 1);
break;
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_size () = wordFromInteger 0
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_cache_block_size () = wordFromInteger 0
declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size`

val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_clint_base () = wordFromInteger 0
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/0.11/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_size () = wordFromInteger 0
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_cache_block_size () = wordFromInteger 0
declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size`

val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_clint_base () = wordFromInteger 0
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras.lem
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_size () = wordFromInteger 0
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_cache_block_size () = wordFromInteger 0
declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size`

val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_clint_base () = wordFromInteger 0
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
Expand Down
4 changes: 4 additions & 0 deletions handwritten_support/riscv_extras_sequential.lem
Original file line number Diff line number Diff line change
Expand Up @@ -167,6 +167,10 @@ val plat_rom_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_rom_size () = wordFromInteger 0
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val plat_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a
let plat_cache_block_size () = wordFromInteger 0
declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size`

val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a
let plat_clint_base () = wordFromInteger 0
declare ocaml target_rep function plat_clint_base = `Platform.clint_base`
Expand Down
4 changes: 4 additions & 0 deletions model/riscv_csr_map.sail
Original file line number Diff line number Diff line change
Expand Up @@ -111,6 +111,8 @@ mapping clause csr_name_map = 0x143 <-> "stval"
mapping clause csr_name_map = 0x144 <-> "sip"
/* supervisor protection and translation */
mapping clause csr_name_map = 0x180 <-> "satp"
/* supervisor envcfg */
mapping clause csr_name_map = 0x10A <-> "senvcfg"
/* machine information registers */
mapping clause csr_name_map = 0xF11 <-> "mvendorid"
mapping clause csr_name_map = 0xF12 <-> "marchid"
Expand Down Expand Up @@ -157,6 +159,8 @@ mapping clause csr_name_map = 0xB00 <-> "mcycle"
mapping clause csr_name_map = 0xB02 <-> "minstret"
mapping clause csr_name_map = 0xB80 <-> "mcycleh"
mapping clause csr_name_map = 0xB82 <-> "minstreth"
/* machine envcfg */
mapping clause csr_name_map = 0x30A <-> "menvcfg"
/* TODO: other hpm counters and events */
/* trigger/debug */
mapping clause csr_name_map = 0x7a0 <-> "tselect"
Expand Down
76 changes: 76 additions & 0 deletions model/riscv_insts_zicbom.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
/* ****************************************************************** */
/* This file specifies the instructions in the Zicbom extension */

/* ****************************************************************** */
union clause ast = RISCV_ZICBOM : (cbop_zicbom, regidx)

mapping encdec_cbop : cbop_zicbom <-> bits(12) = {
CBO_CLEAN <-> 0b000000000001,
CBO_FLUSH <-> 0b000000000010,
CBO_INVAL <-> 0b000000000000
}

mapping clause encdec = RISCV_ZICBOM(cbop, rs1) if haveZicbom()
<-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicbom()

mapping cbop_mnemonic : cbop_zicbom <-> string = {
CBO_CLEAN <-> "cbo.clean",
CBO_FLUSH <-> "cbo.flush",
CBO_INVAL <-> "cbo.inval"
}

mapping clause assembly = RISCV_ZICBOM(cbop, rs1)
<-> cbop_mnemonic(cbop) ^ spc() ^ reg_name(rs1)

val process_clean_inval : (xlenbits, xlenbits, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_clean_inval(vaddr, width, cbop) = {
match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Read(Data), cur_privilege),
TR_Failure(e, _) => Some(e)
};
match res {
None() => RETIRE_SUCCESS, // do nothing for cbop currently
Some(e) => {
match (e) {
E_Load_Access_Fault() => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
E_Load_Page_Fault() => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }
}
}
}
}
}
}

function cbo_clean_flush_enable(p : Privilege) -> bool =
~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | ((p == User) & (senvcfg.CBCFE() == 0b0)))

function cbop_for_cbo_inval(p : Privilege) -> option(cbop_zicbom) = {
let illegal = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
((p == User) & (senvcfg.CBIE() == 0b00));
let flush = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
((p == User) & (senvcfg.CBIE() == 0b01));
if illegal then None()
else if flush then Some(CBO_FLUSH)
else Some(CBO_INVAL)
}

function clause execute(RISCV_ZICBOM(cbop, rs1)) = {
let rs1_val = X(rs1);
let cache_block_size = plat_cache_block_size();
let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1));
let cbcfe = cbo_clean_flush_enable(cur_privilege);
let final_op : option(cbop_zicbom) = match (cbop, cbcfe) {
(CBO_CLEAN, true) => Some(CBO_CLEAN),
(CBO_CLEAN, false) => None(),
(CBO_FLUSH, true) => Some(CBO_FLUSH),
(CBO_FLUSH, false) => None(),
(CBO_INVAL, _) => cbop_for_cbo_inval(cur_privilege)
};
match final_op {
None() => { handle_illegal(); RETIRE_FAIL },
Some(cbop) => process_clean_inval(vaddr, cache_block_size, cbop)
}
}
57 changes: 57 additions & 0 deletions model/riscv_insts_zicboz.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
/* ****************************************************************** */
/* This file specifies the instructions in the Zicboz extension */

/* ****************************************************************** */
union clause ast = RISCV_ZICBOZ : (regidx)
mapping clause encdec = RISCV_ZICBOZ(rs1) if haveZicboz()
<-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicboz()

mapping clause assembly = RISCV_ZICBOZ(rs1)
<-> "cbo.zero" ^ spc() ^ reg_name(rs1)

function get_envcfg_cbze(p : Privilege) -> bool =
~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | ((p == User) & (senvcfg.CBZE() == 0b0)))

val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_cbo_zero(vaddr, width) = {
offset : xlenbits = zeros();
failed : bool = false;
while (offset <_u width) & (failed == false) do {
let addr = vaddr + offset;
match ext_data_get_addr(zeros(), addr, Write(Data), BYTE) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true },
Ext_DataAddr_OK(vaddr) =>
match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); failed = true },
TR_Address(paddr, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); failed = true },
MemValue(_) => {
let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, zeros(), false, false, false);
match (res) {
MemValue(true) => offset = offset + EXTZ(0b1),
MemValue(false) => internal_error("store got false from mem_write_value"),
MemException(e) => { handle_mem_exception(vaddr, e); failed = true }
}
}
}
}
}
};
};
if failed then RETIRE_FAIL
else RETIRE_SUCCESS
}

function clause execute(RISCV_ZICBOZ(rs1)) = {
let rs1_val = X(rs1);
let cache_block_size = plat_cache_block_size();
let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1));
if get_envcfg_cbze(cur_privilege) then
process_cbo_zero(vaddr, cache_block_size)
else {
handle_illegal();
RETIRE_FAIL
}
}
4 changes: 4 additions & 0 deletions model/riscv_insts_zicsr.sail
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,7 @@ function readCSR csr : csreg -> xlenbits = {
(0x304, _) => mie.bits(),
(0x305, _) => get_mtvec(),
(0x306, _) => EXTZ(mcounteren.bits()),
(0x30A, _) => menvcfg.bits(),
(0x310, 32) => mstatush.bits(),
(0x320, _) => EXTZ(mcountinhibit.bits()),

Expand Down Expand Up @@ -143,6 +144,7 @@ function readCSR csr : csreg -> xlenbits = {
(0x104, _) => lower_mie(mie, mideleg).bits(),
(0x105, _) => get_stvec(),
(0x106, _) => EXTZ(scounteren.bits()),
(0x10A, _) => senvcfg.bits(),
(0x140, _) => sscratch,
(0x141, _) => get_xret_target(Supervisor) & pc_alignment_mask(),
(0x142, _) => scause.bits(),
Expand Down Expand Up @@ -184,6 +186,7 @@ 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(EXTZ(mcounteren.bits())) },
(0x30A, _) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) },
(0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now
(0x320, _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(EXTZ(mcountinhibit.bits())) },
(0x340, _) => { mscratch = value; Some(mscratch) },
Expand Down Expand Up @@ -231,6 +234,7 @@ 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(EXTZ(scounteren.bits())) },
(0x10A, _) => { senvcfg = legalize_envcfg(senvcfg, value); Some(senvcfg.bits()) },
(0x140, _) => { sscratch = value; Some(sscratch) },
(0x141, _) => { Some(set_xret_target(Supervisor, value)) },
(0x142, _) => { scause->bits() = value; Some(scause.bits()) },
Expand Down
2 changes: 2 additions & 0 deletions model/riscv_platform.sail
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,8 @@ val elf_entry = {
c: "elf_entry"
} : unit -> int

val plat_cache_block_size = {c: "plat_cache_block_size", ocaml: "Platform.cache_block_size", interpreter: "Platform.cache_block_size", lem: "plat_cache_block_size"} : unit -> xlenbits

/* Main memory */
val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits
val plat_ram_size = {c: "plat_ram_size", ocaml: "Platform.dram_size", interpreter: "Platform.dram_size", lem: "plat_ram_size"} : unit -> xlenbits
Expand Down
10 changes: 7 additions & 3 deletions model/riscv_pmp_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -149,10 +149,8 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_acce
}

/* priority checks */

function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
function pmpCheck_xlen (addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
let check : bool =
match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) {
PMP_Success => true,
Expand Down Expand Up @@ -233,6 +231,12 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
}
}

function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
pmpCheck_xlen(addr, width, acc, priv)
}

function init_pmp() -> unit = {
pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF));
pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF));
Expand Down
5 changes: 5 additions & 0 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x304 => p == Machine, // mie
0x305 => p == Machine, // mtvec
0x306 => p == Machine & haveUsrMode(), // mcounteren
0x30a => p == Machine, // menvcfg
0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
0x320 => p == Machine, // mcountinhibit
/* machine mode: trap handling */
Expand Down Expand Up @@ -138,6 +139,8 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
0x105 => haveSupMode() & (p == Machine | p == Supervisor), // stvec
0x106 => haveSupMode() & (p == Machine | p == Supervisor), // scounteren

0x10a => haveSupMode() & (p == Machine | p == Supervisor), // senvcfg

/* supervisor mode: trap handling */
0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch
0x141 => haveSupMode() & (p == Machine | p == Supervisor), // sepc
Expand Down Expand Up @@ -596,6 +599,8 @@ function init_sys() -> unit = {
minstret = EXTZ(0b0);
minstret_written = false;

menvcfg->bits() = EXTZ(0b0);

init_pmp();

// log compatibility with spike
Expand Down
Loading

0 comments on commit 54f4dc9

Please sign in to comment.