1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
let entryValid = entry.valid in
let entryR = entry.r in
let entryMask = entry.pagemask in
let entryVPN = entry.vpn2 in
let entryASID = entry.asid in
let entryG = entry.g in
(entryValid &
(r == entryR) &
((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) &
((asid == (entryASID)) | (entryG)))
function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
let r = (VAddr[63..62]) in
let vpn2 = (VAddr[39..13]) in
let asid = TLBEntryHi.ASID in {
foreach (idx from 0 to 63) {
if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then
return (Some ((TLBIndexT) idx))
};
None
}
function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
let idx = tlbSearch(vAddr) in
switch(idx) {
case (Some(idx)) ->
let entry = (TLBEntries[idx]) in
let entryMask = entry.pagemask in
let evenOddBit = switch(entryMask) {
case 0x0000 -> 12
case 0x0003 -> 14
case 0x000f -> 16
case 0x003f -> 18
case 0x00ff -> 20
case 0x03ff -> 22
case 0x0fff -> 24
case 0x3fff -> 26
case 0xffff -> 28
case _ -> undefined
} in
let isOdd = (vAddr[evenOddBit]) in
let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then
(entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1)
else
(entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in
if (~(v)) then
(SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
else if ((accessType == StoreData) & ~(d)) then
(SignalExceptionTLB(TLBMod, vAddr))
else
(EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]),
if (accessType == StoreData) then caps else capl)
case None -> (SignalExceptionTLB(
if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
}
}
function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) =
{
let currentAccessLevel = getAccessLevel() in
let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
let (requiredLevel, addr) = switch(vAddr[63..62]) {
case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *)
case (true, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *)
case (true, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *)
case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
case (_, _) -> (Kernel, None) (* xkseg mapped *)
}
case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode (ignored) *)
case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *)
case 0b00 -> (User, None) (* xuseg - user mapped *)
} in
if (((nat)currentAccessLevel) < ((nat)requiredLevel)) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
let (pa, c) = switch(addr) {
case (Some(a)) -> (a, false)
case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
TLBTranslate2(vAddr, accessType)
}
in if (unsigned(pa) > MAX_PA) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
(pa, c)
}
function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
let (addr, c) = TLBTranslateC(vAddr, accessType) in addr
|