diff --git a/Makefile b/Makefile index da4029633..ea94caa14 100644 --- a/Makefile +++ b/Makefile @@ -57,6 +57,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 2fdb63f92..bb7c178ae 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -107,6 +107,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) { diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 341bd5964..981ec92c4 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -25,6 +25,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); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 077fc50dc..f47dd893d 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -26,6 +26,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 c4289e679..ecb0c9b82 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -30,6 +30,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 3a9bfc08d..0a35af5e3 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -54,7 +54,8 @@ const char *RV32ISA = "RV32IMAC"; #define OPT_PMP_COUNT 1002 #define OPT_PMP_GRAIN 1003 #define OPT_ENABLE_SVINVAL 1004 -#define OPT_ENABLE_ZCB 10014 +#define OPT_ENABLE_ZCB 1005 +#define OPT_CACHE_BLOCK_SIZE_EXP 1006 static bool do_dump_dts = false; static bool do_show_times = false; @@ -152,6 +153,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 } }; @@ -245,6 +247,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" @@ -407,6 +410,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 4bc330020..245a7fe80 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -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` 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/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 1baa33701..6f0d5cf4e 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -101,6 +101,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 6c66492b4..3504bfa70 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -105,6 +105,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. */ @@ -164,6 +172,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 2b1c132ec..643cd1d75 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 69f271496..cab41054c 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -103,6 +103,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 56be8d8a8..d3467ed4b 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -74,6 +74,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)");