diff options
Diffstat (limited to 'mips')
| -rw-r--r-- | mips/mips_insts.sail | 10 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 20 | ||||
| -rw-r--r-- | mips/mips_wrappers.sail | 10 |
3 files changed, 34 insertions, 6 deletions
diff --git a/mips/mips_insts.sail b/mips/mips_insts.sail index f93309ed..e1f8d8e0 100644 --- a/mips/mips_insts.sail +++ b/mips/mips_insts.sail @@ -1118,7 +1118,7 @@ function clause execute (Load(width, signed, linked, base, rt, offset)) = MEMr_reserve(pAddr, wordWidthBytes(width)); } else - MEMr(pAddr, wordWidthBytes(width)); + MEMr_wrapper(pAddr, wordWidthBytes(width)); if (signed) then wGPR(rt) := EXTS(memResult) else @@ -1185,7 +1185,7 @@ function clause execute(LWL(base, rt, offset)) = (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); let pAddr = (TLBTranslate(vAddr, LoadData)) in { - mem_val := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *) + mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) reg_val := rGPR(rt); wGPR(rt) := EXTS(switch(vAddr[1..0]) { @@ -1205,7 +1205,7 @@ function clause execute(LWR(base, rt, offset)) = (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, W); let pAddr = (TLBTranslate(vAddr, LoadData)) in { - mem_val := MEMr (pAddr[63..2] : 0b00, 4); (* read word of interest *) + mem_val := MEMr_wrapper (pAddr[63..2] : 0b00, 4); (* read word of interest *) reg_val := rGPR(rt); wGPR(rt) := EXTS(switch(vAddr[1..0]) (* it is acceptable to sign extend in all cases *) { @@ -1269,7 +1269,7 @@ function clause execute(LDL(base, rt, offset)) = (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - mem_val := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *) + mem_val := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *) reg_val := rGPR(rt); wGPR(rt) := switch(vAddr[2..0]) { @@ -1295,7 +1295,7 @@ function clause execute(LDR(base, rt, offset)) = (bit[64]) vAddr := addrWrapper(EXTS(offset) + rGPR(base), LoadData, D); let pAddr = (TLBTranslate(vAddr, StoreData)) in { - mem_val := MEMr (pAddr[63..3] : 0b000, 8); (* read double of interest *) + mem_val := MEMr_wrapper (pAddr[63..3] : 0b000, 8); (* read double of interest *) reg_val := rGPR(rt); wGPR(rt) := switch(vAddr[2..0]) { diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index a490efb9..5472ae84 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -221,6 +221,13 @@ let (vector <0, 32, inc, (register<(bit[64])>) >) GPR = GPR21, GPR22, GPR23, GPR24, GPR25, GPR26, GPR27, GPR28, GPR29, GPR30, GPR31 ] +(* JTAG Uart registers *) + +register (bit[8]) UART_WDATA +register (bit[1]) UART_WRITTEN +register (bit[8]) UART_RDATA +register (bit[1]) UART_RVALID + (* Check whether a given 64-bit vector is a properly sign extended 32-bit word *) val bit[64] -> bool effect pure NotWordVal function bool NotWordVal (word) = @@ -539,3 +546,16 @@ function bool isAddressAligned(addr, (WordType) wordType) = case D -> (addr[2..0] == 0b000) } +function forall Nat 'n. (bit[8 * 'n]) effect { rmem } MEMr_wrapper ((bit[64]) addr, ([:'n:]) size) = + if (addr == 0x000000007f000000) then + { + let rvalid = (bit[1]) UART_RVALID in + { + UART_RVALID := [bitzero]; + mask(0x00000000 : UART_RDATA : [rvalid] : 0b0000000 : 0x0000) + } + } + else if (addr == 0x000000007f000004) then + mask(0x000000000004ffff) (* Always plenty of write space available and jtag activity *) + else + MEMr(addr, size) diff --git a/mips/mips_wrappers.sail b/mips/mips_wrappers.sail index e8b17a29..03d03cec 100644 --- a/mips/mips_wrappers.sail +++ b/mips/mips_wrappers.sail @@ -35,7 +35,15 @@ (* mips_wrappers.sail: wrappers functions and hooks for CHERI extensibility (mostly identity functions here) *) -function unit effect {wmem} MEMw_wrapper(addr, size, data) = MEMw(addr, size, data) +function unit effect {wmem} MEMw_wrapper(addr, size, data) = + if (addr == 0x000000007f000000) then + { + UART_WDATA := data[31..24]; + UART_WRITTEN := 1; + } + else + MEMw(addr, size, data) + function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) = MEMw_conditional(addr, size, data) |