Add support for cmo extensions except prefetch.* instructions

(They will be overlapped by ORI instruciton).

Makefile

@@ -41,6 +41,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbkx.sail
 
 SAIL_DEFAULT_INST += riscv_insts_zicond.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

@@ -134,6 +134,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}
 };
 
@@ -216,6 +217,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"
@@ -245,6 +247,7 @@ char *process_args(int argc, char **argv)
 #ifdef SAILCOV
                     "c:"
 #endif
+                    "B:"
                          , options, NULL);
     if (c == -1) break;
     switch (c) {
@@ -345,6 +348,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

@@ -177,6 +177,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

@@ -169,6 +169,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_addr_checks.sail

@@ -116,7 +116,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 : xlenbits)
          -> Ext_DataAddr_Check(ext_data_addr_error) =
   let addr = X(base) + offset in
   Ext_DataAddr_OK(addr)

model/riscv_csr_map.sail

@@ -113,6 +113,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"
@@ -159,6 +161,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_aext.sail

@@ -127,7 +127,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
     /* Get the address, X(rs1) (no offset).
      * Extensions might perform additional checks on address validity.
      */
-    match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
+    match ext_data_get_addr(rs1, zeros(), Read(Data), EXTZ(size_bits(width))) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
         let aligned : bool =
@@ -188,7 +188,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
       /* Get the address, X(rs1) (no offset).
        * Extensions might perform additional checks on address validity.
        */
-      match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
+      match ext_data_get_addr(rs1, zeros(), Write(Data), EXTZ(size_bits(width))) {
         Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
         Ext_DataAddr_OK(vaddr) => {
           let aligned : bool =
@@ -278,7 +278,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     /* Get the address, X(rs1) (no offset).
      * Some extensions perform additional checks on address validity.
      */
-    match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) {
+    match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), EXTZ(size_bits(width))) {
       Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
       Ext_DataAddr_OK(vaddr) => {
         match translateAddr(vaddr, ReadWrite(Data, Data)) {

model/riscv_insts_base.sail

@@ -388,7 +388,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
   let offset : xlenbits = EXTS(imm);
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Read(Data), width) {
+  match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
@@ -444,7 +444,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
   let offset : xlenbits = EXTS(imm);
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Write(Data), width) {
+  match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)

model/riscv_insts_fext.sail

@@ -377,7 +377,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
   let offset : xlenbits = EXTS(imm);
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Read(Data), width) {
+  match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)
@@ -443,7 +443,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
   let (aq, rl, con) = (false, false, false);
   /* Get the address, X(rs1) + offset.
      Some extensions perform additional checks on address validity. */
-  match ext_data_get_addr(rs1, offset, Write(Data), width) {
+  match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) {
     Ext_DataAddr_Error(e)  => { ext_handle_data_check_error(e); RETIRE_FAIL },
     Ext_DataAddr_OK(vaddr) =>
       if   check_misaligned(vaddr, width)

model/riscv_insts_zicbom.sail

@@ -0,0 +1,73 @@
+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 : (regidx, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_clean_inval(rs1, cbop) = {
+  let rs1_val = X(rs1);
+  let cache_block_size = plat_cache_block_size();
+  let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1));
+  let offset = begin_addr - rs1_val;
+  match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) {
+    Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
+    Ext_DataAddr_OK(vaddr) => {
+      let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
+        TR_Address(paddr, _) => pmpCheck_xlen(paddr, cache_block_size, Read(Data), cur_privilege),
+        TR_Failure(e, _) => Some(e)
+      };
+      match res {
+        None() => RETIRE_SUCCESS,  // do nothing for cbop currently
+        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 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(cbop) => process_clean_inval(rs1, cbop)
+  }
+}

model/riscv_insts_zicboz.sail

@@ -0,0 +1,55 @@
+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 : (regidx) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
+function process_cbo_zero(rs1) = {
+  let rs1_val = X(rs1);
+  let cache_block_size = plat_cache_block_size();
+  let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1));
+  let offset = begin_addr - rs1_val;
+  index : xlenbits = zeros();
+  failed : bool = false;
+  match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) {
+    Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true },
+    Ext_DataAddr_OK(vaddr) =>
+      while (index <_u cache_block_size) & (failed == false) do {
+        let addr = vaddr + index;
+        match translateAddr(addr, 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) => index = index + EXTZ(0b1),
+                  MemValue(false) => internal_error(__FILE__, __LINE__, "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)) = {
+  if get_envcfg_cbze(cur_privilege) then
+    process_cbo_zero(rs1)
+  else {
+    handle_illegal();
+    RETIRE_FAIL
+  }
+}

model/riscv_insts_zicsr.sail

@@ -98,6 +98,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()),
 
@@ -145,6 +146,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(),
@@ -186,6 +188,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) },
@@ -233,6 +236,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

@@ -88,6 +88,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