add support for cmo extension

[liweiwei90]

add support for cmo extension:

• add parameter for cache block size
• add cbo.zero to zero the cache block
• add cbo.inval/flush/clean to do envcfg csr and memory access check
• add prefetch* to only do the address-translation

[jrtc27]

Various initial feedback; generally only commented on the first instance of something even when it applies multiple times, so please check for other instances of things I've said, especially when it comes to code formatting

[liweiwei90]

Various initial feedback; generally only commented on the first instance of something even when it applies multiple times, so please check for other instances of things I've said, especially when it comes to code formatting

OK, I'll try to seperate the three extensions.

[allenjbaum]

Thanks for an incredibly quick and thorough review. But, at one point you say there shouldn't be random spaces, but the guidelines said you can add them to align things vertically to make them easier to understand. Which would be fine if in this case he added a couple more extra spaces to make the expressions actually line up. Do I have that correct?

…

On Fri, Dec 17, 2021 at 10:20 PM Jessica Clarke ***@***.***> wrote: ***@***.**** commented on this pull request. Various initial feedback; generally only commented on the first instance of something even when it applies multiple times, so please check for other instances of things I've said, especially when it comes to code formatting ------------------------------ In Makefile <#137 (comment)>: > @@ -29,6 +29,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbc.sail 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_cmoext.sail As you can see from the big block above, each Zfoo gets its own zfoo.sail file, so Zicbom, Zicbop and Zicboz should get their own files named accordingly ------------------------------ In c_emulator/riscv_platform_impl.c <#137 (comment)>: > @@ -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(0x10); 16 bytes is a strange default, 64 seems like a more common cache line size to default to ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ Not an extension name ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ + + +/* ****************************************************************** */ +union clause ast = RISCV_CBO : (cbop, regidx) Should be specific to Zcbop ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ + + +/* ****************************************************************** */ +union clause ast = RISCV_CBO : (cbop, regidx) + +mapping encdec_cbop : cbop <-> bits(12) = { + CBO_CLEAN <-> 0b000000000001, + CBO_FLUSH <-> 0b000000000010, + CBO_INVAL <-> 0b000000000000, + CBO_ZERO <-> 0b000000000100 CBO_ZERO is part of a separate extension to the other three so should get its own ast clause ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ + + +/* ****************************************************************** */ +union clause ast = RISCV_CBO : (cbop, regidx) + +mapping encdec_cbop : cbop <-> bits(12) = { + CBO_CLEAN <-> 0b000000000001, + CBO_FLUSH <-> 0b000000000010, + CBO_INVAL <-> 0b000000000000, + CBO_ZERO <-> 0b000000000100 +} + +mapping clause encdec = RISCV_CBO(cbop, rs1) These need guards on the extensions being enabled ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval", + CBO_ZERO <-> "cbo.zero" +} + +mapping clause assembly = RISCV_CBO(cbop, rs1) + <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + +val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +function write_zero(paddr, width) = { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); + match (res) { + MemValue(true) => { + if(unsigned(width) > 8) then + write_zero(paddr + 8, width - 8) Use a loop when you want a loop ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +mapping clause encdec = RISCV_CBO(cbop, rs1) + <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 + +mapping cbo_mnemonic : cbop <-> string = { + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval", + CBO_ZERO <-> "cbo.zero" +} + +mapping clause assembly = RISCV_CBO(cbop, rs1) + <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + +val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +function write_zero(paddr, width) = { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); Why 8? Either do byte by byte or do max_mem_access at a time (which is 16), but don't hard-code an arbitrary word size using magic constants. Also use zeros() rather than to_bits(N, 0). Finally, this is broken if width isn't divisible by 8 (or whatever word size is used), so there should be an assertion to ensure that never happens if it's not expected to (i.e., since everything's a power of two, that it's impossible to configure the cache block size as less than the word size), or it should be handled gracefully (which is one reason to make the model simple and just do a byte-by-byte loop). ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +mapping cbo_mnemonic : cbop <-> string = { + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval", + CBO_ZERO <-> "cbo.zero" +} + +mapping clause assembly = RISCV_CBO(cbop, rs1) + <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + +val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +function write_zero(paddr, width) = { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); + match (res) { + MemValue(true) => { + if(unsigned(width) > 8) then Spaces after if, and no parens needed ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); + match (res) { + MemValue(true) => { + if(unsigned(width) > 8) then + write_zero(paddr + 8, width - 8) + else + MemValue(true) + }, + MemValue(false) => MemValue(false), + MemException(e) => MemException(e) + } +} + +val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_cbo_zero(vaddr, width) = { + match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) { The first argument should be rs1 for the instruction, and you have a bunch of the same bug so I'm only commenting on this one. And BYTE is definitely wrong, it needs to match the exact size of the write you're performing, you can't be lazy like with paging and probe a single byte when writing a whole page, it has to be exact. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } +} + +val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_cbo_zero(vaddr, width) = { + match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = write_zero(paddr, width); What if the block size is high enough that it covers multiple pages? ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = write_zero(paddr, width); + match (res) { + MemValue(true) => RETIRE_SUCCESS, + MemValue(false) => internal_error("store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + } + } + } + } + } +} + +union translation_check = { So... option(ExceptionType) ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + match translateAddr(vaddr, Execute()) { + TR_Failure(e, _) => TransTrap(e), + TR_Address(paddr, _) => TransSuccess() + } + }; + match fetch { + TransSuccess() => RETIRE_SUCCESS, + TransTrap(fe) => + match (le, se, fe) { + (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_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 }, + (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL } Don't put spaces before commas like that ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } + } + } +} + +union translation_check = { + TransTrap : ExceptionType, + TransSuccess : unit +} + +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) = { + let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) { + Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()), What are all these uses of exception 14 for? You need to pass the ext_data_addr_error to ext_handle_data_check_error and return RETIRE_FAIL if you get an Ext_DataAddr_Error that you decide to honour, not some random reserved exception cause. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_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 }, + (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL } + } + } + } + } + } + } +} + +function check_clean_flush(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | This variable is pointless ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) Just put the second bit in and avoid the EXTZ ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +} + +function check_clean_flush(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | + ((p == User) & (senvcfg.CBCFE() == 0b0))); + ret +} + +function check_inval(p : Privilege) -> bits(2) = { + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | + ((p == User) & (senvcfg.CBIE() == 0b00)); + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) + else EXTZ(0b11) EXTZ is a no-op ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | + ((p == User) & (senvcfg.CBIE() == 0b00)); + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); Give the variables descriptive names, e.g. trap and flush ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_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 }, + (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL } + } + } + } + } + } + } +} + +function check_clean_flush(p : Privilege) -> bool = { These names should probably be more obviously scoped to cache operations and more clearly state that they're about "what operation is this instruction mapped to"; check_foo sounds like an assertion ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } + } + } + } +} + +function check_clean_flush(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | + ((p == User) & (senvcfg.CBCFE() == 0b0))); + ret +} + +function check_inval(p : Privilege) -> bits(2) = { + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | Types shouldn't be needed ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) + else EXTZ(0b11) +} + +function check_zero(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | + ((p == User) & (senvcfg.CBZE() == 0b0))); + ret +} + +function clause execute(RISCV_CBO(cbop, rs1)) = { + let rs1_val = X(rs1); + let cache_block_size : xlenbits = plat_cache_block_size() ; No random spaces ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +} + +function check_zero(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | + ((p == User) & (senvcfg.CBZE() == 0b0))); + ret +} + +function clause execute(RISCV_CBO(cbop, rs1)) = { + let rs1_val = X(rs1); + let cache_block_size : xlenbits = plat_cache_block_size() ; + let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1)); + match cbop { + CBO_CLEAN => { + if (check_clean_flush(cur_privilege)) then + /* perform clean*/ Space before the *, but also, this comment is a waste of time ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) + else EXTZ(0b11) +} + +function check_zero(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | + ((p == User) & (senvcfg.CBZE() == 0b0))); + ret +} + +function clause execute(RISCV_CBO(cbop, rs1)) = { + let rs1_val = X(rs1); + let cache_block_size : xlenbits = plat_cache_block_size() ; + let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1)); + match cbop { This seems like it'd be nicer as two steps: 1. Take the instruction's operation and map it to option(operation) based on the CSRs 2. Treat that operation as the actual operation to perform (with None() being handle_illegal) Also avoids all the magic constants being returned from functions and read here (I realise it's repurposing the encodings of the CSRs, but that's not the most friendly way of writing it) ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +} + +mapping clause encdec = RISCV_PREFETCH(op, rs1, offset) + <-> offset @ encdec_prefetch(op) @ rs1 @ 0b110 @ 0b00000 @ 0b0010011 + +mapping pre_mnemonic : preop <-> string = { + PREFETCH_I <-> "prefetch.i", + PREFETCH_R <-> "prefetch.r", + PREFETCH_W <-> "prefetch.w" +} + +mapping clause assembly = RISCV_PREFETCH(op, rs1, offset) + <-> pre_mnemonic(op) ^ spc() ^ hex_bits_12(offset @ 0b00000) ^ "(" ^ reg_name(rs1) ^ ")" + +function clause execute(RISCV_PREFETCH(preop, rs1, offset)) = { + /* do nothing other than translate_address for prefetch.i/r/w */ Why do we even bother doing that? They're just hints, they can be entirely nop'ed out in the model like any other hint. Which is already the case, given they're ORI instructions, and base.sail gets included before cmoext.sail so the real ORIs will take precedence and this code is entirely dead. Especially since this is actually wrong, due to translateAddr having the side-effect of (if enabled instead of trapping for software emulation) atomically updating accessed and dirty bits as needed, which is specifically not performed for prefetch. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + TR_Address(paddr, _) => RETIRE_SUCCESS + } + } + }, + PREFETCH_R => { + match ext_data_get_addr(rs1, EXTS(offset @ 0b00000), Read(Data), BYTE) { + Ext_DataAddr_Error(e) => RETIRE_SUCCESS, + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => RETIRE_SUCCESS, + TR_Address(paddr, _) => RETIRE_SUCCESS + } + } + } + } +} Make sure every line has a terminating newline character (required by POSIX for a file to be a valid text file) ------------------------------ In model/riscv_sys_control.sail <#137 (comment)>: > @@ -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 Space after the // ------------------------------ In model/riscv_sys_regs.sail <#137 (comment)>: > @@ -813,3 +813,18 @@ 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 + +function legalize_envcfg(c : Envcfg, v : xlenbits) -> Envcfg = { + let c = update_CBZE(c, [v[7]]); + let c = update_CBCFE(c, [v[6]]); + let c = update_CBIE(c, v[5 .. 4]); Doesn't this need to legalise 10? ------------------------------ In model/riscv_types.sail <#137 (comment)>: > +enum cbop = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL, CBO_ZERO} /* cbo ops*/ +enum preop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* prefetch ops*/ Follow the convention below; put them in a separate block and include the extension names ------------------------------ In ocaml_emulator/platform_impl.ml <#137 (comment)>: > @@ -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)) Ok so this one defaults to 64 as I'd expect, unlike the C model ------------------------------ In c_emulator/riscv_sim.c <#137 (comment)>: > @@ -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 & 7) == 0) && (block_size < 4096)) { I can't obviously find either of these restrictions in the spec; where have these come from? 4096 seems pretty unproblematic, that's a whole page, things just get awkward when you cover multiple pages, but the PMP already makes that an issue. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } +} + +union translation_check = { + TransTrap : ExceptionType, + TransSuccess : unit +} + +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) = { + let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) { + Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()), + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Read(Data)) { How does invalidate interact with the dirty bit of page table entries? Just translating a read won't dirty the page, but surely an invalidate needs to dirty the page if actually invalidating rather than just cleaning/flushing? Though whether it's "only dirty if the cache line is dirty" or "always dirty even if there's nothing to write back" I don't know. I can only see discussion of accessed and dirty bits for prefetch and zeroing, not management instruction. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } +} + +union translation_check = { + TransTrap : ExceptionType, + TransSuccess : unit +} + +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) = { + let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) { + Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()), + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Read(Data)) { (The answer to that affects whether or not you can clean this up by just hoisting all three load, store and fetch calculations and matching on them all at the same time, which would flatten this function somewhat) — Reply to this email directly, view it on GitHub <#137 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJWIR7QEM5BHJMGYTKTURQR4HANCNFSM5KKGQEIA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[allenjbaum]

I am concerned that jrtc27 has pointed out things that are bugs in the code, yet there are no tests that cover those. Shouldn't there be?

…

On Fri, Dec 17, 2021 at 10:20 PM Jessica Clarke ***@***.***> wrote: ***@***.**** commented on this pull request. Various initial feedback; generally only commented on the first instance of something even when it applies multiple times, so please check for other instances of things I've said, especially when it comes to code formatting ------------------------------ In Makefile <#137 (comment)>: > @@ -29,6 +29,7 @@ SAIL_DEFAULT_INST += riscv_insts_zbc.sail 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_cmoext.sail As you can see from the big block above, each Zfoo gets its own zfoo.sail file, so Zicbom, Zicbop and Zicboz should get their own files named accordingly ------------------------------ In c_emulator/riscv_platform_impl.c <#137 (comment)>: > @@ -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(0x10); 16 bytes is a strange default, 64 seems like a more common cache line size to default to ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ Not an extension name ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ + + +/* ****************************************************************** */ +union clause ast = RISCV_CBO : (cbop, regidx) Should be specific to Zcbop ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ + + +/* ****************************************************************** */ +union clause ast = RISCV_CBO : (cbop, regidx) + +mapping encdec_cbop : cbop <-> bits(12) = { + CBO_CLEAN <-> 0b000000000001, + CBO_FLUSH <-> 0b000000000010, + CBO_INVAL <-> 0b000000000000, + CBO_ZERO <-> 0b000000000100 CBO_ZERO is part of a separate extension to the other three so should get its own ast clause ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > @@ -0,0 +1,245 @@ +/* ****************************************************************** */ +/* This file specifies the instructions in the cmo extension */ + + +/* ****************************************************************** */ +union clause ast = RISCV_CBO : (cbop, regidx) + +mapping encdec_cbop : cbop <-> bits(12) = { + CBO_CLEAN <-> 0b000000000001, + CBO_FLUSH <-> 0b000000000010, + CBO_INVAL <-> 0b000000000000, + CBO_ZERO <-> 0b000000000100 +} + +mapping clause encdec = RISCV_CBO(cbop, rs1) These need guards on the extensions being enabled ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval", + CBO_ZERO <-> "cbo.zero" +} + +mapping clause assembly = RISCV_CBO(cbop, rs1) + <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + +val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +function write_zero(paddr, width) = { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); + match (res) { + MemValue(true) => { + if(unsigned(width) > 8) then + write_zero(paddr + 8, width - 8) Use a loop when you want a loop ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +mapping clause encdec = RISCV_CBO(cbop, rs1) + <-> encdec_cbop(cbop) @ rs1 @ 0b010 @ 0b00000 @ 0b0001111 + +mapping cbo_mnemonic : cbop <-> string = { + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval", + CBO_ZERO <-> "cbo.zero" +} + +mapping clause assembly = RISCV_CBO(cbop, rs1) + <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + +val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +function write_zero(paddr, width) = { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); Why 8? Either do byte by byte or do max_mem_access at a time (which is 16), but don't hard-code an arbitrary word size using magic constants. Also use zeros() rather than to_bits(N, 0). Finally, this is broken if width isn't divisible by 8 (or whatever word size is used), so there should be an assertion to ensure that never happens if it's not expected to (i.e., since everything's a power of two, that it's impossible to configure the cache block size as less than the word size), or it should be handled gracefully (which is one reason to make the model simple and just do a byte-by-byte loop). ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +mapping cbo_mnemonic : cbop <-> string = { + CBO_CLEAN <-> "cbo.clean", + CBO_FLUSH <-> "cbo.flush", + CBO_INVAL <-> "cbo.inval", + CBO_ZERO <-> "cbo.zero" +} + +mapping clause assembly = RISCV_CBO(cbop, rs1) + <-> cbo_mnemonic(cbop) ^ spc() ^ reg_name(rs1) + +val write_zero: (xlenbits, xlenbits) -> MemoryOpResult(bool) effect {wmv, wmvt, rreg, wreg, escape} +function write_zero(paddr, width) = { + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); + match (res) { + MemValue(true) => { + if(unsigned(width) > 8) then Spaces after if, and no parens needed ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + let res : MemoryOpResult(bool) = mem_write_value(paddr, 8, to_bits(64, 0), false, false, false); + match (res) { + MemValue(true) => { + if(unsigned(width) > 8) then + write_zero(paddr + 8, width - 8) + else + MemValue(true) + }, + MemValue(false) => MemValue(false), + MemException(e) => MemException(e) + } +} + +val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_cbo_zero(vaddr, width) = { + match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) { The first argument should be rs1 for the instruction, and you have a bunch of the same bug so I'm only commenting on this one. And BYTE is definitely wrong, it needs to match the exact size of the write you're performing, you can't be lazy like with paging and probe a single byte when writing a whole page, it has to be exact. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } +} + +val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg} +function process_cbo_zero(vaddr, width) = { + match ext_data_get_addr(to_bits(5, 0), vaddr, Write(Data), BYTE) { + Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL }, + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Write(Data)) { + TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + TR_Address(paddr, _) => { + let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false); + match (eares) { + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = write_zero(paddr, width); What if the block size is high enough that it covers multiple pages? ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, + MemValue(_) => { + let res : MemoryOpResult(bool) = write_zero(paddr, width); + match (res) { + MemValue(true) => RETIRE_SUCCESS, + MemValue(false) => internal_error("store got false from mem_write_value"), + MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL } + } + } + } + } + } + } +} + +union translation_check = { So... option(ExceptionType) ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + match translateAddr(vaddr, Execute()) { + TR_Failure(e, _) => TransTrap(e), + TR_Address(paddr, _) => TransSuccess() + } + }; + match fetch { + TransSuccess() => RETIRE_SUCCESS, + TransTrap(fe) => + match (le, se, fe) { + (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_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 }, + (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL } Don't put spaces before commas like that ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } + } + } +} + +union translation_check = { + TransTrap : ExceptionType, + TransSuccess : unit +} + +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) = { + let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) { + Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()), What are all these uses of exception 14 for? You need to pass the ext_data_addr_error to ext_handle_data_check_error and return RETIRE_FAIL if you get an Ext_DataAddr_Error that you decide to honour, not some random reserved exception cause. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_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 }, + (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL } + } + } + } + } + } + } +} + +function check_clean_flush(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | This variable is pointless ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) Just put the second bit in and avoid the EXTZ ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +} + +function check_clean_flush(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | + ((p == User) & (senvcfg.CBCFE() == 0b0))); + ret +} + +function check_inval(p : Privilege) -> bits(2) = { + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | + ((p == User) & (senvcfg.CBIE() == 0b00)); + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) + else EXTZ(0b11) EXTZ is a no-op ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | + ((p == User) & (senvcfg.CBIE() == 0b00)); + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); Give the variables descriptive names, e.g. trap and flush ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + (E_Load_Access_Fault(), _, _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, E_SAMO_Access_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Access_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_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 }, + (_, E_SAMO_Page_Fault(), _) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (_, _, E_Fetch_Page_Fault()) => { handle_mem_exception(vaddr, E_SAMO_Page_Fault()); RETIRE_FAIL }, + (E_Extension(e), _ , _ ) => { ext_handle_data_check_error(e); RETIRE_FAIL } + } + } + } + } + } + } +} + +function check_clean_flush(p : Privilege) -> bool = { These names should probably be more obviously scoped to cache operations and more clearly state that they're about "what operation is this instruction mapped to"; check_foo sounds like an assertion ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } + } + } + } +} + +function check_clean_flush(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBCFE() == 0b0)) | + ((p == User) & (senvcfg.CBCFE() == 0b0))); + ret +} + +function check_inval(p : Privilege) -> bits(2) = { + let bit0 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b00)) | Types shouldn't be needed ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + let bit1 : bool = ((p != Machine) & (menvcfg.CBIE() == 0b01)) | + ((p == User) & (senvcfg.CBIE() == 0b01)); + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) + else EXTZ(0b11) +} + +function check_zero(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | + ((p == User) & (senvcfg.CBZE() == 0b0))); + ret +} + +function clause execute(RISCV_CBO(cbop, rs1)) = { + let rs1_val = X(rs1); + let cache_block_size : xlenbits = plat_cache_block_size() ; No random spaces ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +} + +function check_zero(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | + ((p == User) & (senvcfg.CBZE() == 0b0))); + ret +} + +function clause execute(RISCV_CBO(cbop, rs1)) = { + let rs1_val = X(rs1); + let cache_block_size : xlenbits = plat_cache_block_size() ; + let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1)); + match cbop { + CBO_CLEAN => { + if (check_clean_flush(cur_privilege)) then + /* perform clean*/ Space before the *, but also, this comment is a waste of time ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + if bit0 then EXTZ(0b0) + else if bit1 then EXTZ(0b1) + else EXTZ(0b11) +} + +function check_zero(p : Privilege) -> bool = { + let ret : bool = ~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | + ((p == User) & (senvcfg.CBZE() == 0b0))); + ret +} + +function clause execute(RISCV_CBO(cbop, rs1)) = { + let rs1_val = X(rs1); + let cache_block_size : xlenbits = plat_cache_block_size() ; + let vaddr: xlenbits = rs1_val & ~(cache_block_size - EXTZ(0b1)); + match cbop { This seems like it'd be nicer as two steps: 1. Take the instruction's operation and map it to option(operation) based on the CSRs 2. Treat that operation as the actual operation to perform (with None() being handle_illegal) Also avoids all the magic constants being returned from functions and read here (I realise it's repurposing the encodings of the CSRs, but that's not the most friendly way of writing it) ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > +} + +mapping clause encdec = RISCV_PREFETCH(op, rs1, offset) + <-> offset @ encdec_prefetch(op) @ rs1 @ 0b110 @ 0b00000 @ 0b0010011 + +mapping pre_mnemonic : preop <-> string = { + PREFETCH_I <-> "prefetch.i", + PREFETCH_R <-> "prefetch.r", + PREFETCH_W <-> "prefetch.w" +} + +mapping clause assembly = RISCV_PREFETCH(op, rs1, offset) + <-> pre_mnemonic(op) ^ spc() ^ hex_bits_12(offset @ 0b00000) ^ "(" ^ reg_name(rs1) ^ ")" + +function clause execute(RISCV_PREFETCH(preop, rs1, offset)) = { + /* do nothing other than translate_address for prefetch.i/r/w */ Why do we even bother doing that? They're just hints, they can be entirely nop'ed out in the model like any other hint. Which is already the case, given they're ORI instructions, and base.sail gets included before cmoext.sail so the real ORIs will take precedence and this code is entirely dead. Especially since this is actually wrong, due to translateAddr having the side-effect of (if enabled instead of trapping for software emulation) atomically updating accessed and dirty bits as needed, which is specifically not performed for prefetch. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + TR_Address(paddr, _) => RETIRE_SUCCESS + } + } + }, + PREFETCH_R => { + match ext_data_get_addr(rs1, EXTS(offset @ 0b00000), Read(Data), BYTE) { + Ext_DataAddr_Error(e) => RETIRE_SUCCESS, + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Read(Data)) { + TR_Failure(e, _) => RETIRE_SUCCESS, + TR_Address(paddr, _) => RETIRE_SUCCESS + } + } + } + } +} Make sure every line has a terminating newline character (required by POSIX for a file to be a valid text file) ------------------------------ In model/riscv_sys_control.sail <#137 (comment)>: > @@ -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 Space after the // ------------------------------ In model/riscv_sys_regs.sail <#137 (comment)>: > @@ -813,3 +813,18 @@ 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 + +function legalize_envcfg(c : Envcfg, v : xlenbits) -> Envcfg = { + let c = update_CBZE(c, [v[7]]); + let c = update_CBCFE(c, [v[6]]); + let c = update_CBIE(c, v[5 .. 4]); Doesn't this need to legalise 10? ------------------------------ In model/riscv_types.sail <#137 (comment)>: > +enum cbop = {CBO_CLEAN, CBO_FLUSH, CBO_INVAL, CBO_ZERO} /* cbo ops*/ +enum preop = {PREFETCH_I, PREFETCH_R, PREFETCH_W} /* prefetch ops*/ Follow the convention below; put them in a separate block and include the extension names ------------------------------ In ocaml_emulator/platform_impl.ml <#137 (comment)>: > @@ -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)) Ok so this one defaults to 64 as I'd expect, unlike the C model ------------------------------ In c_emulator/riscv_sim.c <#137 (comment)>: > @@ -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 & 7) == 0) && (block_size < 4096)) { I can't obviously find either of these restrictions in the spec; where have these come from? 4096 seems pretty unproblematic, that's a whole page, things just get awkward when you cover multiple pages, but the PMP already makes that an issue. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } +} + +union translation_check = { + TransTrap : ExceptionType, + TransSuccess : unit +} + +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) = { + let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) { + Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()), + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Read(Data)) { How does invalidate interact with the dirty bit of page table entries? Just translating a read won't dirty the page, but surely an invalidate needs to dirty the page if actually invalidating rather than just cleaning/flushing? Though whether it's "only dirty if the cache line is dirty" or "always dirty even if there's nothing to write back" I don't know. I can only see discussion of accessed and dirty bits for prefetch and zeroing, not management instruction. ------------------------------ In model/riscv_insts_cmoext.sail <#137 (comment)>: > + } + } + } +} + +union translation_check = { + TransTrap : ExceptionType, + TransSuccess : unit +} + +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) = { + let load: translation_check = match ext_data_get_addr(to_bits(5, 0), vaddr, Read(Data), BYTE) { + Ext_DataAddr_Error(e) => TransTrap(E_Reserved_14()), + Ext_DataAddr_OK(vaddr) => + match translateAddr(vaddr, Read(Data)) { (The answer to that affects whether or not you can clean this up by just hoisting all three load, store and fetch calculations and matching on them all at the same time, which would flatten this function somewhat) — Reply to this email directly, view it on GitHub <#137 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJWIR7QEM5BHJMGYTKTURQR4HANCNFSM5KKGQEIA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[jrtc27]

Thanks for an incredibly quick and thorough review. But, at one point you say there shouldn't be random spaces, but the guidelines said you can add them to align things vertically to make them easier to understand. Which would be fine if in this case he added a couple more extra spaces to make the expressions actually line up. Do I have that correct?
…

Yes, that's right; I took an educated guess based on the low number of additional spaces that the intent was not to line things up

[dkruckemyer-ventana]

What are the next steps to take here?

[arichardson]

The description of this PR says prefetch is supported, but I don't see any Zicbop support in the code? Maybe that got lost while splitting up the files?

[ptomsich]

What is the status on this PR?
I see plenty of unresolved review comments but no recent code changes (last update is 8 months old)... who is driving this?

Given that the Zicbo[mpz] extensions are comparatively self-contained (and we don't have to implement any real cache-management functionality/prefetchers), I'd like to see this pushed over the finish line sooner than later.

[liweiwei90]

The description of this PR says prefetch is supported, but I don't see any Zicbop support in the code? Maybe that got lost while splitting up the files?

Yeah. the file with the support for Zicbop is deleted in previous updates. It will be dead code since prefetch instructions reuse the encoding of existed instruction.

[liweiwei90]

What is the status on this PR? I see plenty of unresolved review comments but no recent code changes (last update is 8 months old)... who is driving this?

Sorry, I didn't maintain this PR after I replied the comments and update the code to fix the problems several month ago. I think most of the questions have been resolved or replied(may need further discussion).

Given that the Zicbo[mpz] extensions are comparatively self-contained (and we don't have to implement any real cache-management functionality/prefetchers), I'd like to see this pushed over the finish line sooner than later.

Yeah. I agree. I'll try to re-maintain and update it sooner.

[jrtc27]

At a glance I don't think the extension hooks comments have been properly addressed

[liweiwei90]

At a glance I don't think the extension hooks comments have been properly addressed

Sorry. Do you mean ext_data_get_addr problem?

[jrtc27]

At a glance I don't think the extension hooks comments have been properly addressed

Sorry. Do you mean ext_data_get_addr problem?

Yes. You give it a register index for the base address register used, an offset from that register's value and the size of the memory operation being performed. All of those must be correct. Currently you pass zeros() as the register index, the virtual address as the offset and BYTE as the width. This works in the upstream Sail model because all it does is return Ext_DataAddr_OK(X(base) + offset), but that relies on the specifics of the implementation; your use does not conform to the interface. This would break our work downstream which uses that hook for something actually useful, and needs the register index and access width to be correct.

[liweiwei90]

At a glance I don't think the extension hooks comments have been properly addressed

Sorry. Do you mean ext_data_get_addr problem?

Yes. You give it a register index for the base address register used, an offset from that register's value and the size of the memory operation being performed. All of those must be correct. Currently you pass zeros() as the register index, the virtual address as the offset and BYTE as the width. This works in the upstream Sail model because all it does is return Ext_DataAddr_OK(X(base) + offset), but that relies on the specifics of the implementation; your use does not conform to the interface. This would break our work downstream which uses that hook for something actually useful, and needs the register index and access width to be correct.

Yeah. I don't find the original meaning of this function as I commented before. So I used it as an address calculation progress.
For the rs1 and offset, I can adjust it to conform the interface. However, I think cache block size is right size for the memory access. However it seems not a correct value for it. So Byte is used currently.

[jrtc27]

At a glance I don't think the extension hooks comments have been properly addressed

Sorry. Do you mean ext_data_get_addr problem?

Yes. You give it a register index for the base address register used, an offset from that register's value and the size of the memory operation being performed. All of those must be correct. Currently you pass zeros() as the register index, the virtual address as the offset and BYTE as the width. This works in the upstream Sail model because all it does is return Ext_DataAddr_OK(X(base) + offset), but that relies on the specifics of the implementation; your use does not conform to the interface. This would break our work downstream which uses that hook for something actually useful, and needs the register index and access width to be correct.

Yeah. I don't find the original meaning of this function as I commented before. So I used it as an address calculation progress. For the rs1 and offset, I can adjust it to conform the interface. However, I think cache block size is right size for the memory access. However it seems not a correct value for it. So Byte is used currently.

We can change it to take the actual number of bytes rather than one of the width enum values.

[liweiwei90]

At a glance I don't think the extension hooks comments have been properly addressed

Sorry. Do you mean ext_data_get_addr problem?

Yes. You give it a register index for the base address register used, an offset from that register's value and the size of the memory operation being performed. All of those must be correct. Currently you pass zeros() as the register index, the virtual address as the offset and BYTE as the width. This works in the upstream Sail model because all it does is return Ext_DataAddr_OK(X(base) + offset), but that relies on the specifics of the implementation; your use does not conform to the interface. This would break our work downstream which uses that hook for something actually useful, and needs the register index and access width to be correct.

Yeah. I don't find the original meaning of this function as I commented before. So I used it as an address calculation progress. For the rs1 and offset, I can adjust it to conform the interface. However, I think cache block size is right size for the memory access. However it seems not a correct value for it. So Byte is used currently.

We can change it to take the actual number of bytes rather than one of the width enum values.

OK. I'll change it.

[github-actions]

Unit Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit ab52bc3. ± Comparison against base commit 3fca4c8.

♻️ This comment has been updated with latest results.

[ptomsich]

Action items from today:

• @liweiwei90 Update PR w/ new patch set and provide information on testing (e.g., link to the cbo.zero ACT PR)
• @billmcspadden-riscv Find a subject matter expert (from the CMO TG?) to review the updated test set.

[liweiwei90]

Action items from today:

* @liweiwei90 Update PR w/ new patch set and provide information on testing (e.g., link to the cbo.zero ACT PR)

OK. I'll check the above comments again and mark them as resolved or update the patch if needed. The ACT PR can be found in riscv-non-isa/riscv-arch-test#226

[liweiwei90]

Two problems may need further discussion:

1. What is the reasonable size range for cache block size? Whether cache block size can be multiple pages?
2. For pmpcheck, whether xlenbits type can be converted to atom type? How ?

[ptomsich]

Two problems may need further discussion:

1. What is the reasonable size range for cache block size? Whether cache block size can be multiple pages?

The specification does not disallow it, so it must be supported by our implementations.

The only requirements (from the specification) are:

• naturally aligned
• power-of-two

[Timmmm]

Shouldn't these size_bits be word_width_bytes everywhere?

Also when you rebase you'll have to upload a load of the vector code that calls ext_data_get_addr(). Though you can be lazy and just wait if you want, because I am rebasing/updating this...

[Timmmm]

Is xlenbits the right type? Maybe nat would be better (or range(1, 1024) for performance reasons).

[Timmmm]

I'm working on this. There are a number of things I've noticed/changed - I'll list them here just so they don't get lost in case of unexpected bus accidents. But if you can wait a few weeks I will upload a PR.

• Restrict cache block size to a page size (4096). Technically the spec doesn't disallow larger sizes, but it also describe any behaviour with block sizes larger than a page, and there are lots of questions as to how that would work. I guess they didn't specify it because nobody is going to have a cache block that large anyway, so restricting it to that makes sense IMO.
• Change the block size parameter to be the exponent instead of actual size. This avoids the possibility of invalid values, and makes the code a bit simpler (e.g. making masks). Not 100% sure about this change tbh. --cache-block-size 64 is a bit easier to follow than --cache-block-size-exp 6. I may revert this and just do that transformation in C. Or maybe not because then I also have to figure out how to do it in OCaml.
• Use long CLI option instead of -B.
• Change it from writing 1 byte at a time to just do the whole write in one go. This is faster, simpler and produces more sensible traces.
• To do that I had to increase max_mem_access to 4096, but that's fine. It generates exactly the same code.
• For flush/inval, do PMA/PMP check for read or write access, rather than actually performing a read. This means if only write access is allowed it will work correctly, and also it will produce the correct traces (since no read was actually performed). This depends on our PMA implementation, which I hope to upstream at some point.
• General simplifications, refactoring, minor fixes, comments etc.
• Still no tests in this repo, but we will test it privately using STING.

[davidharrishmc]

As mentioned back in May, cbo.zero support in Sail is gating the ability to verify the cbo.zero tests that were recently added to riscv-arch-test. Looking forward to this PR being completed.

riscv-non-isa/riscv-arch-test#226

[Timmmm]

I've prepared a PR for this, but the people that need to approve me uploading it are on holiday. And also it depends on #350 and an HPM counter PR that I also need to get approval for too. Hopefully not too much longer. #350 is ready to merge I think.

[davidharrishmc]

Nudge.

[Timmmm]

Coincidentally I prepared a PR today. Just getting approval to send it (shouldn't take long).

[Timmmm]

@davidharrishmc See #455

[Timmmm]

#455 was merged so I'll close this one. Thanks for the initial code @liweiwei90!