diff options
Diffstat (limited to 'cheri/sail_latex/sailfnexecuteLWL.tex')
| -rw-r--r-- | cheri/sail_latex/sailfnexecuteLWL.tex | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/cheri/sail_latex/sailfnexecuteLWL.tex b/cheri/sail_latex/sailfnexecuteLWL.tex deleted file mode 100644 index 46fd760d..00000000 --- a/cheri/sail_latex/sailfnexecuteLWL.tex +++ /dev/null @@ -1,17 +0,0 @@ -function clause #\hyperref[zexecute]{execute}#(#\hyperref[zLWL]{LWL}#(base, rt, offset)) = - { - vAddr = #\hyperref[zaddrWrapperUnaligned]{addrWrapperUnaligned}#(#\hyperref[zsignzyextend]{sign\_extend}#(offset) + #\hyperref[zrGPR]{rGPR}#(base), LoadData, WL); - let pAddr = (#\hyperref[zTLBTranslate]{TLBTranslate}#(vAddr, LoadData)) in - { - mem_val = #\hyperref[zMEMrzywrapper]{MEMr\_wrapper}# (pAddr[63..2] @ 0b00, 4); /* read word of interest */ - reg_val = #\hyperref[zrGPR]{rGPR}#(rt); - result : #\hyperref[zbits]{bits}#(32) = match vAddr[1..0] - { - 0b00 => mem_val, - 0b01 => mem_val[23..0] @ reg_val[07..0], - 0b10 => mem_val[15..0] @ reg_val[15..0], - 0b11 => mem_val[07..0] @ reg_val[23..0] - }; - #\hyperref[zwGPR]{wGPR}#(rt) = #\hyperref[zsignzyextend]{sign\_extend}#(result); - } - } |
