sail-riscv add support for cmo extension

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

Dec 18 '21 04:12 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.

Dec 18 '21 06:12 liweiwei90

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771784758:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771784779:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771784974:

@@ -0,0 +1,245 @@ +/* ****************************************************************** / +/ This file specifies the instructions in the cmo extension */

Not an extension name

In model/riscv_insts_cmoext.sail https://github.com/riscv/sail-riscv/pull/137#discussion_r771785051:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785096:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785227:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785389:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785539:

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785561:

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786104:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786167:

} +}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786207:
       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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786390:
         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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786996:
       }
     }
   }
 }
} +}
+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787475:
           (_, 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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787525:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787529:

+}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787679:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787805:
           (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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787830:
         }
     }
   }
 }
}

} +}
+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787908:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787924:

+}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788069:

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:

Take the instruction's operation and map it to option(operation) based on the CSRs

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788325:

+}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788443:
       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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788467:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788585:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788674:

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788699:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788770:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771789431:
   }
 }
} +}
+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771789668:
   }
 }
} +}
+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 https://github.com/riscv/sail-riscv/pull/137#pullrequestreview-835745264, 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: @.***>

Dec 18 '21 06:12 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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771784758:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771784779:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771784974:

@@ -0,0 +1,245 @@ +/* ****************************************************************** / +/ This file specifies the instructions in the cmo extension */

Not an extension name

In model/riscv_insts_cmoext.sail https://github.com/riscv/sail-riscv/pull/137#discussion_r771785051:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785096:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785227:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785389:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785539:

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771785561:

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786104:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786167:

} +}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786207:
       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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786390:
         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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771786996:
       }
     }
   }
 }
} +}
+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787475:
           (_, 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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787525:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787529:

+}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787679:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787805:
           (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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787830:
         }
     }
   }
 }
}

} +}
+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787908:

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771787924:

+}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788069:

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:

Take the instruction's operation and map it to option(operation) based on the CSRs

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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788325:

+}

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788443:
       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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788467:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788585:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788674:

+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788699:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771788770:

@@ -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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771789431:
   }
 }
} +}
+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 https://github.com/riscv/sail-riscv/pull/137#discussion_r771789668:
   }
 }
} +}
+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 https://github.com/riscv/sail-riscv/pull/137#pullrequestreview-835745264, 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: @.***>

Dec 18 '21 06:12 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? …

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

Dec 18 '21 06:12 jrtc27

What are the next steps to take here?

Jan 26 '22 15:01 dkruckemyer-ventana

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?

Jan 27 '23 09:01 arichardson

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.

May 25 '23 09:05 ptomsich

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.

May 25 '23 15:05 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.

May 25 '23 15:05 liweiwei90

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

May 26 '23 01:05 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?

May 26 '23 01:05 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.

May 26 '23 01:05 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.

May 26 '23 02:05 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.

May 26 '23 02:05 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.

OK. I'll change it.

May 26 '23 02:05 liweiwei90

Unit Test Results

712 tests ±0 712 :heavy_check_mark: ±0 0s :stopwatch: ±0s     6 suites ±0     0 :zzz: ±0     1 files ±0     0 :x: ±0

Results for commit ab52bc3e. ± Comparison against base commit 3fca4c87.

:recycle: This comment has been updated with latest results.

May 29 '23 20:05 github-actions[bot]

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.

May 30 '23 11:05 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)

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 https://github.com/riscv-non-isa/riscv-arch-test/pull/226

May 30 '23 12:05 liweiwei90

Two problems may need further discussion:

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

May 30 '23 13:05 liweiwei90

Two problems may need further discussion:

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

Jun 01 '23 17:06 ptomsich

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.

Nov 22 '23 12:11 Timmmm

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.

https://github.com/riscv-non-isa/riscv-arch-test/pull/226

Dec 21 '23 14:12 davidharrishmc

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.

Dec 21 '23 15:12 Timmmm

Nudge.

Mar 06 '24 16:03 davidharrishmc

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

Mar 06 '24 19:03 Timmmm

@davidharrishmc See #455

Apr 22 '24 16:04 Timmmm

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

Aug 30 '24 17:08 Timmmm

sail-riscv sail-riscv copied to clipboard

add support for cmo extension

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

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

16 bytes is a strange default, 64 seems like a more common cache line size to default to

Not an extension name

Should be specific to Zcbop

CBO_ZERO is part of a separate extension to the other three so should get its own ast clause

These need guards on the extensions being enabled

Use a loop when you want a loop

Spaces after if, and no parens needed

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.

What if the block size is high enough that it covers multiple pages?

So... option(ExceptionType)

Don't put spaces before commas like that

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.

This variable is pointless

Just put the second bit in and avoid the EXTZ

EXTZ is a no-op

Give the variables descriptive names, e.g. trap and flush

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

Types shouldn't be needed

No random spaces

Space before the *, but also, this comment is a waste of time

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.

Make sure every line has a terminating newline character (required by POSIX for a file to be a valid text file)

Space after the //

Doesn't this need to legalise 10?

Follow the convention below; put them in a separate block and include the extension names

Ok so this one defaults to 64 as I'd expect, unlike the C model

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.

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

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

16 bytes is a strange default, 64 seems like a more common cache line size to default to

Not an extension name

Should be specific to Zcbop

CBO_ZERO is part of a separate extension to the other three so should get its own ast clause

These need guards on the extensions being enabled

Use a loop when you want a loop

Spaces after if, and no parens needed

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.

What if the block size is high enough that it covers multiple pages?

So... option(ExceptionType)

Don't put spaces before commas like that

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.

This variable is pointless

Just put the second bit in and avoid the EXTZ

EXTZ is a no-op

Give the variables descriptive names, e.g. trap and flush

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

Types shouldn't be needed

No random spaces

Space before the *, but also, this comment is a waste of time

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.

Make sure every line has a terminating newline character (required by POSIX for a file to be a valid text file)

Space after the //

Doesn't this need to legalise 10?

Follow the convention below; put them in a separate block and include the extension names

Ok so this one defaults to 64 as I'd expect, unlike the C model

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.

Unit Test Results

sail-riscv
sail-riscv copied to clipboard