diff options
| -rw-r--r-- | model/main_rvfi.sail | 23 | ||||
| -rw-r--r-- | model/riscv_mem.sail | 4 | ||||
| -rw-r--r-- | model/rvfi_dii.sail | 2 |
3 files changed, 17 insertions, 12 deletions
diff --git a/model/main_rvfi.sail b/model/main_rvfi.sail index 0ba4acf..837f2d4 100644 --- a/model/main_rvfi.sail +++ b/model/main_rvfi.sail @@ -4,19 +4,19 @@ val rvfi_fetch : unit -> FetchResult effect {escape, rmem, rreg, wmv, wreg} function rvfi_fetch() = /* check for legal PC */ - if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (haveRVC())))) + if (PC[0] != 0b0 | (PC[1] != 0b0 & (~ (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() = PC; - rvfi_exec->rvfi_insn() = zero_extend(i,64); + rvfi_exec->rvfi_insn() = sail_zero_extend(i,64); /* TODO: should we write these even if they're not really registers? */ rvfi_exec->rvfi_rs1_data() = X(i[19 .. 15]); rvfi_exec->rvfi_rs2_data() = X(i[24 .. 20]); - rvfi_exec->rvfi_rs1_addr() = zero_extend(i[19 .. 15],8); - rvfi_exec->rvfi_rs2_addr() = zero_extend(i[24 .. 20],8); - if (i[1 .. 0] == 0b11) + 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]) } @@ -29,7 +29,7 @@ val rvfi_step : int -> bool effect {barr, eamem, escape, exmem, rmem, rreg, wmv, function rvfi_step(step_no) = { minstret_written = false; /* see note for minstret */ let (retired, stepped) : (bool, bool) = - match curInterrupt(cur_privilege, mip, mie, mideleg) { + match dispatchInterrupt(cur_privilege) { Some(intr, priv) => { print_bits("Handling interrupt: ", intr); handle_interrupt(intr, priv); @@ -51,8 +51,13 @@ function rvfi_step(step_no) = { }, Some(ast) => { print("[" ^ string_of_int(step_no) ^ "] [" ^ cur_privilege ^ "]: " ^ BitStr(PC) ^ " (" ^ BitStr(h) ^ ") " ^ ast); - nextPC = PC + 2; - (execute(ast), true) + /* check for RVC once here instead of every RVC execute clause. */ + if haveRVC() then { + nextPC = PC + 2; + (execute(ast), true) + } else { + (false, true) + } } } }, @@ -95,7 +100,7 @@ function main () = { rvfi_zero_exec_packet(); rvfi_halt_exec_packet(); let _ = rvfi_get_exec_packet(); - PC = zero_extend(0x1000, 64); + PC = sail_zero_extend(0x1000, 64); print_bits("PC = ", PC); try { init_platform(); diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 3549e80..1ccb5c7 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -34,7 +34,7 @@ function rvfi_read (addr, width, result) = { MemValue(v) => if width <= 8 then { - rvfi_exec->rvfi_mem_wdata() = zero_extend(v,64); + rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(v,64); rvfi_exec->rvfi_mem_wmask() = to_bits(8,width) } else (), MemException(_) => () @@ -116,7 +116,7 @@ val rvfi_write : forall 'n, 'n > 0. (xlenbits, atom('n), bits(8 * 'n)) -> unit e function rvfi_write (addr, width, value) = { rvfi_exec->rvfi_mem_addr() = addr; if width <= 8 then { - rvfi_exec->rvfi_mem_wdata() = zero_extend(value,64); + rvfi_exec->rvfi_mem_wdata() = sail_zero_extend(value,64); rvfi_exec->rvfi_mem_wmask() = to_bits(8,width); } } diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 9680ab4..b0e3a06 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -63,7 +63,7 @@ register rvfi_exec : RVFI_DII_Execution_Packet val rvfi_zero_exec_packet : unit -> unit effect {wreg} function rvfi_zero_exec_packet () = - rvfi_exec = Mk_RVFI_DII_Execution_Packet(zero_extend(0b0,704)) + rvfi_exec = Mk_RVFI_DII_Execution_Packet(sail_zero_extend(0b0,704)) val rvfi_halt_exec_packet : unit -> unit effect {wreg} |