Open
Description
It is fairly difficult for me to verify the RTL for the CSR instruction against the Sail, since they are not really that related at the moment. I have done so, but it requires that I change a fairly large amount of the Sail. In particular:
- There are many CSRs present in the Sail that do not exist in ibex
- The implementation of some CSRs clearly do not match the RTL (e.g. legalisation of mcause and mstatus, and writeability of mcounteren).
- The CHERI
access_system_registers
checks in the RTL clear the output bits, but do not raise an exception. This is fine but the Sail does not do this. Ideally either the RTL would throw an exception, or the Sail would look like the following:
/* snip */
if not(check_CSR(csr, cur_privilege, isWrite))
then { handle_illegal(); RETIRE_FAIL }
else {
let can_read = pcc_access_system_regs() | (csr[11..8] == 0xb);
// or whatever condition is precisely intended ^
let csr_val = if can_read then readCSR(csr) else 0x00000000;
if isWrite & pcc_access_system_regs() then {
let new_val : xlenbits = match op {
CSRRW => rs1_val,
CSRRS => csr_val | rs1_val,
CSRRC => csr_val & ~(rs1_val)
};
writeCSR(csr, new_val)
};
X(rd) = csr_val;
RETIRE_SUCCESS
}
Metadata
Metadata
Assignees
Labels
No labels