aboutsummaryrefslogtreecommitdiff
path: root/model
diff options
context:
space:
mode:
Diffstat (limited to 'model')
-rw-r--r--model/riscv_fetch_rvfi.sail50
1 files changed, 31 insertions, 19 deletions
diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail
index 50251e3..0f2ed4b 100644
--- a/model/riscv_fetch_rvfi.sail
+++ b/model/riscv_fetch_rvfi.sail
@@ -1,21 +1,33 @@
-function fetch() -> FetchResult =
- /* check for legal PC */
- if (PC[0] != bitzero | (PC[1] != bitzero & (~ (haveRVC()))))
- then F_Error(E_Fetch_Addr_Align(), PC)
- else {
- let i = rvfi_instruction.rvfi_insn();
- rvfi_exec->rvfi_order() = minstret;
- rvfi_exec->rvfi_pc_rdata() = EXTZ(get_arch_pc());
- rvfi_exec->rvfi_insn() = EXTZ(i);
+function fetch() -> FetchResult = {
+ rvfi_exec->rvfi_order() = minstret;
+ rvfi_exec->rvfi_pc_rdata() = EXTZ(get_arch_pc());
- /* TODO: should we write these even if they're not really registers? */
- rvfi_exec->rvfi_rs1_data() = EXTZ(X(i[19 .. 15]));
- rvfi_exec->rvfi_rs2_data() = EXTZ(X(i[24 .. 20]));
- rvfi_exec->rvfi_rs1_addr() = sail_zero_extend(i[19 .. 15],8);
- rvfi_exec->rvfi_rs2_addr() = sail_zero_extend(i[24 .. 20],8);
-
- if (i[1 .. 0] == 0b11)
- then F_Base(i)
- else F_RVC(i[15 .. 0])
+ /* First allow extensions to check pc */
+ match ext_fetch_check_pc(PC, PC) {
+ Ext_FetchAddr_Error(e) => F_Ext_Error(e),
+ Ext_FetchAddr_OK(use_pc) => {
+ /* then check PC alignment */
+ if (use_pc[0] != bitzero | (use_pc[1] != bitzero & (~ (haveRVC()))))
+ then F_Error(E_Fetch_Addr_Align(), PC)
+ else {
+ let i = rvfi_instruction.rvfi_insn();
+ rvfi_exec->rvfi_insn() = EXTZ(i);
+ /* TODO: should we write these even if they're not really registers? */
+ rvfi_exec->rvfi_rs1_data() = EXTZ(X(i[19 .. 15]));
+ rvfi_exec->rvfi_rs2_data() = EXTZ(X(i[24 .. 20]));
+ rvfi_exec->rvfi_rs1_addr() = sail_zero_extend(i[19 .. 15],8);
+ rvfi_exec->rvfi_rs2_addr() = sail_zero_extend(i[24 .. 20],8);
+ if (i[1 .. 0] != 0b11)
+ then F_RVC(i[15 .. 0])
+ else {
+ /* fetch PC check for the next instruction granule */
+ PC_hi : xlenbits = PC + 2;
+ match ext_fetch_check_pc(PC, PC_hi) {
+ Ext_FetchAddr_Error(e) => F_Ext_Error(e),
+ Ext_FetchAddr_OK(use_pc_hi) => F_Base(i)
+ }
+ }
+ }
+ }
}
-
+}