summaryrefslogtreecommitdiff
path: root/cheri/sail_latex/sailfnexecuteLWL.tex
diff options
context:
space:
mode:
Diffstat (limited to 'cheri/sail_latex/sailfnexecuteLWL.tex')
-rw-r--r--cheri/sail_latex/sailfnexecuteLWL.tex17
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);
- }
- }