diff options
Diffstat (limited to 'cheri/sail_latex/sailfnexecuteLoad.tex')
| -rw-r--r-- | cheri/sail_latex/sailfnexecuteLoad.tex | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/cheri/sail_latex/sailfnexecuteLoad.tex b/cheri/sail_latex/sailfnexecuteLoad.tex deleted file mode 100644 index 2db4a73b..00000000 --- a/cheri/sail_latex/sailfnexecuteLoad.tex +++ /dev/null @@ -1,30 +0,0 @@ -function clause #\hyperref[zexecute]{execute}# (#\hyperref[zLoad]{Load}#(width, sign, linked, base, rt, offset)) = - { - vAddr : #\hyperref[zbits]{bits}#(64) = #\hyperref[zaddrWrapper]{addrWrapper}#(#\hyperref[zsignzyextend]{sign\_extend}#(offset) + #\hyperref[zrGPR]{rGPR}#(base), LoadData, width); - if ~ (#\hyperref[zisAddressAligned]{isAddressAligned}#(vAddr, width)) then - (#\hyperref[zSignalExceptionBadAddr]{SignalExceptionBadAddr}#(AdEL, vAddr)) /* unaligned access */ - else - let pAddr = (#\hyperref[zTLBTranslate]{TLBTranslate}#(vAddr, LoadData)) in - { - memResult : #\hyperref[zbits]{bits}#(64) = if (linked) then - { - CP0LLBit = 0b1; - CP0LLAddr = pAddr; - match width { - W => #\hyperref[zextendLoad]{extendLoad}#(#\hyperref[zMEMrzyreservezywrapper]{MEMr\_reserve\_wrapper}#(pAddr, 4), sign), - D => #\hyperref[zextendLoad]{extendLoad}#(#\hyperref[zMEMrzyreservezywrapper]{MEMr\_reserve\_wrapper}#(pAddr, 8), sign), - _ => throw(#\hyperref[zErrorzyinternalzyerror]{Error\_internal\_error}#()) /* there is no llbc or llhc */ - } - } - else - { - match width { - B => #\hyperref[zextendLoad]{extendLoad}#(#\hyperref[zMEMrzywrapper]{MEMr\_wrapper}#(pAddr, 1), sign), - H => #\hyperref[zextendLoad]{extendLoad}#(#\hyperref[zMEMrzywrapper]{MEMr\_wrapper}#(pAddr, 2), sign), - W => #\hyperref[zextendLoad]{extendLoad}#(#\hyperref[zMEMrzywrapper]{MEMr\_wrapper}#(pAddr, 4), sign), - D => #\hyperref[zextendLoad]{extendLoad}#(#\hyperref[zMEMrzywrapper]{MEMr\_wrapper}#(pAddr, 8), sign) - } - }; - #\hyperref[zwGPR]{wGPR}#(rt) = memResult - } - } |