Use different cache block size for zicbom and zicboz operations

Update disasm for cbo.* instructions

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()
+{ return rv_zicbom_cache_block_size; }
+
+mach_bits plat_zicboz_cache_block_size()
+{ return rv_zicboz_cache_block_size; }
 
 // Provides entropy for the scalar cryptography extension.
 mach_bits plat_get_16_random_bits()

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

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) {

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

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;

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

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

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

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

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) {

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)

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

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

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

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