Skip to content

Merge Retire_Failure into ExecutionResult #884

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Merge Retire_Failure into ExecutionResult #884

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,8 @@ mapping clause assembly = ITYPE(imm, rs1, rd, op)
```
union clause ast = SRET : unit

mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
mapping clause encdec = SRET()
<-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011

function clause execute SRET() = {
let sret_illegal : bool = match cur_privilege {
Expand All @@ -190,9 +191,9 @@ function clause execute SRET() = {
Machine => not(currentlyEnabled(Ext_S))
};
if sret_illegal
then { handle_illegal(); RETIRE_FAIL }
then Illegal_Instruction()
else if not(ext_check_xret_priv (Supervisor))
then { ext_fail_xret_priv(); RETIRE_FAIL }
then Ext_XRET_Priv_Failure()
else {
set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_SUCCESS
Expand Down
2 changes: 1 addition & 1 deletion model/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,13 +176,13 @@ foreach (xlen IN ITEMS 32 64)
"riscv_vmem_types.sail"
${sail_regs_srcs}
${sail_sys_srcs}
"riscv_inst_retire.sail"
"riscv_platform.sail"
"riscv_mem.sail"
${sail_vm_srcs}
# Shared/common code for the cryptography extension.
"riscv_types_kext.sail"
"riscv_zvk_utils.sail"
"riscv_inst_retire.sail"
)

if (variant STREQUAL "rvfi")
Expand Down
17 changes: 11 additions & 6 deletions model/riscv_inst_retire.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,16 +6,21 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/

/* Reasons an instruction retire might fail or be incomplete. */
// Return value from `execute()` function.
union ExecutionResult = {
// Successfully retired.
Retire_Success : unit,

union Retire_Failure = {
// standard reasons
Illegal_Instruction : unit,
// WFI executed, which may or may not retire
// depending on the configuration.
Wait_For_Interrupt : unit,

// Did not retire for a standard reason.
Illegal_Instruction : unit,
Trap : (Privilege, ctl_result, xlenbits),
Memory_Exception : (virtaddr, ExceptionType),

// reasons from external extensions
// Did not retire for custom reason.
Ext_CSR_Check_Failure : unit,
Ext_ControlAddr_Check_Failure : ext_control_addr_error,
Ext_DataAddr_Check_Failure : ext_data_addr_error,
Expand All @@ -27,4 +32,4 @@ union Retire_Failure = {
// RETIRE_SUCCESS enum value so that we don't have to immediately
// update all the places RETIRE_SUCCESS was used.

let RETIRE_SUCCESS : ExecutionResult(Retire_Failure) = RETIRE_OK()
let RETIRE_SUCCESS : ExecutionResult = Retire_Success()
30 changes: 15 additions & 15 deletions model/riscv_insts_aext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -82,19 +82,19 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_Error(e) => Ext_DataAddr_Check_Failure(e),
Ext_DataAddr_OK(vaddr) => {
/* "LR faults like a normal load, even though it's in the AMO major opcode space."
* - Andrew Waterman, isa-dev, 10 Jul 2018.
*/
if not(is_aligned(bits_of(vaddr), width))
then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
then Memory_Exception(vaddr, E_Load_Addr_Align())
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Failure(e, _) => Memory_Exception(vaddr, e),
TR_Address(addr, _) =>
match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
Ok(result) => { load_reservation(bits_of(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
},
}
}
Expand Down Expand Up @@ -131,28 +131,28 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_Error(e) => Ext_DataAddr_Check_Failure(e),
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(bits_of(vaddr), width))
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
then Memory_Exception(vaddr, E_SAMO_Addr_Align())
else {
match translateAddr(vaddr, Write(Data)) { /* Write and ReadWrite are equivalent here:
* both result in a SAMO exception */
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Failure(e, _) => Memory_Exception(vaddr, e),
TR_Address(addr, _) => {
// Check reservation with physical address.
if not(match_reservation(bits_of(addr))) then {
/* cannot happen in rmem */
X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
} else {
match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
Ok(_) => {
let rs2_val = X(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
Ok(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
Ok(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
}
}
}
Expand Down Expand Up @@ -201,19 +201,19 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
* Some extensions perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), ReadWrite(Data, Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_Error(e) => Ext_DataAddr_Check_Failure(e),
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(bits_of(vaddr), width))
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
then Memory_Exception(vaddr, E_SAMO_Addr_Align())
else match translateAddr(vaddr, ReadWrite(Data, Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Failure(e, _) => Memory_Exception(vaddr, e),
TR_Address(addr, _) => {
let rs2_val = X(rs2)[width_bytes * 8 - 1 .. 0];
match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
Ok(_) => {
match mem_read(ReadWrite(Data, Data), addr, width_bytes, aq, aq & rl, true) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
Ok(loaded) => {
let result : bits('width_bytes * 8) =
match op {
Expand All @@ -230,7 +230,7 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
match mem_write_value(addr, width_bytes, sign_extend(result), aq & rl, rl, true) {
Ok(true) => { X(rd) = sign_extend(loaded); RETIRE_SUCCESS },
Ok(false) => { internal_error(__FILE__, __LINE__, "AMO got false from mem_write_value") },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
}
}
}
Expand Down
50 changes: 25 additions & 25 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,12 +62,12 @@ function clause execute (JAL(imm, rd)) = {
let target = PC + sign_extend(imm);
/* Extensions get the first checks on the prospective target address. */
match ext_control_check_pc(target) {
Ext_ControlAddr_Error(e) => RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)),
Ext_ControlAddr_Error(e) => Ext_ControlAddr_Check_Failure(e),
Ext_ControlAddr_OK(target) => {
/* Perform standard alignment check */
let target_bits = bits_of(target);
if bit_to_bool(target_bits[1]) & not(currentlyEnabled(Ext_Zca)) then {
RETIRE_FAIL(Memory_Exception(target, E_Fetch_Addr_Align()))
Memory_Exception(target, E_Fetch_Addr_Align())
} else {
X(rd) = get_next_pc();
set_next_pc(target_bits);
Expand Down Expand Up @@ -121,11 +121,11 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
let target = PC + sign_extend(imm);
/* Extensions get the first checks on the prospective target address. */
match ext_control_check_pc(target) {
Ext_ControlAddr_Error(e) => RETIRE_FAIL(Ext_ControlAddr_Check_Failure(e)),
Ext_ControlAddr_Error(e) => Ext_ControlAddr_Check_Failure(e),
Ext_ControlAddr_OK(target) => {
let target_bits = bits_of(target);
if bit_to_bool(target_bits[1]) & not(currentlyEnabled(Ext_Zca)) then {
RETIRE_FAIL(Memory_Exception(target, E_Fetch_Addr_Align()))
Memory_Exception(target, E_Fetch_Addr_Align())
} else {
set_next_pc(target_bits);
RETIRE_SUCCESS
Expand Down Expand Up @@ -305,16 +305,16 @@ function clause execute (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_Error(e) => Ext_DataAddr_Check_Failure(e),
Ext_DataAddr_OK(vaddr) => {
if check_misaligned(vaddr, width)
then RETIRE_FAIL(Memory_Exception(vaddr, E_Load_Addr_Align()))
then Memory_Exception(vaddr, E_Load_Addr_Align())
else match translateAddr(vaddr, Read(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Failure(e, _) => Memory_Exception(vaddr, e),
TR_Address(paddr, _) =>
match mem_read(Read(Data), paddr, width_bytes, aq, rl, false) {
Ok(result) => { X(rd) = extend_value(is_unsigned, result); RETIRE_SUCCESS },
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
},
}
},
Expand Down Expand Up @@ -361,21 +361,21 @@ function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => RETIRE_FAIL(Ext_DataAddr_Check_Failure(e)),
Ext_DataAddr_Error(e) => Ext_DataAddr_Check_Failure(e),
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
then RETIRE_FAIL(Memory_Exception(vaddr, E_SAMO_Addr_Align()))
then Memory_Exception(vaddr, E_SAMO_Addr_Align())
else match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
TR_Failure(e, _) => Memory_Exception(vaddr, e),
TR_Address(paddr, _) => {
match mem_write_ea(paddr, width_bytes, aq, rl, false) {
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e)),
Err(e) => Memory_Exception(vaddr, e),
Ok(_) => {
let rs2_val = X(rs2);
match mem_write_value(paddr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq, rl, false) {
Ok(true) => RETIRE_SUCCESS,
Ok(false) => internal_error(__FILE__, __LINE__, "store got false from mem_write_value"),
Err(e) => RETIRE_FAIL(Memory_Exception(vaddr, e))
Err(e) => Memory_Exception(vaddr, e)
}
}
}
Expand Down Expand Up @@ -584,7 +584,7 @@ function clause execute ECALL() = {
},
excinfo = (None() : option(xlenbits)),
ext = None() };
RETIRE_FAIL(Trap(cur_privilege, CTL_TRAP(t), PC))
Trap(cur_privilege, CTL_TRAP(t), PC)
}

mapping clause assembly = ECALL() <-> "ecall"
Expand All @@ -597,9 +597,9 @@ mapping clause encdec = MRET()

function clause execute MRET() = {
if cur_privilege != Machine
then RETIRE_FAIL(Illegal_Instruction())
then Illegal_Instruction()
else if not(ext_check_xret_priv(Machine))
then RETIRE_FAIL(Ext_XRET_Priv_Failure())
then Ext_XRET_Priv_Failure()
else {
set_next_pc(exception_handler(cur_privilege, CTL_MRET(), PC));
RETIRE_SUCCESS
Expand All @@ -621,9 +621,9 @@ function clause execute SRET() = {
Machine => not(currentlyEnabled(Ext_S))
};
if sret_illegal
then RETIRE_FAIL(Illegal_Instruction())
then Illegal_Instruction()
else if not(ext_check_xret_priv (Supervisor))
then RETIRE_FAIL(Ext_XRET_Priv_Failure())
then Ext_XRET_Priv_Failure()
else {
set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_SUCCESS
Expand All @@ -639,7 +639,7 @@ mapping clause encdec = EBREAK()
<-> 0b000000000001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011

function clause execute EBREAK() =
RETIRE_FAIL(Memory_Exception(Virtaddr(PC), E_Breakpoint()))
Memory_Exception(Virtaddr(PC), E_Breakpoint())

mapping clause assembly = EBREAK() <-> "ebreak"

Expand All @@ -651,11 +651,11 @@ mapping clause encdec = WFI()

function clause execute WFI() =
match cur_privilege {
Machine => RETIRE_FAIL(Wait_For_Interrupt()),
Machine => Wait_For_Interrupt(),
Supervisor => if mstatus[TW] == 0b1
then RETIRE_FAIL(Illegal_Instruction())
else RETIRE_FAIL(Wait_For_Interrupt()),
User => RETIRE_FAIL(Illegal_Instruction())
then Illegal_Instruction()
else Wait_For_Interrupt(),
User => Illegal_Instruction()
}

mapping clause assembly = WFI() <-> "wfi"
Expand All @@ -673,9 +673,9 @@ function clause execute SFENCE_VMA(rs1, rs2) = {
// is 9 but we always set it to 16 for RV64.
let asid = if rs2 != zreg then Some(X(rs2)[asidlen - 1 .. 0]) else None();
match cur_privilege {
User => RETIRE_FAIL(Illegal_Instruction()),
User => Illegal_Instruction(),
Supervisor => match mstatus[TVM] {
0b1 => RETIRE_FAIL(Illegal_Instruction()),
0b1 => Illegal_Instruction(),
0b0 => { flush_TLB(asid, addr); RETIRE_SUCCESS },
},
Machine => { flush_TLB(asid, addr); RETIRE_SUCCESS }
Expand Down
2 changes: 1 addition & 1 deletion model/riscv_insts_begin.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
scattered union ast

/* returns whether an instruction was retired, used for computing minstret */
val execute : ast -> ExecutionResult(Retire_Failure)
val execute : ast -> ExecutionResult
scattered function execute

val assembly : ast <-> string
Expand Down
Loading
Loading