diff options
Diffstat (limited to 'cheri/sail_latex/sailfntlbSearch.tex')
| -rw-r--r-- | cheri/sail_latex/sailfntlbSearch.tex | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/cheri/sail_latex/sailfntlbSearch.tex b/cheri/sail_latex/sailfntlbSearch.tex deleted file mode 100644 index 8bce6f3b..00000000 --- a/cheri/sail_latex/sailfntlbSearch.tex +++ /dev/null @@ -1,10 +0,0 @@ -function #\hyperref[ztlbSearch]{tlbSearch}#(VAddr) = - let r = (VAddr[63..62]) in - let vpn2 = (VAddr[39..13]) in - let asid = TLBEntryHi.#\hyperref[zASID]{ASID}#() in { - foreach (idx from 0 to 63) { - if(#\hyperref[ztlbEntryMatch]{tlbEntryMatch}#(r, vpn2, asid, #\hyperref[zregzyderef]{reg\_deref}#(TLBEntries[idx]))) then - return #\hyperref[zSome]{Some}#(#\hyperref[ztozybits]{to\_bits}#(6, idx)) - }; - #\hyperref[zNone]{None}#() - } |