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

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