diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 17ad17faa..0e1620d45 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -48,8 +48,11 @@ mach_bits plat_rom_base(unit u) mach_bits plat_rom_size(unit u) { return rv_rom_size; } -mach_bits plat_cache_block_size() -{ return rv_cache_block_size; } +mach_bits plat_zicbom_cache_block_size(unit u) +{ return rv_zicbom_cache_block_size; } + +mach_bits plat_zicboz_cache_block_size(unit u) +{ return rv_zicboz_cache_block_size; } // 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 98efde81e..7b0952fc2 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -19,7 +19,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(unit); +mach_bits plat_zicbom_cache_block_size(unit); +mach_bits plat_zicboz_cache_block_size(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 1cadc985e..0e6b4e1ba 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -20,7 +20,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 = UINT64_C(0x40); +uint64_t rv_zicbom_cache_block_size = UINT64_C(0x40); +uint64_t rv_zicboz_cache_block_size = UINT64_C(0x40); // 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 b686578d2..d9da10b57 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -23,7 +23,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; +extern uint64_t rv_zicbom_cache_block_size; +extern uint64_t rv_zicboz_cache_block_size; // 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 2d80b45ce..13299fe82 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -133,7 +133,8 @@ static struct option options[] = { #ifdef SAILCOV {"sailcov-file", required_argument, 0, 'c'}, #endif - {"cache-block-size", required_argument, 0, 'B'}, + {"zicbom-cache-block-size", required_argument, 0, 'M'}, + {"zicboz-cache-block-size", required_argument, 0, 'Z'}, {0, 0, 0, 0} }; @@ -246,7 +247,8 @@ char *process_args(int argc, char **argv) #ifdef SAILCOV "c:" #endif - "B:" + "M:" + "Z:" , options, NULL); if (c == -1) break; switch (c) { @@ -347,13 +349,23 @@ char *process_args(int argc, char **argv) sailcov_file = strdup(optarg); break; #endif - case 'B': + case 'M': block_size = atol(optarg); - if (((block_size & (block_size - 1)) == 0) && (block_size < 4096)) { - fprintf(stderr, "setting cache-block-size to %" PRIu64 " B\n", block_size); - rv_cache_block_size = block_size; + if (((block_size & (block_size - 1)) == 0) && (block_size <= 4096)) { + fprintf(stderr, "setting cache-block-size for zicbom to %" PRIu64 " B\n", block_size); + rv_zicbom_cache_block_size = block_size; } else { - fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg); + fprintf(stderr, "invalid cache-block-size for zicbom '%s' provided.\n", optarg); + exit(1); + } + break; + case 'Z': + block_size = atol(optarg); + if (((block_size & (block_size - 1)) == 0) && (block_size <= 4096)) { + fprintf(stderr, "setting cache-block-size for zicboz to %" PRIu64 " B\n", block_size); + rv_zicboz_cache_block_size = block_size; + } else { + fprintf(stderr, "invalid cache-block-size for zicboz '%s' provided.\n", optarg); exit(1); } break; diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem index 3e038115a..a3ffa159b 100644 --- a/handwritten_support/0.11/riscv_extras.lem +++ b/handwritten_support/0.11/riscv_extras.lem @@ -107,9 +107,13 @@ 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 : forall 'a. Size 'a => unit -> bitvector 'a -let plat_cache_block_size () = wordFromInteger 0 -declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` +val plat_zicbom_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicbom_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicbom_cache_block_size = `Platform.zicbom_cache_block_size` + +val plat_zicboz_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicboz_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicboz_cache_block_size = `Platform.zicboz_cache_block_size` val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem index d841f615d..abe9fe353 100644 --- a/handwritten_support/0.11/riscv_extras_sequential.lem +++ b/handwritten_support/0.11/riscv_extras_sequential.lem @@ -99,9 +99,13 @@ 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 : forall 'a. Size 'a => unit -> bitvector 'a -let plat_cache_block_size () = wordFromInteger 0 -declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` +val plat_zicbom_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicbom_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicbom_cache_block_size = `Platform.zicbom_cache_block_size` + +val plat_zicboz_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicboz_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicboz_cache_block_size = `Platform.zicboz_cache_block_size` val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 1cf0714a7..8f64c8c1a 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -175,9 +175,13 @@ 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 : forall 'a. Size 'a => unit -> bitvector 'a -let plat_cache_block_size () = wordFromInteger 0 -declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` +val plat_zicbom_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicbom_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicbom_cache_block_size = `Platform.zicbom_cache_block_size` + +val plat_zicboz_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicboz_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicboz_cache_block_size = `Platform.zicboz_cache_block_size` val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index ca36eb931..886c66612 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -167,9 +167,13 @@ 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 : forall 'a. Size 'a => unit -> bitvector 'a -let plat_cache_block_size () = wordFromInteger 0 -declare ocaml target_rep function plat_cache_block_size = `Platform.cache_block_size` +val plat_zicbom_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicbom_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicbom_cache_block_size = `Platform.zicbom_cache_block_size` + +val plat_zicboz_cache_block_size : forall 'a. Size 'a => unit -> bitvector 'a +let plat_zicboz_cache_block_size () = wordFromInteger 0 +declare ocaml target_rep function plat_zicboz_cache_block_size = `Platform.zicboz_cache_block_size` val plat_clint_base : forall 'a. Size 'a => unit -> bitvector 'a let plat_clint_base () = wordFromInteger 0 diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail index 0365f8c0e..224693279 100644 --- a/model/riscv_insts_zicbom.sail +++ b/model/riscv_insts_zicbom.sail @@ -20,7 +20,7 @@ mapping cbop_mnemonic : cbop_zicbom <-> string = { } mapping clause assembly = RISCV_ZICBOM(cbop, rs1) - <-> cbop_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + <-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ reg_name(rs1) ^ ")" val process_clean_inval : (xlenbits, xlenbits, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg} function process_clean_inval(vaddr, width, cbop) = { @@ -59,7 +59,7 @@ function cbop_for_cbo_inval(p : Privilege) -> option(cbop_zicbom) = { function clause execute(RISCV_ZICBOM(cbop, rs1)) = { let rs1_val = X(rs1); - let cache_block_size = plat_cache_block_size(); + let cache_block_size = plat_zicbom_cache_block_size(); let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1)); let cbcfe = cbo_clean_flush_enable(cur_privilege); let final_op : option(cbop_zicbom) = match (cbop, cbcfe) { diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail index 3fd0f57d1..690446a36 100644 --- a/model/riscv_insts_zicboz.sail +++ b/model/riscv_insts_zicboz.sail @@ -7,7 +7,7 @@ mapping clause encdec = RISCV_ZICBOZ(rs1) if haveZicboz() <-> 0b000000000100 @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 if haveZicboz() mapping clause assembly = RISCV_ZICBOZ(rs1) - <-> "cbo.zero" ^ spc() ^ reg_name(rs1) + <-> "cbo.zero" ^ spc() ^ "(" ^ reg_name(rs1) ^ ")" function get_envcfg_cbze(p : Privilege) -> bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | ((p == User) & (senvcfg.CBZE() == 0b0))) @@ -46,7 +46,7 @@ function process_cbo_zero(vaddr, width) = { function clause execute(RISCV_ZICBOZ(rs1)) = { let rs1_val = X(rs1); - let cache_block_size = plat_cache_block_size(); + let cache_block_size = plat_zicboz_cache_block_size(); let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1)); if get_envcfg_cbze(cur_privilege) then process_cbo_zero(vaddr, cache_block_size) diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index c9e808e97..872ef167e 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -86,7 +86,8 @@ val elf_entry = { c: "elf_entry" } : unit -> int -val plat_cache_block_size = {c: "plat_cache_block_size", ocaml: "Platform.cache_block_size", interpreter: "Platform.cache_block_size", lem: "plat_cache_block_size"} : unit -> xlenbits +val plat_zicbom_cache_block_size = {c: "plat_zicbom_cache_block_size", ocaml: "Platform.zicbom_cache_block_size", interpreter: "Platform.zicbom_cache_block_size", lem: "plat_zicbom_cache_block_size"} : unit -> xlenbits +val plat_zicboz_cache_block_size = {c: "plat_zicboz_cache_block_size", ocaml: "Platform.zicboz_cache_block_size", interpreter: "Platform.zicboz_cache_block_size", lem: "plat_zicboz_cache_block_size"} : unit -> xlenbits /* Main memory */ val plat_ram_base = {c: "plat_ram_base", ocaml: "Platform.dram_base", interpreter: "Platform.dram_base", lem: "plat_ram_base"} : unit -> xlenbits diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index 8ffff87fd..c81da0f9f 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -90,7 +90,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 () = arch_bits_of_int64 !P.cache_block_size_ref +let zicbom_cache_block_size () = arch_bits_of_int64 !P.zicbom_cache_block_size_ref +let zicboz_cache_block_size () = arch_bits_of_int64 !P.zicboz_cache_block_size_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 b55edfbb1..012becf05 100644 --- a/ocaml_emulator/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml @@ -57,7 +57,8 @@ let rom_base = 0x00001000L;; (* Spike::DEFAULT_RSTVEC *) let dram_size_ref = ref (Int64.(shift_left 64L 20)) -let cache_block_size_ref = ref (Int64.(64L)) +let zicbom_cache_block_size_ref = ref (Int64.(64L)) +let zicboz_cache_block_size_ref = ref (Int64.(64L)) type mem_region = { addr : Int64.t; @@ -146,8 +147,11 @@ 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 b = - cache_block_size_ref := Int64.(Int64.of_int b) +let set_zicbom_cache_block_size b = + zicbom_cache_block_size_ref := Int64.(Int64.of_int b) + +let set_zicboz_cache_block_size b = + zicboz_cache_block_size_ref := Int64.(Int64.of_int b) let make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) try diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index 6b828445c..624544b0e 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -59,9 +59,12 @@ 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", - Arg.Int PI.set_cache_block_size, - " size of cache block size to use (in bytes)"); + ("-zicbom-cache-block-size", + Arg.Int PI.set_zicbom_cache_block_size, + " size of cache block size for zicbom to use (in bytes)"); + ("-zicboz-cache-block-size", + Arg.Int PI.set_zicboz_cache_block_size, + " size of cache block size for zicboz to use (in bytes)"); ("-report-arch", Arg.Unit report_arch, " report model architecture (RV32 or RV64)");