Skip to content

Commit

Permalink
Merge pull request #455 from Timmmm/user/timh/cbo
Browse files Browse the repository at this point in the history
Implement Zicbom, Zicboz (cbo.flush, cbo.inval, cbo.zero)
  • Loading branch information
billmcspadden-riscv authored Aug 30, 2024
2 parents 05b845c + fcd31da commit e199a2e
Show file tree
Hide file tree
Showing 18 changed files with 308 additions and 2 deletions.
2 changes: 2 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail
SAIL_DEFAULT_INST += riscv_insts_vext_fp_vm.sail
SAIL_DEFAULT_INST += riscv_insts_vext_red.sail
SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.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
15 changes: 15 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,16 @@ bool sys_enable_bext(unit u)
return rv_enable_bext;
}

bool sys_enable_zicbom(unit u)
{
return rv_enable_zicbom;
}

bool sys_enable_zicboz(unit u)
{
return rv_enable_zicboz;
}

uint64_t sys_pmp_count(unit u)
{
return rv_pmp_count;
Expand Down Expand Up @@ -112,6 +122,11 @@ mach_bits plat_rom_size(unit u)
return rv_rom_size;
}

mach_bits plat_cache_block_size_exp()
{
return rv_cache_block_size_exp;
}

// Provides entropy for the scalar cryptography extension.
mach_bits plat_get_16_random_bits(unit u)
{
Expand Down
4 changes: 4 additions & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ bool sys_enable_writable_misa(unit);
bool sys_enable_writable_fiom(unit);
bool sys_enable_vext(unit);
bool sys_enable_bext(unit);
bool sys_enable_zicbom(unit);
bool sys_enable_zicboz(unit);

uint64_t sys_pmp_count(unit);
uint64_t sys_pmp_grain(unit);
Expand All @@ -26,6 +28,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_exp(unit);

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

Expand Down
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ bool rv_enable_writable_misa = true;
bool rv_enable_fdext = true;
bool rv_enable_vext = true;
bool rv_enable_bext = false;
bool rv_enable_zicbom = false;
bool rv_enable_zicboz = false;

bool rv_enable_dirty_update = false;
bool rv_enable_misaligned = false;
Expand All @@ -27,6 +29,9 @@ uint64_t rv_ram_size = UINT64_C(0x4000000);
uint64_t rv_rom_base = UINT64_C(0x1000);
uint64_t rv_rom_size = UINT64_C(0x100);

// Default 64, which is mandated by RVA22.
uint64_t rv_cache_block_size_exp = UINT64_C(6);

// Provides entropy for the scalar cryptography extension.
uint64_t rv_16_random_bits(void)
{
Expand Down
4 changes: 4 additions & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@ extern bool rv_enable_next;
extern bool rv_enable_fdext;
extern bool rv_enable_vext;
extern bool rv_enable_bext;
extern bool rv_enable_zicbom;
extern bool rv_enable_zicboz;
extern bool rv_enable_writable_misa;
extern bool rv_enable_dirty_update;
extern bool rv_enable_misaligned;
Expand All @@ -31,6 +33,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_exp;

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

Expand Down
38 changes: 38 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,9 @@ enum {
OPT_PMP_GRAIN,
OPT_ENABLE_SVINVAL,
OPT_ENABLE_ZCB,
OPT_ENABLE_ZICBOM,
OPT_ENABLE_ZICBOZ,
OPT_CACHE_BLOCK_SIZE,
};

static bool do_dump_dts = false;
Expand Down Expand Up @@ -151,6 +154,9 @@ static struct option options[] = {
{"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM},
{"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL },
{"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB },
{"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM },
{"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ },
{"cache-block-size", required_argument, 0, OPT_CACHE_BLOCK_SIZE },
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c' },
#endif
Expand Down Expand Up @@ -234,6 +240,17 @@ static void read_dtb(const char *path)
fprintf(stdout, "Read %zd bytes of DTB from %s.\n", dtb_len, path);
}

// Return log2(x), or -1 if x is not a power of 2.
static int ilog2(uint64_t x)
{
for (unsigned i = 0; i < sizeof(x) * 8; ++i) {
if (x == (UINT64_C(1) << i)) {
return i;
}
}
return -1;
}

/**
* Parses the command line arguments and returns the argv index for the first
* ELF file that should be loaded. As getopt transforms the argv array, all
Expand All @@ -247,6 +264,7 @@ static int process_args(int argc, char **argv)
uint64_t ram_size = 0;
uint64_t pmp_count = 0;
uint64_t pmp_grain = 0;
uint64_t block_size_exp = 0;
while (true) {
c = getopt_long(argc, argv,
"a"
Expand Down Expand Up @@ -401,6 +419,26 @@ static int process_args(int argc, char **argv)
fprintf(stderr, "enabling Zcb extension.\n");
rv_enable_zcb = true;
break;
case OPT_ENABLE_ZICBOM:
fprintf(stderr, "enabling Zicbom extension.\n");
rv_enable_zicbom = true;
break;
case OPT_ENABLE_ZICBOZ:
fprintf(stderr, "enabling Zicboz extension.\n");
rv_enable_zicboz = true;
break;
case OPT_CACHE_BLOCK_SIZE:
block_size_exp = ilog2(atol(optarg));

if (block_size_exp < 0 || block_size_exp > 12) {
fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg);
exit(1);
}

fprintf(stderr, "setting cache-block-size to 2^%" PRIu64 " = %u B\n",
block_size_exp, 1 << block_size_exp);
rv_cache_block_size_exp = block_size_exp;
break;
case 'x':
fprintf(stderr, "enabling Zfinx support.\n");
rv_enable_zfinx = true;
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 @@ -193,6 +193,10 @@ val plat_rom_size : unit -> bitvector
let plat_rom_size () = []
declare ocaml target_rep function plat_rom_size = `Platform.rom_size`

val plat_cache_block_size_exp : unit -> bitvector
let plat_cache_block_size_exp () = []
declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp`

val plat_clint_base : unit -> bitvector
let plat_clint_base () = []
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 @@ -173,6 +173,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_exp : unit -> integer
let plat_cache_block_size_exp () = wordFromInteger 0
declare ocaml target_rep function plat_cache_block_size_exp = `Platform.cache_block_size_exp`

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
114 changes: 114 additions & 0 deletions model/riscv_insts_zicbom.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
/*=======================================================================================*/
/* 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 */
/*=======================================================================================*/

// Cache Block Operations - Management

enum clause extension = Ext_Zicbom
function clause extensionEnabled(Ext_Zicbom) = sys_enable_zicbom()

function cbo_clean_flush_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBCFE][0], senvcfg[CBCFE][0])
function cbo_inval_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][0], senvcfg[CBIE][0])
function cbo_inval_as_inval(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBIE][1], senvcfg[CBIE][1])

/* ****************************************************************** */
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 extensionEnabled(Ext_Zicbom)
<-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if extensionEnabled(Ext_Zicbom)

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() ^ "(" ^ opt_spc() ^ reg_name(rs1) ^ opt_spc() ^ ")"

val process_clean_inval : (regidx, cbop_zicbom) -> Retired
function process_clean_inval(rs1, cbop) = {
let rs1_val = X(rs1);
let cache_block_size_exp = plat_cache_block_size_exp();
let cache_block_size = 2 ^ cache_block_size_exp;

// Offset from rs1 to the beginning of the cache block. This is 0 if rs1
// is aligned to the cache block, or negative if rs1 is misaligned.
let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val;

// TODO: This is incorrect since CHERI only requires at least one byte
// to be in bounds here, whereas `ext_data_get_addr()` checks that all bytes
// are in bounds. We will need to add a new function, parameter or access type.
match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) {
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, _) => {
// "A cache-block management instruction is permitted to access the
// specified cache block whenever a load instruction or store instruction
// is permitted to access the corresponding physical addresses. If
// neither a load instruction nor store instruction is permitted to
// access the physical addresses, but an instruction fetch is permitted
// to access the physical addresses, whether a cache-block management
// instruction is permitted to access the cache block is UNSPECIFIED."
//
// In this implementation we currently don't allow access for fetches.
let exc_read = phys_access_check(Read(Data), cur_privilege, paddr, cache_block_size);
let exc_write = phys_access_check(Write(Data), cur_privilege, paddr, cache_block_size);
match (exc_read, exc_write) {
// Access is permitted if read OR write are allowed. If neither
// are allowed then we always report a store exception.
(Some(exc_read), Some(exc_write)) => Some(exc_write),
_ => None(),
}
},
TR_Failure(e, _) => Some(e)
};
// "If access to the cache block is not permitted, a cache-block management
// instruction raises a store page fault or store guest-page fault exception
// if address translation does not permit any access or raises a store access
// fault exception otherwise."
match res {
// The model has no caches so there's no action required.
None() => RETIRE_SUCCESS,
Some(e) => {
let e : ExceptionType = match e {
E_Load_Access_Fault() => E_SAMO_Access_Fault(),
E_SAMO_Access_Fault() => E_SAMO_Access_Fault(),
E_Load_Page_Fault() => E_SAMO_Page_Fault(),
E_SAMO_Page_Fault() => E_SAMO_Page_Fault(),
// No other exceptions should be generated since we're not checking
// for fetch access and it's can't be misaligned.
_ => internal_error(__FILE__, __LINE__, "unexpected exception for cmo.clean/inval"),
};
handle_mem_exception(vaddr, e);
RETIRE_FAIL
}
}
}
}
}

function clause execute(RISCV_ZICBOM(cbop, rs1)) =
match cbop {
CBO_CLEAN if cbo_clean_flush_enabled(cur_privilege) =>
process_clean_inval(rs1, cbop),
CBO_FLUSH if cbo_clean_flush_enabled(cur_privilege) =>
process_clean_inval(rs1, cbop),
CBO_INVAL if cbo_inval_enabled(cur_privilege) =>
process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH),
_ => {
handle_illegal();
RETIRE_FAIL
},
}
65 changes: 65 additions & 0 deletions model/riscv_insts_zicboz.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
/*=======================================================================================*/
/* 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 */
/*=======================================================================================*/

// Cache Block Operations - Zero

enum clause extension = Ext_Zicboz
function clause extensionEnabled(Ext_Zicboz) = sys_enable_zicboz()

function cbo_zero_enabled(p : Privilege) -> bool = feature_enabled_for_priv(p, menvcfg[CBZE][0], senvcfg[CBZE][0])

/* ****************************************************************** */
union clause ast = RISCV_ZICBOZ : (regidx)

mapping clause encdec = RISCV_ZICBOZ(rs1) if extensionEnabled(Ext_Zicboz)
<-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if extensionEnabled(Ext_Zicboz)

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

function clause execute(RISCV_ZICBOZ(rs1)) = {
if cbo_zero_enabled(cur_privilege) then {
let rs1_val = X(rs1);
let cache_block_size_exp = plat_cache_block_size_exp();
let cache_block_size = 2 ^ cache_block_size_exp;

// Offset from rs1 to the beginning of the cache block. This is 0 if rs1
// is aligned to the cache block, or negative if rs1 is misaligned.
let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val;

match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
// "An implementation may update the bytes in any order and with any granularity
// and atomicity, including individual bytes."
//
// This implementation does a single atomic write.
match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(paddr, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, cache_block_size, false, false, false);
match (eares) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
let res : MemoryOpResult(bool) = mem_write_value(paddr, cache_block_size, zeros(), false, false, false);
match (res) {
MemValue(true) => RETIRE_SUCCESS,
MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
}
}
}
}
}
},
}
} else {
handle_illegal();
RETIRE_FAIL
}
}
5 changes: 5 additions & 0 deletions model/riscv_platform.sail
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,11 @@ val elf_entry = {
c: "elf_entry"
} : unit -> int

// Cache block size is 2^cache_block_size_exp. Max is `max_mem_access` (4096)
// because this model performs `cbo.zero` with a single write, and the behaviour
// with cache blocks larger than a page is not clearly defined.
val plat_cache_block_size_exp = {c: "plat_cache_block_size_exp", ocaml: "Platform.cache_block_size_exp", interpreter: "Platform.cache_block_size_exp", lem: "plat_cache_block_size_exp"} : unit -> range(0, 12)

/* 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
8 changes: 8 additions & 0 deletions model/riscv_sys_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,14 @@ function check_CSR_access(csrrw, csrpr, p, isWrite) =
function check_TVM_SATP(csr : csreg, p : Privilege) -> bool =
not(csr == 0x180 & p == Supervisor & mstatus[TVM] == 0b1)

// There are several features that are controlled by machine/supervisor enable
// bits (m/senvcfg, m/scounteren, etc.). This abstracts that logic.
function feature_enabled_for_priv(p : Privilege, machine_enable_bit : bit, supervisor_enable_bit : bit) -> bool = match p {
Machine => true,
Supervisor => machine_enable_bit == bitone,
User => machine_enable_bit == bitone & (not(extensionEnabled(Ext_S)) | supervisor_enable_bit == bitone),
}

function check_Counteren(csr : csreg, p : Privilege) -> bool =
match(csr, p) {
(0xC00, Supervisor) => mcounteren[CY] == 0b1,
Expand Down
Loading

0 comments on commit e199a2e

Please sign in to comment.