Implement Zicbom, Zicboz (cbo.flush, cbo.inval, cbo.zero)

Note that Zicbop (prefetch hints) does not need to be implemented because all it does is label some existing base instructions as prefetch hints.

Also I have not wired up the enable flags to the emulators because it is rather tedious (and will hopefully be replaced by riscv-config at some point).

Author: Tim Hutt

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

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

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

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

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

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

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`

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`

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

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)