Skip to content

Commit

Permalink
Change the parameters of ext_data_get_addr in riscv_insns_zicbo*.sail to
Browse files Browse the repository at this point in the history 
conform to the interface.

Update the type of width parameter of ext_data_get_addr to xlenbits.
  • Loading branch information
Weiwei Li committed May 26, 2023
1 parent 3337007 commit fabc698
Show file tree
Hide file tree
Showing 6 changed files with 32 additions and 30 deletions.
2 changes: 1 addition & 1 deletion model/riscv_addr_checks.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ type ext_data_addr_error = unit

/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : word_width)
function ext_data_get_addr(base : regidx, offset : xlenbits, acc : AccessType(ext_access_type), width : xlenbits)
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)
Expand Down
6 changes: 3 additions & 3 deletions model/riscv_insts_aext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read(Data), width) {
match ext_data_get_addr(rs1, zeros(), Read(Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -186,7 +186,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), width) {
match ext_data_get_addr(rs1, zeros(), Write(Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -276,7 +276,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width) {
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite(Data, Data)) {
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_base.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -386,7 +386,7 @@ function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -442,7 +442,7 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_insts_fext.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ function clause execute(LOAD_FP(imm, rs1, rd, width)) = {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width) {
match ext_data_get_addr(rs1, offset, Read(Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -441,7 +441,7 @@ function clause execute (STORE_FP(imm, rs2, rs1, width)) = {
let (aq, rl, con) = (false, false, false);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width) {
match ext_data_get_addr(rs1, offset, Write(Data), EXTZ(size_bits(width))) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down
17 changes: 9 additions & 8 deletions model/riscv_insts_zicbom.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,17 @@ mapping cbop_mnemonic : cbop_zicbom <-> string = {
mapping clause assembly = RISCV_ZICBOM(cbop, rs1)
<-> cbop_mnemonic(cbop) ^ spc() ^ "(" ^ reg_name(rs1) ^ ")"

val process_clean_inval : (xlenbits, xlenbits, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_clean_inval(vaddr, width, cbop) = {
match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) {
val process_clean_inval : (regidx, cbop_zicbom) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_clean_inval(rs1, cbop) = {
let rs1_val = X(rs1);
let cache_block_size = plat_cache_block_size();
let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1));
let offset = begin_addr - rs1_val;
match ext_data_get_addr(rs1, offset, Read(Data), cache_block_size) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let res: option(ExceptionType) = match translateAddr(vaddr, Read(Data)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Read(Data), cur_privilege),
TR_Address(paddr, _) => pmpCheck_xlen(paddr, cache_block_size, Read(Data), cur_privilege),
TR_Failure(e, _) => Some(e)
};
match res {
Expand Down Expand Up @@ -58,9 +62,6 @@ function cbop_for_cbo_inval(p : Privilege) -> option(cbop_zicbom) = {
}

function clause execute(RISCV_ZICBOM(cbop, rs1)) = {
let rs1_val = X(rs1);
let cache_block_size = plat_cache_block_size();
let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1));
let cbcfe = cbo_clean_flush_enable(cur_privilege);
let final_op : option(cbop_zicbom) = match (cbop, cbcfe) {
(CBO_CLEAN, true) => Some(CBO_CLEAN),
Expand All @@ -71,6 +72,6 @@ function clause execute(RISCV_ZICBOM(cbop, rs1)) = {
};
match final_op {
None() => { handle_illegal(); RETIRE_FAIL },
Some(cbop) => process_clean_inval(vaddr, cache_block_size, cbop)
Some(cbop) => process_clean_inval(rs1, cbop)
}
}
29 changes: 15 additions & 14 deletions model/riscv_insts_zicboz.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,16 +12,20 @@ mapping clause assembly = RISCV_ZICBOZ(rs1)
function get_envcfg_cbze(p : Privilege) -> bool =
~(((p != Machine) & (menvcfg.CBZE() == 0b0)) | ((p == User) & (senvcfg.CBZE() == 0b0)))

val process_cbo_zero : (xlenbits, xlenbits) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_cbo_zero(vaddr, width) = {
offset : xlenbits = zeros();
val process_cbo_zero : (regidx) -> Retired effect {eamem, escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_cbo_zero(rs1) = {
let rs1_val = X(rs1);
let cache_block_size = plat_cache_block_size();
let begin_addr = rs1_val & ~(cache_block_size - EXTZ(0b1));
let offset = begin_addr - rs1_val;
index : xlenbits = zeros();
failed : bool = false;
while (offset <_u width) & (failed == false) do {
let addr = vaddr + offset;
match ext_data_get_addr(zeros(), addr, Write(Data), BYTE) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true },
Ext_DataAddr_OK(vaddr) =>
match translateAddr(vaddr, Write(Data)) {
match ext_data_get_addr(rs1, offset, Write(Data), cache_block_size) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); failed = true },
Ext_DataAddr_OK(vaddr) =>
while (index <_u cache_block_size) & (failed == false) do {
let addr = vaddr + index;
match translateAddr(addr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); failed = true },
TR_Address(paddr, _) => {
let eares : MemoryOpResult(unit) = mem_write_ea(paddr, 1, false, false, false);
Expand All @@ -30,7 +34,7 @@ function process_cbo_zero(vaddr, width) = {
MemValue(_) => {
let res : MemoryOpResult(bool) = mem_write_value(paddr, 1, zeros(), false, false, false);
match (res) {
MemValue(true) => offset = offset + EXTZ(0b1),
MemValue(true) => index = index + EXTZ(0b1),
MemValue(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
MemException(e) => { handle_mem_exception(vaddr, e); failed = true }
}
Expand All @@ -45,11 +49,8 @@ function process_cbo_zero(vaddr, width) = {
}

function clause execute(RISCV_ZICBOZ(rs1)) = {
let rs1_val = X(rs1);
let cache_block_size = plat_cache_block_size();
let vaddr = rs1_val & ~(cache_block_size - EXTZ(0b1));
if get_envcfg_cbze(cur_privilege) then
process_cbo_zero(vaddr, cache_block_size)
process_cbo_zero(rs1)
else {
handle_illegal();
RETIRE_FAIL
Expand Down

0 comments on commit fabc698

Please sign in to comment.