diff options
| author | Robert Norton | 2018-05-17 17:26:16 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-05-17 17:29:37 +0100 |
| commit | 2c5bbd6f7fbfdf32bafab50e36a1bebcd7cd8dab (patch) | |
| tree | d1da5c12d566d80a230520ca5bbbc88710e27fa5 /mips/mips_prelude.sail | |
| parent | 1867ec89a4493ca6ce92c8926885c4090b6d3d5d (diff) | |
changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ocaml main so that we can have simboot + kernel. Support UART output only.
Diffstat (limited to 'mips/mips_prelude.sail')
| -rw-r--r-- | mips/mips_prelude.sail | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index f9049b5d..c151f38b 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -614,22 +614,20 @@ function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * reverse_endianness'(sizeof 'W, value) }*/ -val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem} -function MEMr_wrapper (addr, size) = reverse_endianness(MEMr (addr, size)) -/* TODO +val MEMr_wrapper : forall 'n, 1 <= 'n <=8 . (bits(64), atom('n)) -> bits(8*'n) effect {rmem, rreg, wreg} +function MEMr_wrapper (addr, size) = if (addr == 0x000000007f000000) then { let rvalid = UART_RVALID in - let rdata = (bits(8 * 'n)) (mask(0x00000000 : UART_RDATA : rvalid : 0b0000000 : 0x0000)) in { UART_RVALID = [bitzero]; - rdata + mask(0x00000000 @ UART_RDATA @ rvalid @ 0b0000000 @ 0x0000) } } else if (addr == 0x000000007f000004) then mask(0x000000000004ffff) /* Always plenty of write space available and jtag activity */ else - reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ */ + reverse_endianness(MEMr(addr, size)) /* MEMr assumes little endian */ val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } function MEMr_reserve_wrapper (addr , size) = |