diff options
| -rw-r--r-- | mips/main.sail | 11 | ||||
| -rw-r--r-- | mips/prelude.sail | 6 |
2 files changed, 7 insertions, 10 deletions
diff --git a/mips/main.sail b/mips/main.sail index 45ced6d7..c444d2dc 100644 --- a/mips/main.sail +++ b/mips/main.sail @@ -9,6 +9,13 @@ function fetch_and_execute () = { nextPC = if inBranchDelay then delayedPC else PC + 4; cp2_next_pc(); instCount = instCount + 1; + if UART_WRITTEN then { + putchar(unsigned(UART_WDATA)); + UART_WRITTEN = 0b0; + }; + /* the following skips are required on mips to fake the tag effects otherwise type checker complains */ + skip_rmemt(); + skip_wmvt(); print_bits("PC: ", PC); try { let pc_pa = TranslatePC(PC); @@ -30,10 +37,6 @@ function fetch_and_execute () = { just continue from nextPC, which should have been set to the appropriate exception vector (along with clearing branchPending etc.) . */ }; - if UART_WRITTEN then { - putchar(unsigned(UART_WDATA)); - UART_WRITTEN = 0b0; - } } val elf_entry = { diff --git a/mips/prelude.sail b/mips/prelude.sail index 477d0967..a44cb6bb 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -130,9 +130,6 @@ val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int overload operator ^ = {xor_vec, int_power} -val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n + 'm) - val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) @@ -142,9 +139,6 @@ val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n) overload operator + = {add_range, add_int, add_vec, add_vec_int} -val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n - 'm) - val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) |