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)");