Skip to content

Commit

Permalink
add legalize function for cbie: treat 0b10 as 0b00
Browse files Browse the repository at this point in the history 
delete zicbop (dead code)
add Cbo(_) access type, and update translation progress to support it
update process_clean_inval function
  • Loading branch information
Weiwei Li committed Jan 6, 2022
1 parent 4f86a9e commit 7b39e3f
Show file tree
Hide file tree
Showing 9 changed files with 48 additions and 111 deletions.
1 change: 0 additions & 1 deletion Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,6 @@ SAIL_DEFAULT_INST += riscv_insts_zkn.sail
SAIL_DEFAULT_INST += riscv_insts_zks.sail

SAIL_DEFAULT_INST += riscv_insts_zicbom.sail
SAIL_DEFAULT_INST += riscv_insts_zicbop.sail
SAIL_DEFAULT_INST += riscv_insts_zicboz.sail

SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
Expand Down
51 changes: 16 additions & 35 deletions model/riscv_insts_zicbom.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,47 +25,28 @@ mapping clause assembly = RISCV_ZICBOM(cbop, rs1)

val process_clean_inval : (xlenbits, xlenbits, bool, bool) -> Retired effect {escape, rmem, rmemt, rreg, wmv, wmvt, wreg}
function process_clean_inval(vaddr, width, clean, inval) = {
let load: option(ExceptionType) = match ext_data_get_addr(zeros(), vaddr, Read(Data), BYTE) {
Ext_DataAddr_Error(e) => Some(E_Reserved_14()),
Ext_DataAddr_OK(vaddr) =>
match translateAddr(vaddr, Read(Cbo)) {
TR_Failure(e, _) => Some(e),
TR_Address(paddr, _) => None()
}
};
match load {
None() => RETIRE_SUCCESS,
Some(le) => {
let store: option(ExceptionType) = match ext_data_get_addr(zeros(), vaddr, Write(Data), BYTE) {
Ext_DataAddr_Error(e) => Some(E_Reserved_14()),
Ext_DataAddr_OK(vaddr) =>
match translateAddr(vaddr, Write(Cbo)) {
TR_Failure(e, _) => Some(e),
TR_Address(paddr, _) => None()
}
match ext_data_get_addr(zeros(), vaddr, Cbo(Data), BYTE) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
let data: option(ExceptionType) = match translateAddr(vaddr, Cbo(Data)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Data), cur_privilege),
TR_Failure(e, _) => Some(e)
};
match store {
match data {
None() => RETIRE_SUCCESS,
Some(se) => {
let fetch: option(ExceptionType) = match ext_control_check_addr(vaddr) {
Ext_ControlAddr_Error(e) => Some(E_Reserved_14()),
Ext_ControlAddr_OK(vaddr) =>
match translateAddr(vaddr, Execute()) {
TR_Failure(e, _) => Some(e),
TR_Address(paddr, _) => None()
}
Some(de) => {
let fetch: option(ExceptionType) = match translateAddr(vaddr, Cbo(Fetch)) {
TR_Address(paddr, _) => pmpCheck_xlen(paddr, width, Cbo(Fetch), cur_privilege),
TR_Failure(e, _) => Some(e)
};
match fetch {
None() => RETIRE_SUCCESS,
Some(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 }
match (de, fe) {
(E_SAMO_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_SAMO_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 }
}
}
}
Expand Down
62 changes: 0 additions & 62 deletions model/riscv_insts_zicbop.sail
View file

This file was deleted.

18 changes: 12 additions & 6 deletions model/riscv_pmp_control.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,9 @@ function pmpCheckRWX(ent, acc) = {
Read(_) => ent.R() == 0b1,
Write(_) => ent.W() == 0b1,
ReadWrite(_) => ent.R() == 0b1 & ent.W() == 0b1,
Execute() => ent.X() == 0b1
Execute() => ent.X() == 0b1,
Cbo(Data) => ent.R() == 0b1 | ent.W() == 0b1,
Cbo(Fetch) => ent.X() == 0b1
}
}

Expand Down Expand Up @@ -149,10 +151,8 @@ function pmpMatchEntry(addr: xlenbits, width: xlenbits, acc: AccessType(ext_acce
}

/* priority checks */

function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
function pmpCheck_xlen (addr: xlenbits, width: xlenbits, acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
let check : bool =
match pmpMatchEntry(addr, width, acc, priv, pmp0cfg, pmpaddr0, zeros()) {
PMP_Success => true,
Expand Down Expand Up @@ -222,17 +222,23 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce
_ => false
}
}}}}}}}}}}}}}}}};

if check
then None()
else match acc {
Read(_) => Some(E_Load_Access_Fault()),
Write(_) => Some(E_SAMO_Access_Fault()),
ReadWrite(_) => Some(E_SAMO_Access_Fault()),
Execute() => Some(E_Fetch_Access_Fault())
Execute() => Some(E_Fetch_Access_Fault()),
Cbo(_) => Some(E_SAMO_Access_Fault())
}
}

function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: AccessType(ext_access_type), priv: Privilege)
-> option(ExceptionType) = {
let width : xlenbits = to_bits(sizeof(xlen), width);
pmpCheck_xlen(addr, width, acc, priv)
}

function init_pmp() -> unit = {
pmp0cfg = update_A(pmp0cfg, pmpAddrMatchType_to_bits(OFF));
pmp1cfg = update_A(pmp1cfg, pmpAddrMatchType_to_bits(OFF));
Expand Down
6 changes: 5 additions & 1 deletion model/riscv_pte.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,11 +125,15 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege,
(Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
(ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),
(Cbo(Data), User) => to_pte_check(p.U() == 0b1 & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))),
(Cbo(Fetch), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),

(Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1),
(ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),
(Cbo(Data), Supervisor) => to_pte_check((p.U() == 0b1 | do_sum) & (p.W() == 0b1 | (p.R() == 0b1 | (p.X() == 0b1 & mxr)))),
(Cbo(Fetch), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),

(_, Machine) => internal_error("m-mode mem perm check")
}
Expand All @@ -140,7 +144,7 @@ function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : ex
Execute() => false,
Read() => false,
Write(Data) => true,
Write(Cbo) => false,
Cbo(_) => false,
ReadWrite(_,_) => true
});

Expand Down
4 changes: 3 additions & 1 deletion model/riscv_ptw.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,9 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) ->
(Write(_), PTW_Access()) => E_SAMO_Access_Fault(),
(Write(_), _) => E_SAMO_Page_Fault(),
(Execute(), PTW_Access()) => E_Fetch_Access_Fault(),
(Execute(), _) => E_Fetch_Page_Fault()
(Execute(), _) => E_Fetch_Page_Fault(),
(Cbo(_), PTW_Access()) => E_SAMO_Access_Fault(),
(Cbo(_), _) => E_SAMO_Page_Fault()
} in {
/* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
e
Expand Down
11 changes: 8 additions & 3 deletions model/riscv_sys_regs.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -827,9 +827,14 @@ bitfield Envcfg : xlenbits = {
register senvcfg : Envcfg
register menvcfg : Envcfg

function legalize_envcfg(c : Envcfg, v : xlenbits) -> Envcfg = {
let c = update_CBZE(c, [v[7]]);
function legalize_envcfg_cbie(o : bits(2), v : bits(2)) -> bits(2) = match (v) {
0b10 => 0b00,
_ => v
}

function legalize_envcfg(o : Envcfg, v : xlenbits) -> Envcfg = {
let c = update_CBZE(o, [v[7]]);
let c = update_CBCFE(c, [v[6]]);
let c = update_CBIE(c, v[5 .. 4]);
let c = update_CBIE(c, legalize_envcfg_cbie(o.CBIE(), v[5 .. 4]));
c
}
1 change: 1 addition & 0 deletions model/riscv_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,6 +168,7 @@ enum Retired = {RETIRE_SUCCESS, RETIRE_FAIL}
union AccessType ('a : Type) = {
Read : 'a,
Write : 'a,
Cbo : 'a,
ReadWrite : ('a, 'a),
Execute : unit
}
Expand Down
5 changes: 3 additions & 2 deletions model/riscv_vmem_types.sail
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@
type ext_access_type = unit

let Data : ext_access_type = ()
let Cbo : ext_access_type = ()
let Fetch : ext_access_type = ()

let default_write_acc : ext_access_type = Data

Expand All @@ -81,7 +81,8 @@ function accessType_to_str (a) =
Read(_) => "R",
Write(_) => "W",
ReadWrite(_, _) => "RW",
Execute() => "X"
Execute() => "X",
Cbo(_) => "RWX"
}

overload to_str = {accessType_to_str}

0 comments on commit 7b39e3f

Please sign in to comment.