Skip to content

Commit

Permalink
Implement Zicbom, Zicboz (cbo.flush, cbo.inval, cbo.zero)
Browse files Browse the repository at this point in the history
Note that Zicbop (prefetch hints) does not need to be implemented because all it does is label some existing base instructions as prefetch hints.
  • Loading branch information
Timmmm committed Aug 5, 2024
1 parent 2078d87 commit c0729fb
Show file tree
Hide file tree
Showing 18 changed files with 308 additions and 3 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
39 changes: 38 additions & 1 deletion 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 ((1ull << i) == x) {
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 All @@ -414,7 +452,6 @@ static int process_args(int argc, char **argv)
case OPT_TRACE_OUTPUT:
trace_log_path = optarg;
fprintf(stderr, "using %s for trace output.\n", trace_log_path);
break;
case '?':
print_usage(argv[0], 1);
break;
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
111 changes: 111 additions & 0 deletions model/riscv_insts_zicbom.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,111 @@
/*=======================================================================================*/
/* 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

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 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() ^ "(" ^ 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
},
}
64 changes: 64 additions & 0 deletions model/riscv_insts_zicboz.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
/*=======================================================================================*/
/* 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

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 haveZicboz()
<-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicboz()

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;

// TODO: This is not correct since CHERI treats CBO operations
// differently to normal accesses with respect to bounds checks.
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 c0729fb

Please sign in to comment.