From cfb00b45f86ada151298fe5a8353dcb74af3915a Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Fri, 12 Apr 2024 13:41:21 +0100 Subject: [PATCH] Implement Zicbom, Zicboz (cbo.flush, cbo.inval, cbo.zero) 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). --- Makefile | 2 + c_emulator/riscv_platform.c | 5 + c_emulator/riscv_platform.h | 2 + c_emulator/riscv_platform_impl.c | 2 + c_emulator/riscv_platform_impl.h | 2 + c_emulator/riscv_sim.c | 17 ++- handwritten_support/riscv_extras.lem | 4 + .../riscv_extras_sequential.lem | 4 + model/prelude_mem.sail | 11 +- model/riscv_addr_checks.sail | 2 +- model/riscv_insts_aext.sail | 6 +- model/riscv_insts_base.sail | 4 +- model/riscv_insts_fext.sail | 4 +- model/riscv_insts_vext_mem.sail | 26 ++--- model/riscv_insts_zicbom.sail | 109 ++++++++++++++++++ model/riscv_insts_zicboz.sail | 68 +++++++++++ model/riscv_platform.sail | 3 + model/riscv_sys_control.sail | 8 ++ model/riscv_sys_regs.sail | 12 ++ model/riscv_types.sail | 2 + ocaml_emulator/platform.ml | 2 + ocaml_emulator/platform_impl.ml | 5 + ocaml_emulator/riscv_ocaml_sim.ml | 3 + 23 files changed, 279 insertions(+), 24 deletions(-) create mode 100644 model/riscv_insts_zicbom.sail create mode 100644 model/riscv_insts_zicboz.sail diff --git a/Makefile b/Makefile index 7068968f4..8158560d4 100644 --- a/Makefile +++ b/Makefile @@ -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 diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 6544de65c..3a5ae20db 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -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() { diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 4a53d12ac..d660381f8 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -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(); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 449bb1df7..e753a2ffa 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -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) { diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index d377c9c43..8cb43bb7a 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -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); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index bf68da282..d2e50fd6e 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -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; @@ -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 } }; @@ -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" @@ -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); diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 27e8ee5ed..4bab0cd39 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -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` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index d1139081d..5ffe482cd 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -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` diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index c4f3d0710..c2488eff2 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -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) = { diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index f9c783574..38a7316d2 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -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) diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 0f4da8372..0e0a52b32 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -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 = @@ -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 = @@ -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)) { diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index 9c4630b33..d28f51d7b 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -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) @@ -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) diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index e4afb30d5..664495450 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -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) @@ -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) diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail index ce9cd6237..4da82e18f 100644 --- a/model/riscv_insts_vext_mem.sail +++ b/model/riscv_insts_vext_mem.sail @@ -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) @@ -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 { @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) @@ -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) diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail new file mode 100644 index 000000000..0c5ab3779 --- /dev/null +++ b/model/riscv_insts_zicbom.sail @@ -0,0 +1,109 @@ +/*=======================================================================================*/ +/* 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 +// +// Note that the CBOP prefetch instructions are existing base instructions that +// are just defined to be hints, so there is not need to add any code for them +// (since this model has no caches to prefetch into and the encodings already +// exist). + +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 the beginning of the cache block. + let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val; + + // TODO: This may not be correct since CHERI may treat CBO operations + // differently to normal accesses with respect to bounds checks. + 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) { + (Some(e0), Some(e1)) => Some(e1), + _ => 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)) = { + if (cbop == CBO_CLEAN | cbop == CBO_FLUSH) & cbo_clean_flush_enabled(cur_privilege) then { + process_clean_inval(rs1, cbop) + } else if (cbop == CBO_INVAL) & cbo_inval_enabled(cur_privilege) then { + process_clean_inval(rs1, if cbo_inval_as_inval(cur_privilege) then CBO_INVAL else CBO_FLUSH) + } else { + handle_illegal(); + RETIRE_FAIL + } +} diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail new file mode 100644 index 000000000..4e28f9bd2 --- /dev/null +++ b/model/riscv_insts_zicboz.sail @@ -0,0 +1,68 @@ +/*=======================================================================================*/ +/* 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 +// +// Note that the CBOP prefetch instructions are existing base instructions that +// are just defined to be hints, so there is not need to add any code for them +// (since this model has no caches to prefetch into and the encodings already +// exist). + +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 the beginning of the cache block. + let offset = (rs1_val & ~(zero_extend(ones(cache_block_size_exp)))) - rs1_val; + + // TODO: This may not be correct since CHERI may treat 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 + } +} diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 19e3d30ae..b21e6af57 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -26,6 +26,9 @@ val elf_entry = { c: "elf_entry" } : unit -> int +// Cache block size is 2^cache_block_size_exp. Max 4096. +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 diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index ecc53ae85..dfe7f7899 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -100,6 +100,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(haveSupMode()) | supervisor_enable_bit == bitone), +} + function check_Counteren(csr : csreg, p : Privilege) -> bool = match(csr, p) { (0xC00, Supervisor) => mcounteren[CY] == 0b1, diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 3e198b43e..8b42b5b15 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -103,6 +103,14 @@ val sys_pmp_grain = {c: "sys_pmp_grain", ocaml: "Platform.pmp_grain", _: "sys_pm /* whether misa.v was enabled at boot */ val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool +// CBO extensions. Zicbop cannot be enabled/disabled because it has no effect +// at all on this model. +// TODO: Add command line flags. +// val sys_enable_zicbom = {c: "sys_enable_zicbom", ocaml: "Platform.enable_zicbom", _: "sys_enable_zicbom"} : unit -> bool +// val sys_enable_zicboz = {c: "sys_enable_zicboz", ocaml: "Platform.enable_zicboz", _: "sys_enable_zicboz"} : unit -> bool +function sys_enable_zicbom() -> bool = true +function sys_enable_zicboz() -> bool = true + /* This function allows an extension to veto a write to Misa if it would violate an alignment restriction on unsetting C. If it returns true the write will have no effect. */ @@ -162,6 +170,10 @@ function haveZmmul() -> bool = true /* Zicond extension support */ function haveZicond() -> bool = true +/* Cache Management Operations extension support. */ +function haveZicbom() -> bool = sys_enable_zicbom() +function haveZicboz() -> bool = sys_enable_zicboz() + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 diff --git a/model/riscv_types.sail b/model/riscv_types.sail index e9a5a1990..c592dd8da 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -336,6 +336,8 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */ +enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* Zicbom ops */ + enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD} enum brop_zbb = {RISCV_ANDN, RISCV_ORN, RISCV_XNOR, RISCV_MAX, diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 2f0aaaf7c..62c514b7a 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -101,6 +101,8 @@ let rom_size () = arch_bits_of_int !rom_size_ref let dram_base () = arch_bits_of_int64 P.dram_base let dram_size () = arch_bits_of_int64 !P.dram_size_ref +let cache_block_size_exp () = Big_int.of_int64 !P.cache_block_size_exp_ref + let clint_base () = arch_bits_of_int64 P.clint_base let clint_size () = arch_bits_of_int64 P.clint_size diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml index 39de43776..6a5d83506 100644 --- a/ocaml_emulator/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml @@ -57,6 +57,8 @@ let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) let dram_size_ref = ref (Int64.(shift_left 64L 20)) +let cache_block_size_exp_ref = ref (Int64.(6L)) + type mem_region = { addr : Int64.t; size : Int64.t @@ -144,6 +146,9 @@ let set_dtc path = let set_dram_size mb = dram_size_ref := Int64.(shift_left (Int64.of_int mb) 20) +let set_cache_block_size_exp b = + cache_block_size_exp_ref := Int64.(Int64.of_int b) + let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) try let cmd = Printf.sprintf "%s -I dts" !dtc_path in diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 8dad8a45a..2f2e8d825 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -71,6 +71,9 @@ let options = Arg.align ([("-dump-dts", ("-ram-size", Arg.Int PI.set_dram_size, " size of physical ram memory to use (in MB)"); + ("-cache-block-size-exp", + Arg.Int PI.set_cache_block_size_exp, + " 2^N exponent of the cache block size (max 12)"); ("-report-arch", Arg.Unit report_arch, " report model architecture (RV32 or RV64)");