summaryrefslogtreecommitdiff
path: root/cheri/sail_latex/sailfntlbEntryMatch.tex
diff options
context:
space:
mode:
Diffstat (limited to 'cheri/sail_latex/sailfntlbEntryMatch.tex')
-rw-r--r--cheri/sail_latex/sailfntlbEntryMatch.tex12
1 files changed, 0 insertions, 12 deletions
diff --git a/cheri/sail_latex/sailfntlbEntryMatch.tex b/cheri/sail_latex/sailfntlbEntryMatch.tex
deleted file mode 100644
index f952062f..00000000
--- a/cheri/sail_latex/sailfntlbEntryMatch.tex
+++ /dev/null
@@ -1,12 +0,0 @@
-function #\hyperref[ztlbEntryMatch]{tlbEntryMatch}#(r, vpn2, asid, entry) =
- let entryValid = entry.#\hyperref[zvalid]{valid}#() in
- let entryR = entry.#\hyperref[zr]{r}#() in
- let entryMask = entry.#\hyperref[zpagemask]{pagemask}#() in
- let entryVPN = entry.#\hyperref[zvpntwo]{vpn2}#() in
- let entryASID = entry.#\hyperref[zasid]{asid}#() in
- let entryG = entry.#\hyperref[zg]{g}#() in
- let vpnMask : #\hyperref[zbits]{bits}#(27) = ~(#\hyperref[zzzerozyextend]{zero\_extend}#(entryMask)) in
- (entryValid &
- (r == entryR) &
- ((vpn2 & vpnMask) == ((entryVPN) & vpnMask)) &
- ((asid == (entryASID)) | (entryG)))