diff options
| author | Jon French <jf451@cam.ac.uk> | 2019-03-14 15:30:17 +0000 |
|---|---|---|
| committer | Jon French <jf451@cam.ac.uk> | 2019-03-14 15:30:17 +0000 |
| commit | 734b2f693b3ded3d70c6552d52f9802c46d667a2 (patch) | |
| tree | 3b7c030ff6a6502dacff43e834226d68f9025393 /model/main_rvfi.sail | |
| parent | ba6ed9f40bdb5f6c3fe8c232fdd4fc1b3b634495 (diff) | |
| parent | 925b2c8a0e3b0adc10d9de8dd6620450561e6c52 (diff) | |
| download | sail-riscv-734b2f693b3ded3d70c6552d52f9802c46d667a2.zip sail-riscv-734b2f693b3ded3d70c6552d52f9802c46d667a2.tar.gz sail-riscv-734b2f693b3ded3d70c6552d52f9802c46d667a2.tar.bz2 | |
Merge branch 'master' into rmem_interpreter
Diffstat (limited to 'model/main_rvfi.sail')
| -rw-r--r-- | model/main_rvfi.sail | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/model/main_rvfi.sail b/model/main_rvfi.sail index 0ba4acf..10b5428 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,11 +100,10 @@ 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(); - init_sys(); + init_model(); loop() } catch { Error_not_implemented(s) => print_string("Error: Not implemented: ", s), |