diff options
| -rw-r--r-- | mips_new_tc/Makefile | 15 | ||||
| -rw-r--r-- | mips_new_tc/main.sail | 52 | ||||
| -rw-r--r-- | mips_new_tc/mips_prelude.sail | 16 | ||||
| -rw-r--r-- | mips_new_tc/mips_wrappers.sail | 2 | ||||
| -rw-r--r-- | mips_new_tc/prelude.sail | 1 |
5 files changed, 84 insertions, 2 deletions
diff --git a/mips_new_tc/Makefile b/mips_new_tc/Makefile new file mode 100644 index 00000000..3bef7551 --- /dev/null +++ b/mips_new_tc/Makefile @@ -0,0 +1,15 @@ +THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) +SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..) +export SAIL_DIR +SAIL_LIB_DIR:=$(SAIL_DIR)/lib +MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc + +SAIL:=$(SAIL_DIR)/sail + +MIPS_SAILS:=$(SAIL_LIB_DIR)/flow.sail $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail + +mips: $(MIPS_SAILS) + $(SAIL) -ocaml -o mips $(MIPS_SAILS) + +clean: + rm -rf _sbuild diff --git a/mips_new_tc/main.sail b/mips_new_tc/main.sail new file mode 100644 index 00000000..0ccd7c71 --- /dev/null +++ b/mips_new_tc/main.sail @@ -0,0 +1,52 @@ + + + +val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef} +function fetch_and_execute () = { + while true do { + PC = nextPC; + inBranchDelay = branchPending; + branchPending = 0b0; + nextPC = if inBranchDelay then delayedPC else PC + 4; + + print_bits("PC: ", PC); + try { + let pc_pa = TranslatePC(PC); + /*print_bits("pa: ", pc_pa);*/ + let instr = MEMr_wrapper(pc_pa, 4); + /*print_bits("hex: ", instr);*/ + let instr_ast = decode(instr); + match instr_ast { + Some(HCF) => { + print("simulation stopped due to halt instruction."); + return (); + }, + Some(ast) => execute(ast), + None => {print("Decode failed"); exit (())} /* Never expect this -- unknown instruction should actually result in reserved instruction ISA-level exception (see mips_ri.sail). */ + } + } catch { + ISAException => print("EXCEPTION") + /* ISA-level exception occurrred either during TranslatePC or execute -- + just continue from nextPC, which should have been set to the appropriate + exception vector (along with clearing branchPending etc.) . */ + }; + } +} + +val elf_entry = "Elf_loader.elf_entry" : unit -> int + +val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg} + +function dump_state () : unit -> unit = { + print_bits("DEBUG MIPS PC ", PC); + foreach (idx from 0 to 32) { + print(concat_str("DEBUG MIPS REG ", concat_str(string_of_int(idx), concat_str(" ", BitStr(rGPR(to_bits(5,idx))))))); + } +} + +function main () = { + nextPC = to_bits(64, elf_entry()); + CP0Status->BEV() = bitone; + fetch_and_execute(); + dump_state () +} diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail index 04d00219..24196c29 100644 --- a/mips_new_tc/mips_prelude.sail +++ b/mips_new_tc/mips_prelude.sail @@ -333,6 +333,19 @@ val MEMea_conditional : forall 'n. ( bits(64) , atom('n)) -> unit effect { eame val MEMval : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv } val MEMval_conditional : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> bool effect { wmv } +/* Extern nops with effects, sometimes useful for faking effect */ +val skip_eamem = "skip" : unit -> unit effect {eamem} +val skip_barr = "skip" : unit -> unit effect {barr} + +function MEMr (addr, size) = __MIPS_read(addr, size) +function MEMr_reserve (addr, size) = __MIPS_read(addr, size) +function MEM_sync () = skip_barr() + +function MEMea (addr, size) = skip_eamem() +function MEMea_conditional (addr, size) = skip_eamem() +function MEMval (addr, size, data) = __MIPS_write(addr, size, data) +function MEMval_conditional (addr, size, data) = { __MIPS_write(addr, size, data); true } + enum Exception = { Interrupt, TLBMod, TLBL, TLBS, AdEL, AdES, Sys, Bp, ResI, CpU, Ov, Tr, C2E, C2Trap, @@ -403,10 +416,11 @@ function SignalExceptionMIPS (ex, kccBase) = nextPC = vectorBase + EXTS(vectorOffset) - kccBase; CP0Cause->ExcCode() = ExceptionCode(ex); CP0Status->EXL() = 0b1; - exit (()); + throw (ISAException); } val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg} +function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000) val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} function SignalExceptionBadAddr(ex, badAddr) = diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail index d0a4cdb2..42e3e427 100644 --- a/mips_new_tc/mips_wrappers.sail +++ b/mips_new_tc/mips_wrappers.sail @@ -72,7 +72,7 @@ function TranslatePC (vAddr) = { let have_cp2 = false -function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000) + val ERETHook : unit -> unit function ERETHook() = () diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail index 53cb0510..1fab008b 100644 --- a/mips_new_tc/prelude.sail +++ b/mips_new_tc/prelude.sail @@ -301,6 +301,7 @@ val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit val print_string = "print_string" : (string, string) -> unit union exception = { + ISAException, Error_not_implemented : string, Error_misaligned_access, Error_EBREAK, |