add support for cmo extension

Makefile

@@ -36,6 +36,9 @@ SAIL_DEFAULT_INST += riscv_insts_zks.sail
 SAIL_DEFAULT_INST += riscv_insts_zbkb.sail
 SAIL_DEFAULT_INST += riscv_insts_zbkx.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

@@ -48,6 +48,9 @@ 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; }
+
 // Provides entropy for the scalar cryptography extension.
 mach_bits plat_get_16_random_bits()
 { return rv_16_random_bits(); }

c_emulator/riscv_platform.h

@@ -19,6 +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);
+
 // Provides entropy for the scalar cryptography extension.
 mach_bits plat_get_16_random_bits();
 

c_emulator/riscv_platform_impl.c

@@ -20,6 +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);
+
 // Provides entropy for the scalar cryptography extension.
 uint64_t rv_16_random_bits(void) {
   // This function can be changed to support deterministic sequences of

c_emulator/riscv_platform_impl.h

@@ -23,6 +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;
+
 // Provides entropy for the scalar cryptography extension.
 extern uint64_t rv_16_random_bits(void);
 

c_emulator/riscv_sim.c

@@ -133,6 +133,7 @@ static struct option options[] = {
 #ifdef SAILCOV
   {"sailcov-file",                required_argument, 0, 'c'},
 #endif
+  {"cache-block-size",            required_argument, 0, 'B'},
   {0, 0, 0, 0}
 };
 
@@ -215,6 +216,7 @@ char *process_args(int argc, char **argv)
 {
   int c;
   uint64_t ram_size = 0;
+  uint64_t block_size = 0;
   while(true) {
     c = getopt_long(argc, argv,
                     "a"
@@ -244,6 +246,7 @@ char *process_args(int argc, char **argv)
 #ifdef SAILCOV
                     "c:"
 #endif
+                    "B:"
                          , options, NULL);
     if (c == -1) break;
     switch (c) {
@@ -344,6 +347,16 @@ char *process_args(int argc, char **argv)
       sailcov_file = strdup(optarg);
       break;
 #endif
+    case 'B':
+      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;
+      } else {
+        fprintf(stderr, "invalid cache-block-size '%s' provided.\n", optarg);
+        exit(1);
+      }
+      break;
     case '?':
       print_usage(argv[0], 1);
       break;

handwritten_support/0.11/riscv_extras.lem

@@ -107,6 +107,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 : 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_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`

handwritten_support/0.11/riscv_extras_sequential.lem

@@ -99,6 +99,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 : 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_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`

handwritten_support/riscv_extras.lem

@@ -175,6 +175,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 : 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_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`

handwritten_support/riscv_extras_sequential.lem

@@ -167,6 +167,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 : 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_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/riscv_csr_map.sail

@@ -111,6 +111,8 @@ mapping clause csr_name_map = 0x143  <-> "stval"
 mapping clause csr_name_map = 0x144  <-> "sip"
 /* supervisor protection and translation */
 mapping clause csr_name_map = 0x180  <-> "satp"
+/* supervisor envcfg */
+mapping clause csr_name_map = 0x10A  <-> "senvcfg"
 /* machine information registers */
 mapping clause csr_name_map = 0xF11  <-> "mvendorid"
 mapping clause csr_name_map = 0xF12  <-> "marchid"
@@ -157,6 +159,8 @@ mapping clause csr_name_map = 0xB00  <-> "mcycle"
 mapping clause csr_name_map = 0xB02  <-> "minstret"
 mapping clause csr_name_map = 0xB80  <-> "mcycleh"
 mapping clause csr_name_map = 0xB82  <-> "minstreth"
+/* machine envcfg */
+mapping clause csr_name_map = 0x30A  <-> "menvcfg"
 /* TODO: other hpm counters and events */
 /* trigger/debug */
 mapping clause csr_name_map = 0x7a0  <-> "tselect"

model/riscv_insts_zicbom.sail

@@ -0,0 +1,81 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the Zicbom extension */
+
+
+/* ****************************************************************** */
+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() ^ reg_name(rs1)
+
+val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(vaddr, width, clean, inval) = {
+  match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) {
+    Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) => {
+      let data: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
+        TR_Address(paddr, _) =>  pmpCheck_xlen(paddr, width, Read(Data), cur_privilege),
+        TR_Failure(e, _) => Some(e)
+      };
+      match data {
+        None() => RETIRE_SUCCESS,
+        Some(e) => {
+          match (e) {
+            E_Load_Access_Fault() => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL },
+            E_Load_Page_Fault() => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }
+          }
+        }
+      }
+    }
+  }
+}
+
+function cbo_clean_flush_enable(p : Privilege) -> bool = {
+   ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | ((p == User) & (senvcfg.CBCFE() == 0b0)))
+}
+
+function cbop_for_cbo_inval(p : Privilege) -> option(cbop_zicbom) = {
+  let illegal = ((p != Machine) & (menvcfg.CBIE() == 0b00)) |
+                ((p == User) & (senvcfg.CBIE() == 0b00));
+  let flush = ((p != Machine) & (menvcfg.CBIE() == 0b01)) |
+              ((p == User) & (senvcfg.CBIE() == 0b01));
+  if illegal then None()
+  else if flush then Some(CBO_FLUSH)
+  else Some(CBO_INVAL)
+}
+
+function clause execute(RISCV_ZICBOM(cbop, rs1)) = {
+  let rs1_val = X(rs1);
+  let cache_block_size = plat_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) {
+    (CBO_CLEAN, true) => Some(CBO_CLEAN),
+    (CBO_CLEAN, false) => None(),
+    (CBO_FLUSH, true) => Some(CBO_FLUSH),
+    (CBO_FLUSH, false) => None(),
+    (CBO_INVAL, _) => cbop_for_cbo_inval(cur_privilege)
+  };
+  match final_op {
+    None() => { handle_illegal(); RETIRE_FAIL },
+    Some(CBO_CLEAN) => process_clean_inval(vaddr, cache_block_size, true, false),
+    Some(CBO_FLUSH) => process_clean_inval(vaddr, cache_block_size, true, true),
+    Some(CBO_INVAL) => process_clean_inval(vaddr, cache_block_size, false, true)
+  }
+}
+

model/riscv_insts_zicboz.sail

@@ -0,0 +1,57 @@
+/* ****************************************************************** */
+/* This file specifies the instructions in the Zicboz extension */
+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() ^ reg_name(rs1)
+
+function get_envcfg_cbze(p : Privilege) -> bool = {
+  ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | ((p == User) & (senvcfg.CBZE() == 0b0)))
+}
+
+val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_cbo_zero(vaddr, width) = {
+  offset : xlenbits = zeros();
+  failed : bool = false;
+  while (offset <_u width) & (failed == false) do {
+    let addr = vaddr + offset;
+    match ext_data_get_addr(zeros(), addr, Write(Data), BYTE) {
+      Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true },
+      Ext_DataAddr_OK(vaddr) =>
+        match translateAddr(vaddr, Write(Data)) {
+          TR_Failure(e, _) => { handle_mem_exception(vaddr, e); failed = true },
+          TR_Address(paddr, _) => {
+            let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
+            match (eares) {
+              MemException(e) => { handle_mem_exception(vaddr, e); failed = true },
+              MemValue(_) => {
+                let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, zeros(), false, false, false);
+                match (res) {
+                  MemValue(true) => offset = offset + EXTZ(0b1),
+                  MemValue(false) => internal_error("store got false from mem_write_value"),
+                  MemException(e) => { handle_mem_exception(vaddr, e); failed = true }
+                }
+              }
+            }
+          }
+        }
+    };
+  };
+  if failed then RETIRE_FAIL
+  else RETIRE_SUCCESS
+}
+
+function clause execute(RISCV_ZICBOZ(rs1)) = {
+  let rs1_val = X(rs1);
+  let cache_block_size = plat_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)
+  else {
+    handle_illegal();
+    RETIRE_FAIL
+  }
+}
+

model/riscv_insts_zicsr.sail

@@ -96,6 +96,7 @@ function readCSR csr : csreg -> xlenbits = {
     (0x304,  _) => mie.bits(),
     (0x305,  _) => get_mtvec(),
     (0x306,  _) => EXTZ(mcounteren.bits()),
+    (0x30A,  _) => menvcfg.bits(),
     (0x310, 32) => mstatush.bits(),
     (0x320,  _) => EXTZ(mcountinhibit.bits()),
 
@@ -143,6 +144,7 @@ function readCSR csr : csreg -> xlenbits = {
     (0x104,  _) => lower_mie(mie, mideleg).bits(),
     (0x105,  _) => get_stvec(),
     (0x106,  _) => EXTZ(scounteren.bits()),
+    (0x10A,  _) => senvcfg.bits(),
     (0x140,  _) => sscratch,
     (0x141,  _) => get_xret_target(Supervisor) & pc_alignment_mask(),
     (0x142,  _) => scause.bits(),
@@ -184,6 +186,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x304,  _) => { mie = legalize_mie(mie, value); Some(mie.bits()) },
     (0x305,  _) => { Some(set_mtvec(value)) },
     (0x306,  _) => { mcounteren = legalize_mcounteren(mcounteren, value); Some(EXTZ(mcounteren.bits())) },
+    (0x30A,  _) => { menvcfg = legalize_envcfg(menvcfg, value); Some(menvcfg.bits()) },
     (0x310, 32) => { Some(mstatush.bits()) }, // ignore writes for now
     (0x320,  _) => { mcountinhibit = legalize_mcountinhibit(mcountinhibit, value); Some(EXTZ(mcountinhibit.bits())) },
     (0x340,  _) => { mscratch = value; Some(mscratch) },
@@ -231,6 +234,7 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = {
     (0x104,  _) => { mie = legalize_sie(mie, mideleg, value); Some(mie.bits()) },
     (0x105,  _) => { Some(set_stvec(value)) },
     (0x106,  _) => { scounteren = legalize_scounteren(scounteren, value); Some(EXTZ(scounteren.bits())) },
+    (0x10A,  _) => { senvcfg = legalize_envcfg(senvcfg, value); Some(senvcfg.bits()) },
     (0x140,  _) => { sscratch = value; Some(sscratch) },
     (0x141,  _) => { Some(set_xret_target(Supervisor, value)) },
     (0x142,  _) => { scause->bits() = value; Some(scause.bits()) },

model/riscv_platform.sail

@@ -86,6 +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
+
 /* 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

model/riscv_pmp_control.sail

@@ -149,10 +149,8 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_acce
 }
 
 /* priority checks */
-
-function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
+function pmpCheck_xlen (addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege)
                   -> option(ExceptionType) = {
-  let width : xlenbits = to_bits(sizeof(xlen), width);
   let check : bool =
   match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) {
     PMP_Success  => true,
@@ -233,6 +231,12 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
   }
 }
 
+function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
+                  -> option(ExceptionType) = {
+  let width : xlenbits = to_bits(sizeof(xlen), width);
+  pmpCheck_xlen(addr, width, acc, priv)
+}
+
 function init_pmp() -> unit = {
   pmp0cfg  = update_A(pmp0cfg,  pmpAddrMatchType_to_bits(OFF));
   pmp1cfg  = update_A(pmp1cfg,  pmpAddrMatchType_to_bits(OFF));

model/riscv_sys_control.sail

@@ -89,6 +89,7 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x304 => p == Machine, // mie
     0x305 => p == Machine, // mtvec
     0x306 => p == Machine & haveUsrMode(), // mcounteren
+    0x30a => p == Machine, // menvcfg
     0x310 => p == Machine & (sizeof(xlen) == 32), // mstatush
     0x320 => p == Machine, // mcountinhibit
     /* machine mode: trap handling */
@@ -138,6 +139,8 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool =
     0x105 => haveSupMode() & (p == Machine | p == Supervisor), // stvec
     0x106 => haveSupMode() & (p == Machine | p == Supervisor), // scounteren
 
+    0x10a => haveSupMode() & (p == Machine | p == Supervisor), // senvcfg
+
     /* supervisor mode: trap handling */
     0x140 => haveSupMode() & (p == Machine | p == Supervisor), // sscratch
     0x141 => haveSupMode() & (p == Machine | p == Supervisor), // sepc
@@ -596,6 +599,8 @@ function init_sys() -> unit = {
   minstret           = EXTZ(0b0);
   minstret_written   = false;
 
+  menvcfg->bits() = EXTZ(0b0);
+
   init_pmp();
 
   // log compatibility with spike