From 3e05453f5c8d48f57d25ce2e129f36dfeb395a6e Mon Sep 17 00:00:00 2001 From: liweiwei Date: Sat, 18 Dec 2021 11:34:39 +0800 Subject: [PATCH] add support for cmo extension --- Makefile | 3 + c_emulator/riscv_platform.c | 3 + c_emulator/riscv_platform.h | 2 + c_emulator/riscv_platform_impl.c | 2 + c_emulator/riscv_platform_impl.h | 2 + c_emulator/riscv_sim.c | 13 +++ handwritten_support/0.11/riscv_extras.lem | 4 + .../0.11/riscv_extras_sequential.lem | 4 + handwritten_support/riscv_extras.lem | 4 + .../riscv_extras_sequential.lem | 4 + model/riscv_csr_map.sail | 4 + model/riscv_insts_zicbom.sail | 81 +++++++++++++++++++ model/riscv_insts_zicboz.sail | 57 +++++++++++++ model/riscv_insts_zicsr.sail | 4 + model/riscv_platform.sail | 2 + model/riscv_pmp_control.sail | 10 ++- model/riscv_sys_control.sail | 5 ++ model/riscv_sys_regs.sail | 28 +++++++ model/riscv_types.sail | 2 + ocaml_emulator/platform.ml | 2 + ocaml_emulator/platform_impl.ml | 5 ++ ocaml_emulator/riscv_ocaml_sim.ml | 3 + 22 files changed, 241 insertions(+), 3 deletions(-) create mode 100644 model/riscv_insts_zicbom.sail create mode 100644 model/riscv_insts_zicboz.sail diff --git a/Makefile b/Makefile index 5f7f94bf7..513f66061 100644 --- a/Makefile +++ b/Makefile @@ -30,6 +30,9 @@ SAIL_DEFAULT_INST += riscv_insts_zbs.sail SAIL_DEFAULT_INST += riscv_insts_zkn.sail SAIL_DEFAULT_INST += riscv_insts_zks.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 diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index 2572dbcd4..17ad17faa 100644 --- a/c_emulator/riscv_platform.c +++ b/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(); } diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 5335a90bb..98efde81e 100644 --- a/c_emulator/riscv_platform.h +++ b/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(); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index b1504a727..1cadc985e 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/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 diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 165fb94d7..b686578d2 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/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); diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index a2d1bce2e..4601e6da6 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -131,6 +131,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} }; @@ -213,6 +214,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" @@ -241,6 +243,7 @@ char *process_args(int argc, char **argv) #ifdef SAILCOV "c:" #endif + "B:" , options, NULL); if (c == -1) break; switch (c) { @@ -337,6 +340,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; diff --git a/handwritten_support/0.11/riscv_extras.lem b/handwritten_support/0.11/riscv_extras.lem index 2509057e6..3e038115a 100644 --- a/handwritten_support/0.11/riscv_extras.lem +++ b/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` diff --git a/handwritten_support/0.11/riscv_extras_sequential.lem b/handwritten_support/0.11/riscv_extras_sequential.lem index 0c236515f..d841f615d 100644 --- a/handwritten_support/0.11/riscv_extras_sequential.lem +++ b/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` diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 93f19ab7f..1cf0714a7 100644 --- a/handwritten_support/riscv_extras.lem +++ b/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` diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index ddfe74f93..ca36eb931 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/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` diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 31872d3f1..03b9741e1 100644 --- a/model/riscv_csr_map.sail +++ b/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" diff --git a/model/riscv_insts_zicbom.sail b/model/riscv_insts_zicbom.sail new file mode 100644 index 000000000..6969793a2 --- /dev/null +++ b/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) + } +} + diff --git a/model/riscv_insts_zicboz.sail b/model/riscv_insts_zicboz.sail new file mode 100644 index 000000000..c8ac6ec45 --- /dev/null +++ b/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 + } +} + diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 518396f91..709758a0f 100644 --- a/model/riscv_insts_zicsr.sail +++ b/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()) }, diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index ea27f48eb..c9e808e97 100644 --- a/model/riscv_platform.sail +++ b/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 diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 669725b5b..6b21a3846 100644 --- a/model/riscv_pmp_control.sail +++ b/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)); diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6204ae59e..ffa4ce038 100644 --- a/model/riscv_sys_control.sail +++ b/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 diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 98e5019f4..1c2d79546 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -198,6 +198,10 @@ function haveZknh() -> bool = true function haveZkne() -> bool = true function haveZknd() -> bool = true +/* Cache Management Operations extension support. */ +function haveZicbom() -> bool = true +function haveZicboz() -> bool = true + bitfield Mstatush : bits(32) = { MBE : 5, SBE : 4 @@ -813,3 +817,27 @@ function read_seed_csr() -> xlenbits = { /* Writes to the seed CSR are ignored */ function write_seed_csr () -> option(xlenbits) = None() + +bitfield Envcfg : xlenbits = { + CBZE : 7, + CBCFE : 6, + CBIE : 5 .. 4 +} +register senvcfg : Envcfg +register menvcfg : Envcfg + +/* treat 0b10 as 0b00: Partially, the encoding was set up so that bit [4] was an + * "enable" bit, and bit [5] was an "operation" bit. So if bit [4] was zero, + * bit [5] is a don't care. + */ +function legalize_envcfg_cbie(o : bits(2), v : bits(2)) -> bits(2) = match (v) { + 0b10 => 0b00, + _ => v +} + +function legalize_envcfg(o : Envcfg, v : xlenbits) -> Envcfg = { + let c = update_CBZE(o, [v[7]]); + let c = update_CBCFE(c, [v[6]]); + let c = update_CBIE(c, legalize_envcfg_cbie(o.CBIE(), v[5 .. 4])); + c +} diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 08dce73bd..543ba7a64 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -390,6 +390,8 @@ enum amoop = {AMOSWAP, AMOADD, AMOXOR, AMOAND, AMOOR, AMOMIN, AMOMAX, AMOMINU, AMOMAXU} /* AMO ops */ enum csrop = {CSRRW, CSRRS, CSRRC} /* CSR ops */ +enum cbop_zicbom = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL} /* zicbom ops*/ + enum brop_zba = {RISCV_SH1ADD, RISCV_SH2ADD, RISCV_SH3ADD} enum brop_zbb = {RISCV_ANDN, RISCV_ORN, RISCV_XNOR, RISCV_MAX, diff --git a/ocaml_emulator/platform.ml b/ocaml_emulator/platform.ml index ccf487589..8ffff87fd 100644 --- a/ocaml_emulator/platform.ml +++ b/ocaml_emulator/platform.ml @@ -90,6 +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 clint_base () = arch_bits_of_int64 P.clint_base let clint_size () = arch_bits_of_int64 P.clint_size diff --git a/ocaml_emulator/platform_impl.ml b/ocaml_emulator/platform_impl.ml index 39de43776..b55edfbb1 100644 --- a/ocaml_emulator/platform_impl.ml +++ b/ocaml_emulator/platform_impl.ml @@ -57,6 +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)) + type mem_region = { addr : Int64.t; size : Int64.t @@ -144,6 +146,9 @@ 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 make_dtb dts = (* Call the dtc compiler, assumed to be at /usr/bin/dtc *) try let cmd = Printf.sprintf "%s -I dts" !dtc_path in diff --git a/ocaml_emulator/riscv_ocaml_sim.ml b/ocaml_emulator/riscv_ocaml_sim.ml index fb06c407e..d242ffe37 100644 --- a/ocaml_emulator/riscv_ocaml_sim.ml +++ b/ocaml_emulator/riscv_ocaml_sim.ml @@ -55,6 +55,9 @@ 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 B)"); ("-report-arch", Arg.Unit report_arch, " report model architecture (RV32 or RV64)");