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.

Also I have not wired up the enable flags to the emulators because it is rather tedious (and will hopefully be replaced by riscv-config at some point).
  • Loading branch information
Timmmm committed May 15, 2024
1 parent 34e43b2 commit 50b6955
Show file tree
Hide file tree
Showing 23 changed files with 279 additions and 24 deletions.
2 changes: 2 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ SAIL_DEFAULT_INST += riscv_insts_vext_mem.sail
SAIL_DEFAULT_INST += riscv_insts_vext_mask.sail
SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail
SAIL_DEFAULT_INST += riscv_insts_vext_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
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -102,6 +102,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()
{
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 @@ -24,6 +24,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();

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 @@ -25,6 +25,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_exp = UINT64_C(6);

// Provides entropy for the scalar cryptography extension.
uint64_t rv_16_random_bits(void)
{
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 @@ -29,6 +29,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
17 changes: 16 additions & 1 deletion c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,8 @@ const char *RV32ISA = "RV32IMAC";
#define OPT_ENABLE_WRITABLE_FIOM 1001
#define OPT_PMP_COUNT 1002
#define OPT_PMP_GRAIN 1003
#define OPT_ENABLE_ZCB 10014
#define OPT_ENABLE_ZCB 1004
#define OPT_CACHE_BLOCK_SIZE_EXP 1005

static bool do_dump_dts = false;
static bool do_show_times = false;
Expand Down Expand Up @@ -150,6 +151,7 @@ static struct option options[] = {
#ifdef SAILCOV
{"sailcov-file", required_argument, 0, 'c' },
#endif
{"cache-block-size-exp", required_argument, 0, OPT_CACHE_BLOCK_SIZE_EXP},
{0, 0, 0, 0 }
};

Expand Down Expand Up @@ -243,6 +245,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 @@ -405,6 +408,18 @@ 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);
case OPT_CACHE_BLOCK_SIZE_EXP:
block_size_exp = atol(optarg);
if (block_size_exp <= 12) {
fprintf(stderr,
"setting cache-block-size-exp to 2^%" PRIu64 " = %u B\n",
block_size_exp, 1 << block_size_exp);
rv_cache_block_size_exp = block_size_exp;
} else {
fprintf(stderr, "invalid cache-block-size-exp '%s' provided.\n",
optarg);
exit(1);
}
break;
case '?':
print_usage(argv[0], 1);
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 @@ -185,6 +185,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
11 changes: 9 additions & 2 deletions model/prelude_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,15 @@
because it means width argument can be fast native integer. It
would be even better if it could be <= 8 bytes so that data can
also be a 64-bit int but CHERI needs 128-bit accesses for
capabilities and SIMD / vector instructions will also need more. */
type max_mem_access : Int = 16
capabilities and SIMD / vector instructions will also need more.

The specific value does not matter (if it is >8) since anything up
to 2^64-1 will result in a native int being used for the width type.

4096 was chosen because it is a page size, and a reasonable maximum
for cbo.zero.
*/
type max_mem_access : Int = 4096

val write_ram = {lem: "write_ram", coq: "write_ram"} : forall 'n, 0 < 'n <= max_mem_access . (write_kind, xlenbits, int('n), bits(8 * 'n), mem_meta) -> bool
function write_ram(wk, addr, width, data, meta) = {
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_addr_checks.sail
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ type ext_data_addr_error = unit

/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : range(0, max_mem_access))
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_aext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
match ext_data_get_addr(rs1, zeros(), Read(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -126,7 +126,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
match ext_data_get_addr(rs1, zeros(), Write(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -216,7 +216,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) {
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite(Data, Data)) {
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_base.sail
Original file line number Diff line number Diff line change
Expand Up @@ -326,7 +326,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -382,7 +382,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_fext.sail
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
let offset : xlenbits = sign_extend(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
match ext_data_get_addr(rs1, offset, Read(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -381,7 +381,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
let (aq, rl, con) = (false, false, false);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
match ext_data_get_addr(rs1, offset, Write(Data), size_bytes(width)) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down
26 changes: 13 additions & 13 deletions model/riscv_insts_vext_mem.sail
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ function process_vlseg (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem) =
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = (i * nf + j) * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -149,7 +149,7 @@ function process_vlsegff (nf, vm, vd, load_width_bytes, rs1, EMUL_pow, num_elem)
if vm_val[i] then { /* active segments */
foreach (j from 0 to (nf - 1)) {
let elem_offset = (i * nf + j) * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => {
if i == 0 then { ext_handle_data_check_error(e); return RETIRE_FAIL }
else {
Expand Down Expand Up @@ -251,7 +251,7 @@ function process_vsseg (nf, vm, vs3, load_width_bytes, rs1, EMUL_pow, num_elem)
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = (i * nf + j) * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -322,7 +322,7 @@ function process_vlsseg (nf, vm, vd, load_width_bytes, rs1, rs2, EMUL_pow, num_e
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = i * rs2_val + j * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -388,7 +388,7 @@ function process_vssseg (nf, vm, vs3, load_width_bytes, rs1, rs2, EMUL_pow, num_
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset = i * rs2_val + j * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -460,7 +460,7 @@ function process_vlxseg (nf, vm, vd, EEW_index_bytes, EEW_data_bytes, EMUL_index
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), EEW_data_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -551,7 +551,7 @@ function process_vsxseg (nf, vm, vs3, EEW_index_bytes, EEW_data_bytes, EMUL_inde
vstart = to_bits(16, i);
foreach (j from 0 to (nf - 1)) {
let elem_offset : int = signed(vs2_val[i]) + j * EEW_data_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), EEW_data_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -644,7 +644,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
foreach (i from elem_to_align to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand All @@ -668,7 +668,7 @@ function process_vlre (nf, vd, load_width_bytes, rs1, elem_per_reg) = {
foreach (i from 0 to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Read(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -726,7 +726,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
foreach (i from elem_to_align to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset : int = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -760,7 +760,7 @@ function process_vsre (nf, load_width_bytes, rs1, vs3, elem_per_reg) = {
foreach (i from 0 to (elem_per_reg - 1)) {
vstart = to_bits(16, cur_elem);
let elem_offset = cur_elem * load_width_bytes;
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), elem_offset), Write(Data), load_width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down Expand Up @@ -828,7 +828,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
if i < evl then { /* active elements */
vstart = to_bits(16, i);
if op == VLM then { /* load */
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Read(Data), 1) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand All @@ -844,7 +844,7 @@ function process_vm(vd_or_vs3, rs1, num_elem, evl, op) = {
}
}
} else if op == VSM then { /* store */
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), width_type) {
match ext_data_get_addr(rs1, to_bits(sizeof(xlen), i), Write(Data), 1) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); return RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width_type)
Expand Down
Loading

0 comments on commit 50b6955

Please sign in to comment.