/*========================================================================*/ /* */ /* Copyright (c) 2015-2017 Robert M. Norton */ /* Copyright (c) 2015-2017 Kathyrn Gray */ /* All rights reserved. */ /* */ /* This software was developed by the University of Cambridge Computer */ /* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ /* (REMS) project, funded by EPSRC grant EP/K008528/1. */ /* */ /* Redistribution and use in source and binary forms, with or without */ /* modification, are permitted provided that the following conditions */ /* are met: */ /* 1. Redistributions of source code must retain the above copyright */ /* notice, this list of conditions and the following disclaimer. */ /* 2. Redistributions in binary form must reproduce the above copyright */ /* notice, this list of conditions and the following disclaimer in */ /* the documentation and/or other materials provided with the */ /* distribution. */ /* */ /* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ /* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ /* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ /* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ /* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ /* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ /* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ /* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ /* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ /* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ /* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ /* SUCH DAMAGE. */ /*========================================================================*/ /* mips_prelude.sail: declarations of mips registers, and functions common to mips instructions (e.g. address translation) */ register PC : bits(64) register nextPC : bits(64) /* CP0 Registers */ bitfield CauseReg : bits(32) = { BD : 31, /* branch delay */ /*Z0 : 30,*/ CE : 29.. 28, /* for coprocessor enable exception */ /*Z1 : 27.. 24,*/ IV : 23, /* special interrupt vector not supported */ WP : 22, /* watchpoint exception occurred */ /*Z2 : 21.. 16, */ IP : 15.. 8, /* interrupt pending bits */ /*Z3 : 7,*/ ExcCode : 6.. 2, /* code of last exception */ /*Z4 : 1.. 0,*/ } bitfield TLBEntryLoReg : bits(64) = { CapS : 63, CapL : 62, PFN : 29.. 6, C : 5.. 3, D : 2, V : 1, G : 0, } bitfield TLBEntryHiReg : bits(64) = { R : 63.. 62, VPN2 : 39.. 13, ASID : 7.. 0, } bitfield ContextReg : bits(64) = { PTEBase : 63.. 23, BadVPN2 : 22.. 4, /*ZR : 3.. 0,*/ } bitfield XContextReg : bits(64) = { XPTEBase : 63.. 33, XR : 32.. 31, XBadVPN2 : 30.. 4, } let TLBNumEntries = 64 type TLBIndexT = (bits(6)) let TLBIndexMax : TLBIndexT = 0b111111 val MAX : forall 'n. atom('n) -> atom(2 ^ 'n - 1) effect pure function MAX(n) = pow2(n) - 1 let MAX_U64 = MAX(64) /*unsigned(0xffffffffffffffff)*/ let MAX_VA = MAX(40) /*unsigned(0xffffffffff)*/ let MAX_PA = MAX(36) /*unsigned(0xfffffffff)*/ bitfield TLBEntry : bits(117) = { pagemask : 116.. 101, r : 100.. 99, vpn2 : 98.. 72, asid : 71.. 64, g : 63, valid : 62, caps1 : 61, capl1 : 60, pfn1 : 59.. 36, c1 : 35.. 33, d1 : 32, v1 : 31, caps0 : 30, capl0 : 29, pfn0 : 28.. 5, c0 : 4.. 2, d0 : 1, v0 : 0, } register TLBProbe : bits(1) register TLBIndex : TLBIndexT register TLBRandom : TLBIndexT register TLBEntryLo0 : TLBEntryLoReg register TLBEntryLo1 : TLBEntryLoReg register TLBContext : ContextReg register TLBPageMask : bits(16) register TLBWired : TLBIndexT register TLBEntryHi : TLBEntryHiReg register TLBXContext : XContextReg register TLBEntry00 : TLBEntry register TLBEntry01 : TLBEntry register TLBEntry02 : TLBEntry register TLBEntry03 : TLBEntry register TLBEntry04 : TLBEntry register TLBEntry05 : TLBEntry register TLBEntry06 : TLBEntry register TLBEntry07 : TLBEntry register TLBEntry08 : TLBEntry register TLBEntry09 : TLBEntry register TLBEntry10 : TLBEntry register TLBEntry11 : TLBEntry register TLBEntry12 : TLBEntry register TLBEntry13 : TLBEntry register TLBEntry14 : TLBEntry register TLBEntry15 : TLBEntry register TLBEntry16 : TLBEntry register TLBEntry17 : TLBEntry register TLBEntry18 : TLBEntry register TLBEntry19 : TLBEntry register TLBEntry20 : TLBEntry register TLBEntry21 : TLBEntry register TLBEntry22 : TLBEntry register TLBEntry23 : TLBEntry register TLBEntry24 : TLBEntry register TLBEntry25 : TLBEntry register TLBEntry26 : TLBEntry register TLBEntry27 : TLBEntry register TLBEntry28 : TLBEntry register TLBEntry29 : TLBEntry register TLBEntry30 : TLBEntry register TLBEntry31 : TLBEntry register TLBEntry32 : TLBEntry register TLBEntry33 : TLBEntry register TLBEntry34 : TLBEntry register TLBEntry35 : TLBEntry register TLBEntry36 : TLBEntry register TLBEntry37 : TLBEntry register TLBEntry38 : TLBEntry register TLBEntry39 : TLBEntry register TLBEntry40 : TLBEntry register TLBEntry41 : TLBEntry register TLBEntry42 : TLBEntry register TLBEntry43 : TLBEntry register TLBEntry44 : TLBEntry register TLBEntry45 : TLBEntry register TLBEntry46 : TLBEntry register TLBEntry47 : TLBEntry register TLBEntry48 : TLBEntry register TLBEntry49 : TLBEntry register TLBEntry50 : TLBEntry register TLBEntry51 : TLBEntry register TLBEntry52 : TLBEntry register TLBEntry53 : TLBEntry register TLBEntry54 : TLBEntry register TLBEntry55 : TLBEntry register TLBEntry56 : TLBEntry register TLBEntry57 : TLBEntry register TLBEntry58 : TLBEntry register TLBEntry59 : TLBEntry register TLBEntry60 : TLBEntry register TLBEntry61 : TLBEntry register TLBEntry62 : TLBEntry register TLBEntry63 : TLBEntry let TLBEntries : vector(64, dec, register(TLBEntry)) = [ ref TLBEntry63, ref TLBEntry62, ref TLBEntry61, ref TLBEntry60, ref TLBEntry59, ref TLBEntry58, ref TLBEntry57, ref TLBEntry56, ref TLBEntry55, ref TLBEntry54, ref TLBEntry53, ref TLBEntry52, ref TLBEntry51, ref TLBEntry50, ref TLBEntry49, ref TLBEntry48, ref TLBEntry47, ref TLBEntry46, ref TLBEntry45, ref TLBEntry44, ref TLBEntry43, ref TLBEntry42, ref TLBEntry41, ref TLBEntry40, ref TLBEntry39, ref TLBEntry38, ref TLBEntry37, ref TLBEntry36, ref TLBEntry35, ref TLBEntry34, ref TLBEntry33, ref TLBEntry32, ref TLBEntry31, ref TLBEntry30, ref TLBEntry29, ref TLBEntry28, ref TLBEntry27, ref TLBEntry26, ref TLBEntry25, ref TLBEntry24, ref TLBEntry23, ref TLBEntry22, ref TLBEntry21, ref TLBEntry20, ref TLBEntry19, ref TLBEntry18, ref TLBEntry17, ref TLBEntry16, ref TLBEntry15, ref TLBEntry14, ref TLBEntry13, ref TLBEntry12, ref TLBEntry11, ref TLBEntry10, ref TLBEntry09, ref TLBEntry08, ref TLBEntry07, ref TLBEntry06, ref TLBEntry05, ref TLBEntry04, ref TLBEntry03, ref TLBEntry02, ref TLBEntry01, ref TLBEntry00 ] register CP0Compare : bits(32) register CP0Cause : CauseReg register CP0EPC : bits(64) register CP0ErrorEPC : bits(64) register CP0LLBit : bits(1) register CP0LLAddr : bits(64) register CP0BadVAddr : bits(64) register CP0Count : bits(32) register CP0HWREna : bits(32) register CP0UserLocal : bits(64) register CP0ConfigK0 : bits(3) bitfield StatusReg : bits(32) = { CU : 31.. 28, /* co-processor enable bits */ /* RP/FR/RE/MX/PX not implemented */ BEV : 22, /* use boot exception vectors (initialised to one) */ /* TS/SR/NMI not implemented */ IM : 15.. 8, /* Interrupt mask */ KX : 7, /* kernel 64-bit enable */ SX : 6, /* supervisor 64-bit enable */ UX : 5, /* user 64-bit enable */ KSU : 4.. 3, /* Processor mode */ ERL : 2, /* error level (should be initialised to one, but BERI is different) */ EXL : 1, /* exception level */ IE : 0, /* interrupt enable */ } register CP0Status : StatusReg /* Implementation registers -- not ISA defined */ register branchPending : bits(1) /* Set by branch instructions to implement branch delay */ register inBranchDelay : bits(1) /* Needs to be set by outside world when in branch delay slot */ register delayedPC : bits(64) /* Set by branch instructions to implement branch delay */ val execute_branch : bits(64) -> unit effect {wreg} function execute_branch(pc) = { delayedPC = pc; branchPending = 0b1; } /* General purpose registers */ /* Special registers For MUL/DIV */ register HI : bits(64) register LO : bits(64) register GPR : vector(32, dec, bits(64)) /* JTAG Uart registers */ register UART_WDATA : bits(8) register UART_WRITTEN : bits(1) register UART_RDATA : bits(8) register UART_RVALID : bits(1) /* Check whether a given 64-bit vector is a properly sign extended 32-bit word */ val NotWordVal : bits(64) -> bool effect pure function NotWordVal (word) = (word[31] ^^ 32) != word[63..32] /* Read numbered GP reg. (r0 is always zero) */ val rGPR : bits(5) -> bits(64) effect {rreg} function rGPR idx = { let i as atom(_) = unsigned(idx) in if i == 0 then 0x0000000000000000 else GPR[i] } /* Write numbered GP reg. (writes to r0 ignored) */ val wGPR : (bits(5), bits(64)) -> unit effect {wreg} function wGPR (idx, v) = { let i as atom(_) = unsigned(idx) in if i == 0 then () else GPR[i] = v } val MEMr = {lem: "MEMr"} : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } val MEMr_reserve = {lem: "MEMr_reserve"} : forall 'n. ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem } val MEM_sync = {lem: "MEM_sync"} : unit -> unit effect { barr } val MEMea = {lem: "MEMea"} : forall 'n. ( bits(64) , atom('n)) -> unit effect { eamem } val MEMea_conditional = {lem: "MEMea_conditional"} : forall 'n. ( bits(64) , atom('n)) -> unit effect { eamem } val MEMval = {lem: "MEMval"} : forall 'n. ( bits(64) , atom('n), bits(8*'n)) -> unit effect { wmv } val MEMval_conditional = {lem: "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} val skip_wreg = "skip" : unit -> unit effect {wreg} val skip_rreg = "skip" : unit -> unit effect {rreg} val skip_wmvt = "skip" : unit -> unit effect {wmvt} val skip_rmemt = "skip" : unit -> unit effect {rmemt} val skip_escape = "skip" : unit -> unit effect {escape} 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, XTLBRefillL, XTLBRefillS, XTLBInvL, XTLBInvS, MCheck } /* Return the ISA defined code for an exception condition */ function ExceptionCode (ex) : Exception -> bits(5)= let x : bits(8) = match ex { Interrupt => 0x00, /* Interrupt */ TLBMod => 0x01, /* TLB modification exception */ TLBL => 0x02, /* TLB exception (load or fetch) */ TLBS => 0x03, /* TLB exception (store) */ AdEL => 0x04, /* Address error (load or fetch) */ AdES => 0x05, /* Address error (store) */ Sys => 0x08, /* Syscall */ Bp => 0x09, /* Breakpoint */ ResI => 0x0a, /* Reserved instruction */ CpU => 0x0b, /* Coprocessor Unusable */ Ov => 0x0c, /* Arithmetic overflow */ Tr => 0x0d, /* Trap */ C2E => 0x12, /* C2E coprocessor 2 exception */ C2Trap => 0x12, /* C2Trap maps to same exception code, different vector */ XTLBRefillL => 0x02, XTLBRefillS => 0x03, XTLBInvL => 0x02, XTLBInvS => 0x03, MCheck => 0x18 } in x[4..0] val SignalExceptionMIPS : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} function SignalExceptionMIPS (ex, kccBase) = { /* Only update EPC and BD if not already in EXL mode */ if (~ (CP0Status.EXL())) then { if (inBranchDelay[0]) then { CP0EPC = PC - 4; CP0Cause->BD() = 0b1; } else { CP0EPC = PC; CP0Cause->BD() = 0b0; } }; /* choose an exception vector to branch to. Some are not supported e.g. Reset */ vectorOffset = if (CP0Status.EXL()) then 0x180 /* Always use common vector if in exception mode already */ else if ((ex == XTLBRefillL) | (ex == XTLBRefillS)) then 0x080 else if (ex == C2Trap) then 0x280 /* Special vector for CHERI traps */ else 0x180; /* Common vector */ vectorBase : bits(64) = if CP0Status.BEV() then 0xFFFFFFFFBFC00200 else 0xFFFFFFFF80000000; /* On CHERI we have to subtract KCC.base so that we end up at the right absolute vector address after indirecting via new PCC */ nextPC = vectorBase + sign_extend(vectorOffset) - kccBase; CP0Cause->ExcCode() = ExceptionCode(ex); CP0Status->EXL() = 0b1; throw (ISAException()); } /* Defined either in mips_wrappers (directly calling SignalExceptionMIPS) or in cheri_prelude_common (cheri things plus above) */ val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg} val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} function SignalExceptionBadAddr(ex, badAddr) = { CP0BadVAddr = badAddr; SignalException(ex); } val SignalExceptionTLB : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg} function SignalExceptionTLB(ex, badAddr) = { CP0BadVAddr = badAddr; TLBContext->BadVPN2() = (badAddr[31..13]); TLBXContext->XBadVPN2()= (badAddr[39..13]); TLBXContext->XR() = (badAddr[63..62]); TLBEntryHi->R() = (badAddr[63..62]); TLBEntryHi->VPN2() = (badAddr[39..13]); SignalException(ex); } enum MemAccessType = {Instruction, LoadData, StoreData} enum AccessLevel = {User, Supervisor, Kernel} val int_of_AccessLevel : AccessLevel -> int effect pure function int_of_AccessLevel level = match level { User => 0, Supervisor => 1, Kernel => 2 } /*! Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level. */ val grantsAccess : (AccessLevel, AccessLevel) -> bool function grantsAccess (currentLevel, requiredLevel) = int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel) /*! Returns the current effective access level determined by accessing the relevant parts of the MIPS status register. */ val getAccessLevel : unit -> AccessLevel effect {rreg} function getAccessLevel() = if ((CP0Status.EXL()) | (CP0Status.ERL())) then Kernel else match CP0Status.KSU() { 0b00 => Kernel, 0b01 => Supervisor, 0b10 => User, _ => User /* behaviour undefined, assume user */ } val checkCP0Access : unit->unit effect{escape, rreg, wreg} function checkCP0Access () = { let accessLevel = getAccessLevel() in if ((accessLevel != Kernel) & (~(CP0Status.CU()[0]))) then { CP0Cause->CE() = 0b00; SignalException(CpU); } } val incrementCP0Count : unit -> unit effect {rreg,wreg,escape} function incrementCP0Count() = { TLBRandom = (if (TLBRandom == TLBWired) then (TLBIndexMax) else (TLBRandom - 1)); CP0Count = (CP0Count + 1); if (CP0Count == CP0Compare) then { CP0Cause->IP() = CP0Cause.IP() | 0x80; /* IP7 is timer interrupt */ }; let ims = CP0Status.IM() in let ips = CP0Cause.IP() in let ie = CP0Status.IE() in let exl = CP0Status.EXL() in let erl = CP0Status.ERL() in if ((~(exl)) & (~(erl)) & ie & ((ips & ims) != 0x00)) then SignalException(Interrupt); } type regno = bits(5) /* a register number */ type imm16 = bits(16) /* 16-bit immediate */ /* a commonly used instruction format with three register operands */ type regregreg = (regno, regno, regno) /* a commonly used instruction format with two register operands and 16-bit immediate */ type regregimm16 = (regno, regno, imm16) enum decode_failure = { no_matching_pattern, unsupported_instruction, illegal_instruction, internal_error } /* Used by branch and trap instructions */ enum Comparison = { EQ, /* equal */ NE, /* not equal */ GE, /* signed greater than or equal */ GEU,/* unsigned greater than or equal */ GT, /* signed strictly greater than */ LE, /* signed less than or equal */ LT, /* signed strictly less than */ LTU /* unsigned less than or qual */ } val compare : (Comparison, bits(64), bits(64)) -> bool function compare (cmp, valA, valB) = match cmp { EQ => valA == valB, NE => valA != valB, GE => valA >=_s valB, GEU => valA >=_u valB, GT => valB <_s valA, LE => valB >=_s valA, LT => valA <_s valB, LTU => valA <_u valB } enum WordType = { B, H, W, D} val wordWidthBytes : WordType -> range(1, 8) function wordWidthBytes(w) = match w { B => 1, H => 2, W => 4, D => 8 } /* This function checks that memory accesses are naturally aligned -- it is disabled in favour of BERI specific behaviour below. function bool isAddressAligned(addr, (WordType) wordType) = match wordType { B => true H => (addr[0] == 0) W => (addr[1..0] == 0b00) D => (addr[2..0] == 0b000) } */ /* BERI relaxes the natural alignment requirement for loads and stores but still throws an exception if an access spans a cache line boundary. Here we assume this is 32 bytes so that we don't have to worry about clearing multiple tags when an access spans more than one capability. Capability load/stores are still naturally aligned. Provided this is a factor of smallest supported page size (4k) we don't need to worry about accesses spanning page boundaries either. */ let alignment_width = 16 val isAddressAligned : (bits(64), WordType) -> bool function isAddressAligned (addr, wordType) = let a = unsigned(addr) in a / alignment_width == (a + wordWidthBytes(wordType) - 1) / alignment_width val reverse_endianness = "reverse_endianness" : forall 'W, 'W >= 1. bits(8 * 'W) -> bits(8 * 'W) effect pure /* function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness' (w, value) = { ([:8 * 'W:]) width = length(value); if width <= 8 then value else value[7..0] : reverse_endianness'(w - 1, value[(width - 1) .. 8]) } function rec forall Nat 'W, 'W >= 1. bits(8 * 'W) reverse_endianness ((bits(8 * 'W)) value) = { reverse_endianness'(sizeof 'W, value) }*/ 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 { 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 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) = reverse_endianness(MEMr_reserve(addr, size)) function init_cp0_state () : unit -> unit = { CP0Status->BEV() = bitone; } val init_cp2_state : unit -> unit effect {wreg} val cp2_next_pc: unit -> unit effect {rreg, wreg} val dump_cp2_state : unit -> unit effect {rreg, escape}