aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRishiyur S. Nikhil <nikhil@acm.org>2024-04-01 11:07:57 -0400
committerGitHub <noreply@github.com>2024-04-01 10:07:57 -0500
commitf601c866153c79a7ae8404f939dc2d66aa2e41f9 (patch)
tree276b3e032c8455d415ccf2265d5288f1f316bc82
parentd564b93310dd43f519325a418da056f78b1daef2 (diff)
downloadsail-riscv-f601c866153c79a7ae8404f939dc2d66aa2e41f9.zip
sail-riscv-f601c866153c79a7ae8404f939dc2d66aa2e41f9.tar.gz
sail-riscv-f601c866153c79a7ae8404f939dc2d66aa2e41f9.tar.bz2
Unify VM code
Old vmem code had much 'cut-and-paste' replication for RV32 (Sv32) and (#408) RV64 (Sv39, Sv48), and was scattered over several files. New code unifies them into single set of parameterized functions that works for RV32/RV64 and Sv32/Sv39/Sv48 (and is ready for Sv57). Deleted old files: riscv_vmem_rv32.sail riscv_vmem_rv64.sail riscv_vmem_sv32.sail riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_pte.sail riscv_ptw.sail Current files: all named riscv_vmem_* riscv_vmem.sail (root file for vmem) riscv_vmem_common.sail riscv_vmem_pte.sail riscv_vmem_ptw.sail riscv_vmem_tlb.sail riscv_vmem_types.sail Modified top-level Makefile accordingly. Added documentation on new vmem code: doc/notes_Virtual_Memory.adoc
Diffstat
-rw-r--r--Makefile24
-rw-r--r--doc/figs/notes_Virtual_Memory_Fig1.svg1027
-rw-r--r--doc/notes_Virtual_Memory.adoc119
-rw-r--r--model/riscv_pte.sail92
-rw-r--r--model/riscv_vmem.sail452
-rw-r--r--model/riscv_vmem_common.sail245
-rw-r--r--model/riscv_vmem_pte.sail135
-rw-r--r--model/riscv_vmem_ptw.sail (renamed from model/riscv_ptw.sail)45
-rw-r--r--model/riscv_vmem_rv32.sail75
-rw-r--r--model/riscv_vmem_rv64.sail114
-rw-r--r--model/riscv_vmem_sv32.sail200
-rw-r--r--model/riscv_vmem_sv39.sail194
-rw-r--r--model/riscv_vmem_sv48.sail156
-rw-r--r--model/riscv_vmem_tlb.sail139
14 files changed, 1966 insertions, 1051 deletions
diff --git a/Makefile b/Makefile
index 2552241..deaad55 100644
--- a/Makefile
+++ b/Makefile
@@ -71,15 +71,21 @@ SAIL_SYS_SRCS += riscv_softfloat_interface.sail riscv_fdext_regs.sail riscv_fdex
SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions
SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling
-SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
-SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
-
-SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail
-ifeq ($(ARCH),RV32)
-SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS)
-else
-SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
-endif
+# SAIL_RV32_VM_SRCS = riscv_vmem_sv32.sail riscv_vmem_rv32.sail
+# SAIL_RV64_VM_SRCS = riscv_vmem_sv39.sail riscv_vmem_sv48.sail riscv_vmem_rv64.sail
+
+# SAIL_VM_SRCS = riscv_pte.sail riscv_ptw.sail riscv_vmem_common.sail riscv_vmem_tlb.sail
+# ifeq ($(ARCH),RV32)
+# SAIL_VM_SRCS += $(SAIL_RV32_VM_SRCS)
+# else
+# SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
+# endif
+
+SAIL_VM_SRCS += riscv_vmem_common.sail
+SAIL_VM_SRCS += riscv_vmem_pte.sail
+SAIL_VM_SRCS += riscv_vmem_ptw.sail
+SAIL_VM_SRCS += riscv_vmem_tlb.sail
+SAIL_VM_SRCS += riscv_vmem.sail
# Non-instruction sources
PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
diff --git a/doc/figs/notes_Virtual_Memory_Fig1.svg b/doc/figs/notes_Virtual_Memory_Fig1.svg
new file mode 100644
index 0000000..4c5b224
--- /dev/null
+++ b/doc/figs/notes_Virtual_Memory_Fig1.svg
@@ -0,0 +1,1027 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ width="8.0886383in"
+ height="2.3645477in"
+ viewBox="0 0 205.4514 60.059512"
+ version="1.1"
+ id="svg8"
+ sodipodi:docname="notes_Virtual_Memory_Fig1.svg"
+ inkscape:version="1.3 (0e150ed, 2023-07-21)"
+ inkscape:export-filename="/home/nikhil/git_clones/BESSPIN-CloudGFE/AWSteria_RISCV_Virtio/Doc/Fig_010_AWSteria_RISCV_Virtio.png"
+ inkscape:export-xdpi="96"
+ inkscape:export-ydpi="96"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:dc="http://purl.org/dc/elements/1.1/">
+ <defs
+ id="defs2">
+ <marker
+ style="overflow:visible"
+ id="marker6"
+ refX="0"
+ refY="0"
+ orient="auto-start-reverse"
+ inkscape:stockid="Triangle arrow"
+ markerWidth="1"
+ markerHeight="1"
+ viewBox="0 0 1 1"
+ inkscape:isstock="true"
+ inkscape:collect="always"
+ preserveAspectRatio="xMidYMid">
+ <path
+ transform="scale(0.5)"
+ style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
+ d="M 5.77,0 -2.88,5 V -5 Z"
+ id="path6" />
+ </marker>
+ <marker
+ style="overflow:visible"
+ id="marker4"
+ refX="0"
+ refY="0"
+ orient="auto-start-reverse"
+ inkscape:stockid="Triangle arrow"
+ markerWidth="1"
+ markerHeight="1"
+ viewBox="0 0 1 1"
+ inkscape:isstock="true"
+ inkscape:collect="always"
+ preserveAspectRatio="xMidYMid">
+ <path
+ transform="scale(0.5)"
+ style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
+ d="M 5.77,0 -2.88,5 V -5 Z"
+ id="path4" />
+ </marker>
+ <marker
+ style="overflow:visible"
+ id="Triangle"
+ refX="0"
+ refY="0"
+ orient="auto-start-reverse"
+ inkscape:stockid="Triangle arrow"
+ markerWidth="1"
+ markerHeight="1"
+ viewBox="0 0 1 1"
+ inkscape:isstock="true"
+ inkscape:collect="always"
+ preserveAspectRatio="xMidYMid">
+ <path
+ transform="scale(0.5)"
+ style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
+ d="M 5.77,0 -2.88,5 V -5 Z"
+ id="path135" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1546"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1544"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.4,0,0,-0.4,-4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1380"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1378"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(0.4,0,0,0.4,4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ style="overflow:visible"
+ id="Arrow1Send"
+ refX="0"
+ refY="0"
+ orient="auto"
+ inkscape:stockid="Arrow1Send"
+ inkscape:isstock="true">
+ <path
+ transform="matrix(-0.2,0,0,-0.2,-1.2,0)"
+ style="fill:context-stroke;fill-rule:evenodd;stroke:context-stroke;stroke-width:1pt"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ id="path118023"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker2384"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path2382"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.4,0,0,-0.4,-4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker5333"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path5331"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.4,0,0,-0.4,-4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker5323"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path5321"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.4,0,0,-0.4,-4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker4147"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path4145"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.4,0,0,-0.4,-4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker2243"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path2241"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#a20000;fill-opacity:1;fill-rule:evenodd;stroke:#a20000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.4,0,0,-0.4,-4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1817"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1157"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(0.4,0,0,0.4,4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Sstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow1Sstart"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1066"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(0.2,0,0,0.2,1.2,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker2666"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path2664"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(0.4,0,0,0.4,4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Mend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Mend"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1081"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="scale(-0.6)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker2486"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path2484"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker2404"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path2402"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.8,0,0,-0.8,-10,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow1Lend"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1057"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(-0.8,0,0,-0.8,-10,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Mstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow1Mstart"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1060"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(0.4,0,0,0.4,4,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow1Lstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow1Lstart"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1054"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ transform="matrix(0.8,0,0,0.8,10,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lstart"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lstart"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1072"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(1.1,0,0,1.1,1.1,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1075"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
+ inkscape:connector-curvature="0" />
+ </marker>
+ <marker
+ inkscape:stockid="Tail"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Tail"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <g
+ id="g1102"
+ transform="scale(-1.2)"
+ style="fill:#000000;fill-opacity:1;stroke:#000000;stroke-opacity:1">
+ <path
+ id="path1090"
+ d="M -3.8048674,-3.9585227 0.54352094,0"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.8;stroke-linecap:round;stroke-opacity:1"
+ inkscape:connector-curvature="0" />
+ <path
+ id="path1092"
+ d="M -1.2866832,-3.9585227 3.0617053,0"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.8;stroke-linecap:round;stroke-opacity:1"
+ inkscape:connector-curvature="0" />
+ <path
+ id="path1094"
+ d="M 1.3053582,-3.9585227 5.6537466,0"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.8;stroke-linecap:round;stroke-opacity:1"
+ inkscape:connector-curvature="0" />
+ <path
+ id="path1096"
+ d="M -3.8048674,4.1775838 0.54352094,0.21974226"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.8;stroke-linecap:round;stroke-opacity:1"
+ inkscape:connector-curvature="0" />
+ <path
+ id="path1098"
+ d="M -1.2866832,4.1775838 3.0617053,0.21974226"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.8;stroke-linecap:round;stroke-opacity:1"
+ inkscape:connector-curvature="0" />
+ <path
+ id="path1100"
+ d="M 1.3053582,4.1775838 5.6537466,0.21974226"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.8;stroke-linecap:round;stroke-opacity:1"
+ inkscape:connector-curvature="0" />
+ </g>
+ </marker>
+ </defs>
+ <sodipodi:namedview
+ id="base"
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1.0"
+ inkscape:pageopacity="0.0"
+ inkscape:pageshadow="2"
+ inkscape:zoom="1.180926"
+ inkscape:cx="388.67802"
+ inkscape:cy="113.89367"
+ inkscape:document-units="mm"
+ inkscape:current-layer="layer1"
+ showgrid="false"
+ units="in"
+ inkscape:showpageshadow="false"
+ inkscape:window-width="1472"
+ inkscape:window-height="840"
+ inkscape:window-x="0"
+ inkscape:window-y="37"
+ inkscape:window-maximized="0"
+ inkscape:document-rotation="0"
+ inkscape:snap-global="false"
+ inkscape:pagecheckerboard="0"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ showborder="true"
+ inkscape:deskcolor="#d1d1d1" />
+ <metadata
+ id="metadata5">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <g
+ inkscape:label="Layer 1"
+ inkscape:groupmode="layer"
+ id="layer1"
+ transform="translate(-101.49153,-112.42737)">
+ <rect
+ style="fill:#fff1cc;fill-opacity:1;stroke:#000000;stroke-width:0.25;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect4939"
+ width="125.49309"
+ height="55.944481"
+ x="137.12114"
+ y="114.31551"
+ ry="2.3316531"
+ rx="2.5557346" />
+ <text
+ transform="scale(0.81534918,1.2264684)"
+ xml:space="preserve"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.58873px;line-height:1.25;font-family:'Ubuntu Mono';-inkscape-font-specification:'Ubuntu Mono, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ x="97.405945"
+ y="134.38924"
+ id="text974" />
+ <flowRoot
+ xml:space="preserve"
+ id="flowRoot1059"
+ style="font-style:normal;font-weight:normal;font-size:40px;line-height:1.25;font-family:sans-serif;letter-spacing:0px;word-spacing:0px;fill:#000000;fill-opacity:1;stroke:none"><flowRegion
+ id="flowRegion1061"><rect
+ id="rect1063"
+ width="80.070229"
+ height="88.413681"
+ x="371.76654"
+ y="181.8848" /></flowRegion><flowPara
+ id="flowPara1065" /></flowRoot>
+ <g
+ id="g9"
+ transform="translate(-49.622752,35.523771)">
+ <rect
+ ry="0"
+ y="108.40541"
+ x="192.79189"
+ height="7.1145091"
+ width="14.717851"
+ id="rect1236"
+ style="fill:#ffdd55;stroke:#000000;stroke-width:0.202686;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ rx="0" />
+ <text
+ id="text1256"
+ y="111.11807"
+ x="200.02472"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:0;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:center;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan1254"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:center;writing-mode:lr-tb;text-anchor:middle;stroke-width:0.264583"
+ y="111.11807"
+ x="200.02472"
+ sodipodi:role="line">register</tspan><tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;line-height:0.95;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:center;writing-mode:lr-tb;text-anchor:middle;stroke-width:0.264583"
+ y="114.22251"
+ x="200.02472"
+ sodipodi:role="line"
+ id="tspan7">satp</tspan></text>
+ </g>
+ <text
+ id="text13675"
+ y="147.06259"
+ x="115.48001"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan13673"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="147.06259"
+ x="115.48001"
+ sodipodi:role="line">readCSR()</tspan></text>
+ <text
+ id="text1"
+ y="152.38425"
+ x="114.99237"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan1"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="152.38425"
+ x="114.99237"
+ sodipodi:role="line">writeCSR()</tspan></text>
+ <text
+ id="text2"
+ y="127.36551"
+ x="118.3431"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan2"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="127.36551"
+ x="118.3431"
+ sodipodi:role="line">Exec Fetch</tspan></text>
+ <text
+ id="text4"
+ y="162.47141"
+ x="106.89098"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan4"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="162.47141"
+ x="106.89098"
+ sodipodi:role="line">Exec SFENCE.VMA</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ x="138.24333"
+ y="118.39961"
+ id="text5"><tspan
+ sodipodi:role="line"
+ x="138.24333"
+ y="118.39961"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke-width:0.264583"
+ id="tspan5">PUBLIC</tspan></text>
+ <text
+ id="text10"
+ y="154.81339"
+ x="143.27039"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan10"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="154.81339"
+ x="143.27039"
+ sodipodi:role="line">legalize_satp()</tspan></text>
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 131.08217,146.10039 9.72194,1.41668"
+ id="path10" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 131.01779,150.84595 9.72193,-1.41668"
+ id="path11" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 131.01779,152.20482 9.72193,1.41668"
+ id="path12" />
+ <text
+ id="text12"
+ y="129.33925"
+ x="140.94533"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan12"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="129.33925"
+ x="140.94533"
+ sodipodi:role="line">translateAddr()</tspan></text>
+ <text
+ id="text14"
+ y="137.06709"
+ x="138.13412"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan14"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="137.06709"
+ x="138.13412"
+ sodipodi:role="line">union TR_Result</tspan></text>
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 134.27151,126.52583 5.24514,1.24367"
+ id="path1" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 134.27649,130.40406 5.1777,-1.00431"
+ id="path2" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker4)"
+ d="m 152.7748,130.1562 v 4.02821 l -20.82878,0.0982"
+ id="path3"
+ sodipodi:nodetypes="ccc" />
+ <rect
+ style="fill:#ffeb8c;fill-opacity:1;stroke:#000000;stroke-width:0.250001;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect23780"
+ width="95.946877"
+ height="50.37587"
+ x="166.65634"
+ y="119.94226"
+ ry="2.0797374"
+ rx="2.7964213" />
+ <text
+ xml:space="preserve"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ x="167.70322"
+ y="123.9887"
+ id="text6"><tspan
+ sodipodi:role="line"
+ x="167.70322"
+ y="123.9887"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke-width:0.264583"
+ id="tspan6">PRIVATE</tspan></text>
+ <rect
+ style="fill:#f5f5f5;fill-opacity:1;stroke:#000000;stroke-width:0.25;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect1098"
+ width="93.787857"
+ height="26.170418"
+ x="169.13605"
+ y="143.96143"
+ ry="3.3773639"
+ rx="3.2054558" />
+ <text
+ id="text11"
+ y="129.4375"
+ x="171.20601"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan11"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="129.4375"
+ x="171.20601"
+ sodipodi:role="line">translate()</tspan></text>
+ <text
+ id="text16"
+ y="152.201"
+ x="241.45401"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan16"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="152.201"
+ x="241.45401"
+ sodipodi:role="line">add_to_TLB()</tspan></text>
+ <text
+ id="text17"
+ y="152.201"
+ x="216.80208"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan17"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="152.201"
+ x="216.80208"
+ sodipodi:role="line">write_TLB()</tspan></text>
+ <text
+ id="text19"
+ y="129.06493"
+ x="266.80228"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan19"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="129.06493"
+ x="266.80228"
+ sodipodi:role="line">mem_read_priv()</tspan></text>
+ <text
+ id="text20"
+ y="136.8886"
+ x="266.80225"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan20"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="136.8886"
+ x="266.80225"
+ sodipodi:role="line">mem_write_value_priv()</tspan></text>
+ <rect
+ style="fill:#e8e8e8;fill-opacity:1;stroke:#000000;stroke-width:0.25;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect20"
+ width="71.976585"
+ height="16.149025"
+ x="191.1438"
+ y="154.08107"
+ ry="2.0840757"
+ rx="2.4599962" />
+ <text
+ xml:space="preserve"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ x="192.46194"
+ y="158.02766"
+ id="text21"><tspan
+ sodipodi:role="line"
+ x="192.46194"
+ y="158.02766"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke-width:0.264583"
+ id="tspan21">PRIVATE</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ x="170.6655"
+ y="147.87431"
+ id="text22"><tspan
+ sodipodi:role="line"
+ x="170.6655"
+ y="147.87431"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;fill:#800000;fill-opacity:1;stroke-width:0.264583"
+ id="tspan22">PUBLIC</tspan></text>
+ <g
+ id="g10"
+ transform="translate(-30.652516,-12.719399)">
+ <rect
+ ry="0"
+ y="174.35956"
+ x="223.64394"
+ height="7.1145091"
+ width="14.717851"
+ id="rect7"
+ style="fill:#ffdd55;stroke:#000000;stroke-width:0.202686;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ rx="0" />
+ <text
+ id="text9"
+ y="177.07222"
+ x="230.87677"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:0;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:center;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan8"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:center;writing-mode:lr-tb;text-anchor:middle;stroke-width:0.264583"
+ y="177.07222"
+ x="230.87677"
+ sodipodi:role="line">register</tspan><tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;line-height:0.95;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:center;writing-mode:lr-tb;text-anchor:middle;stroke-width:0.264583"
+ y="180.17667"
+ x="230.87677"
+ sodipodi:role="line"
+ id="tspan9">tlb</tspan></text>
+ </g>
+ <text
+ id="text23"
+ y="129.4375"
+ x="199.20695"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan23"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="129.4375"
+ x="199.20695"
+ sodipodi:role="line">translate_TLB_miss()</tspan></text>
+ <text
+ id="text24"
+ y="137.29741"
+ x="195.8665"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan24"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="137.29741"
+ x="195.8665"
+ sodipodi:role="line">translate_TLB_hit()</tspan></text>
+ <text
+ id="text25"
+ y="152.201"
+ x="188.56508"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan25"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="152.201"
+ x="188.56508"
+ sodipodi:role="line">lookup_TLB()</tspan></text>
+ <text
+ id="text26"
+ y="167.38203"
+ x="143.40154"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan26"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="167.38203"
+ x="143.40154"
+ sodipodi:role="line">init_vmem()</tspan></text>
+ <text
+ id="text27"
+ y="167.28378"
+ x="172.77797"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan27"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="167.28378"
+ x="172.77797"
+ sodipodi:role="line">init_TLB()</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 161.71545,166.40828 h 9.43685"
+ id="path27" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 133.911,166.60478 h 7.03222"
+ id="path28" />
+ <text
+ id="text28"
+ y="167.39078"
+ x="115.92992"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan28"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="167.39078"
+ x="115.92992"
+ sodipodi:role="line">init_model()</tspan></text>
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.250001;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 176.87577,129.89865 10.83428,18.5958"
+ id="path29" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.249999;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 186.89072,128.86365 7.96138,5.91995"
+ id="path31" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.249999;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 186.76893,128.64926 h 10.72358"
+ id="path32" />
+ <text
+ id="text32"
+ y="129.4375"
+ x="238.05617"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan32"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="129.4375"
+ x="238.05617"
+ sodipodi:role="line">pt_walk()</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.249999;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 231.21921,128.64926 h 5.27935"
+ id="path33" />
+ <text
+ id="text33"
+ y="168.06976"
+ x="213.94431"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan33"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="168.06976"
+ x="213.94431"
+ sodipodi:role="line">make_TLB_Entry()</tspan></text>
+ <text
+ id="text18"
+ y="158.48621"
+ x="213.68057"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan18"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="158.48621"
+ x="213.68057"
+ sodipodi:role="line">match_TLB_Entry()</tspan></text>
+ <text
+ id="text13"
+ y="162.36276"
+ x="173.46573"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan13"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="162.36276"
+ x="173.46573"
+ sodipodi:role="line">flush_TLB()</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 133.91099,161.48895 h 37.84215"
+ id="path5" />
+ <text
+ id="text15"
+ y="163.39867"
+ x="213.97531"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan15"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="163.39867"
+ x="213.97531"
+ sodipodi:role="line">flush_TLB_Entry()</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 252.20272,128.64926 h 13.71791"
+ id="path34" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.250001;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 252.27727,128.30859 13.41221,7.08193"
+ id="path35" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 223.7105,136.54059 h 42.02785"
+ id="path36" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.249998;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 197.59749,137.97424 17.60506,12.38488"
+ id="path37" />
+ <path
+ style="fill:#ffffff;stroke:#000000;stroke-width:0.249997;stroke-dasharray:none;marker-end:url(#Triangle)"
+ d="m 223.9594,130.04656 16.5295,19.76265"
+ id="path38" />
+ <text
+ id="text38"
+ y="116.68557"
+ x="186.33632"
+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:'Courier New';-inkscape-font-specification:'Courier New Bold';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan38"
+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:2.82222px;font-family:'Courier New';-inkscape-font-specification:'Courier New Bold';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="116.68557"
+ x="186.33632"
+ sodipodi:role="line">riscv_vmem.sail</tspan></text>
+ <text
+ id="text39"
+ y="146.455"
+ x="203.03865"
+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:'Courier New';-inkscape-font-specification:'Courier New Bold';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan39"
+ style="font-style:normal;font-variant:normal;font-weight:bold;font-stretch:normal;font-size:2.82222px;font-family:'Courier New';-inkscape-font-specification:'Courier New Bold';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="146.455"
+ x="203.03865"
+ sodipodi:role="line">riscv_vmem_tlb.sail</tspan></text>
+ <text
+ id="text40"
+ y="145.43625"
+ x="266.60574"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan40"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="145.43625"
+ x="266.60574"
+ sodipodi:role="line">satp64Mode_of_Bits()</tspan></text>
+ <text
+ id="text41"
+ y="150.93819"
+ x="266.50751"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan41"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="150.93819"
+ x="266.50751"
+ sodipodi:role="line">cur_privilege</tspan></text>
+ <text
+ id="text42"
+ y="154.67165"
+ x="266.40927"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan42"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="154.67165"
+ x="266.40927"
+ sodipodi:role="line">effectivePrivilege()</tspan></text>
+ <text
+ id="text43"
+ y="131.39372"
+ x="102.97906"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan43"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="131.39372"
+ x="102.97906"
+ sodipodi:role="line">Exec Load/Store/AMO</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.25;stroke-dasharray:none;marker-end:url(#marker6)"
+ d="m 162.96671,128.551 h 6.88608"
+ id="path43" />
+ <text
+ id="text3"
+ y="158.58211"
+ x="266.40927"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:3.52778px;line-height:1.25;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;letter-spacing:0px;word-spacing:0px;writing-mode:lr-tb;text-anchor:start;fill:#000000;fill-opacity:1;stroke:none;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ id="tspan3"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:2.82222px;font-family:sans-serif;-inkscape-font-specification:sans-serif;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-feature-settings:normal;text-align:start;writing-mode:lr-tb;text-anchor:start;stroke-width:0.264583"
+ y="158.58211"
+ x="266.40927"
+ sodipodi:role="line">plat_enable_dirty_update()</tspan></text>
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.0999998;stroke-dasharray:none"
+ id="rect1"
+ width="205.35141"
+ height="59.959511"
+ x="101.54153"
+ y="112.47737"
+ rx="0"
+ ry="0" />
+ </g>
+</svg>
diff --git a/doc/notes_Virtual_Memory.adoc b/doc/notes_Virtual_Memory.adoc
new file mode 100644
index 0000000..fba39a1
--- /dev/null
+++ b/doc/notes_Virtual_Memory.adoc
@@ -0,0 +1,119 @@
+= Notes on the Virtual Memory part Sail RISC-V Spec
+
+NOTE: this is an AsciiDoc document and can be processed into
+ browser-readable HTML by the free, open-source tool
+ `asciidoctor`.
+
+NOTE: If you are a code maintainer, kindly update this document if
+ there are any significant developements in vmem code.
+
+This is a commentary/reader's guide to the virtual memory ("vmem")
+code in the Sail RISC-V Formal Spec ("Golden Model"). The primary
+vmem specification code is in file:
+
+ model/riscv_vmem.sail
+
+Additional files:
+
+ model/riscv_vmem_common.sail
+ model/riscv_vmem_pte.sail
+ model/riscv_vmem_ptw.sail
+ model/riscv_vmem_tlb.sail
+ model/riscv_vmem_types.sail
+
+`riscv_vmem_common.sail` contains the parameterization for Sv32, Sv39,
+Sv48 and Sv57.
+
+`riscv_vmem_pte.sail` describes Page Table Entries, checks for
+permission bits, etc.
+
+`riscv_vmem_ptw.sail` describes Page Table Walk exceptions.
+
+`riscv_vmem_tlb.sail` implements a simple TLB (Translation Look-Aside
+Buffer). TLBs are not part of the RISC-V architecture spec.
+Nevertheless, it is useful to model at least a minimal TLB so that we
+can demonstrate and test SFENCE.VMA functionality (without TLBs,
+SFENCE.VMA is a no-op and there's nothing to test).
+
+TLBs are also useful for sail-riscv model simulation speed. Without a
+TLB, every Fetch and Load/Store/AMO in virtual memory mode requires a
+full page table walk. Speed matters mostly for large simulations
+(e.g., Linux-boot can speed up from tens of minutes to a few minutes).
+
+The main vmem code in `riscv_vmem.sail` is structured and commented to
+make it is easy to ignore/skip TLB-related parts.
+
+`riscv_vmem_types.sail` concerns non-standard extensions to the vmem
+system and can be ignored (it is used, e.g., by U.Cambridge's CHERI
+system).
+
+// SECTION ================================================================
+== Simplified call graph
+
+The following figure shows a rough call graph, and this can serve as a
+guide for understanding the code.
+
+image::./figs/notes_Virtual_Memory_Fig1.svg[align="center"]
+
+The yellow rectangle(s) represent the code in `riscv_vmem.sail`, and
+the grey rectangle(s) represent the code in `riscv_vmem_tlb.sail`. In
+each case, the lighter outer rectangle shows the publicly visible
+resources ("API"), and the darker inner rectangle shows internal
+(private) resources.
+
+On the left are shown the external places from which the vmem code is
+invoked, using its public resources. On the right are shown the
+external resources used by the vmem code.
+
+The main flow (ignoring TLBs) is at the top: The external execution
+code for instruction fetch, load, store and AMO invoke
+`translateAddr()` and receive a result of `TR_Result` type.
+`translateAddr()`, in turn, invokes `translate()`,
+`translate_TLB_miss()` and `pt_walk()`; the latter invokes the
+external `mem_read_priv()` to read PTEs (Page Table Entries) from
+memory. The SATP register lives in this vmem code, and is accessed by
+the external general `readCSR()` and `writeCSR()` functions.
+
+`translate()` invokes `lookup_TLB()` and, if a hit, invokes
+`translate_TLB_hit()`, avoiding a page-table walk (and therefore no
+reads from memory).
+
+`mem_write_value_priv()` is called for writing back, to memory, PTEs
+(Page Table Entries) whose A and/or D bits have been modified as part
+of the access.
+
+// SECTION ================================================================
+== Status
+
+* 2024-02-18: Many stylistic updates based on PR comments.
+
+* 2023-11-30: Passing all ISA tests in `tests/riscv-tests` (163 for
+ RV32 and 229 for RV64, about half of which run with Virtual Memory).
+ Also passing 712 tests in GitHub CI flow.
+
+* 2023-11-30: Sv57 not yet implemented (the code has placeholders
+ for Sv57 support; search for "Sv57")
+
+* 2023-11-30: Sv48 or Sv57 have not been tested; we do not have any tests for them.
+
+// SECTION ================================================================
+== Diary notes
+
+2019: Original code written, primarily by https://github.com/pmundkur[@pmundkur]
+
+2023-11: Refactored by https://github.com/rsnikhil[@rsnikhil] for:
+
+* Unifying previously separate RV32/RV64, Sv32/Sv39/Sv57 code into a
+ single, parameterized code.
+* Misc. stylistic improvements.
+* Deleted older files:
++
+ riscv_pte.sail
+ riscv_ptw.sail
+ riscv_vmem_common.sail
+ riscv_vmem_rv32.sail
+ riscv_vmem_rv64.sail
+ riscv_vmem_sv32.sail
+ riscv_vmem_sv39.sail
+ riscv_vmem_sv48.sail
++
diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail
deleted file mode 100644
index 1a5bb0e..0000000
--- a/model/riscv_pte.sail
+++ /dev/null
@@ -1,92 +0,0 @@
-/*=======================================================================================*/
-/* This Sail RISC-V architecture model, comprising all files and */
-/* directories except where otherwise noted is subject the BSD */
-/* two-clause license in the LICENSE file. */
-/* */
-/* SPDX-License-Identifier: BSD-2-Clause */
-/*=======================================================================================*/
-
-/* PTE attributes, permission checks and updates */
-
-type pteAttribs = bits(8)
-
-/* Reserved PTE bits could be used by extensions on RV64. There are
- * no such available bits on RV32, so these bits will be zeros on RV32.
- */
-type extPte = bits(10)
-
-/*
- * On SV32, there are no reserved bits available to extensions. Therefore, by
- * default, we initialize the PTE extension field with all zeros. However,
- * extensions may wish, on SV39/48/56, to put flags in the reserved region of
- * those PTEs. To avoid the need for "inhibit" bits in extensions (i.e., so
- * that extensions can use the more common and more RISC-V flavored "enable"
- * disposition), we allow extensions to use any constant value by overriding
- * this default_sv32_ext_pte value.
- */
-let default_sv32_ext_pte : extPte = zeros()
-
-bitfield PTE_Bits : pteAttribs = {
- D : 7,
- A : 6,
- G : 5,
- U : 4,
- X : 3,
- W : 2,
- R : 1,
- V : 0
-}
-
-function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
- let a = Mk_PTE_Bits(p);
- a[R] == 0b0 & a[W] == 0b0 & a[X] == 0b0
-}
-
-function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
- let a = Mk_PTE_Bits(p);
- a[V] == 0b0 | (a[W] == 0b1 & a[R] == 0b0)
-}
-
-union PTE_Check = {
- PTE_Check_Success : ext_ptw,
- PTE_Check_Failure : (ext_ptw, ext_ptw_fail)
-}
-
-function to_pte_check(b : bool) -> PTE_Check =
- if b then PTE_Check_Success(()) else PTE_Check_Failure((), ())
-
-/* For extensions: this function gets the extension-available bits of the PTE in extPte,
- * and the accumulated information of the page-table-walk in ext_ptw. It should return
- * the updated ext_ptw in both the success and failure cases.
- */
-function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = {
- match (ac, priv) {
- (Read(_), User) => to_pte_check(p[U] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))),
- (Write(_), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1),
- (ReadWrite(_, _), User) => to_pte_check(p[U] == 0b1 & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))),
- (Execute(), User) => to_pte_check(p[U] == 0b1 & p[X] == 0b1),
-
- (Read(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & (p[R] == 0b1 | (p[X] == 0b1 & mxr))),
- (Write(_), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1),
- (ReadWrite(_, _), Supervisor) => to_pte_check((p[U] == 0b0 | do_sum) & p[W] == 0b1 & (p[R] == 0b1 | (p[X] == 0b1 & mxr))),
- (Execute(), Supervisor) => to_pte_check(p[U] == 0b0 & p[X] == 0b1),
-
- (_, Machine) => internal_error(__FILE__, __LINE__, "m-mode mem perm check")
- }
-}
-
-function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = {
- let update_d = p[D] == 0b0 & (match a { // dirty-bit
- Execute() => false,
- Read() => false,
- Write(_) => true,
- ReadWrite(_,_) => true
- });
-
- let update_a = p[A] == 0b0; // accessed-bit
- if update_d | update_a then {
- let np = update_A(p, 0b1);
- let np = if update_d then update_D(np, 0b1) else np;
- Some(np, ext)
- } else None()
-}
diff --git a/model/riscv_vmem.sail b/model/riscv_vmem.sail
new file mode 100644
index 0000000..2d1e5d1
--- /dev/null
+++ b/model/riscv_vmem.sail
@@ -0,0 +1,452 @@
+/*=======================================================================================*/
+/* This Sail RISC-V architecture model, comprising all files and */
+/* directories except where otherwise noted is subject the BSD */
+/* two-clause license in the LICENSE file. */
+/* */
+/* SPDX-License-Identifier: BSD-2-Clause */
+/*=======================================================================================*/
+
+// ****************************************************************
+// Virtual memory address translation and memory protection,
+// including PTWs (Page Table Walks) and TLBs (Translation Look-aside Buffers)
+// Supported VM modes: Sv32, Sv39, Sv48. TODO: Sv57
+
+// STYLE NOTES:
+// PRIVATE items are used only within this VM code.
+// PUBLIC items are invoked from other parts of sail-riscv.
+
+// TLB NOTE:
+// TLBs are not part of the RISC-V architecture specification.
+// However, we model a simple TLB so that
+// (1) we can meaningfully test SFENCE.VMA which is a no-op wihout TLBs;
+// (2) we can greatly speed up simulation speed
+// (e.g., from 10s or minutes to few minutes for Linux boot)
+// The TLB implementation is in a separate file: riscv_vmem_tlb.sail
+// The code in this file is structured and commented so you can easily
+// ignore TLB functionality at first reading.
+
+// ****************************************************************
+// Fields of virtual addresses
+
+// PRIVATE: Extract full VPN field from VA
+function vpns_of_va(sv_params : SV_Params,
+ va : bits(64)) -> bits(64) = {
+ let mask : bits(64) = zero_extend(ones(sv_params.va_size_bits));
+ (va & mask) >> pagesize_bits
+}
+
+// PRIVATE: Extract VPN[level] from VA
+function vpn_j_of_va(sv_params : SV_Params,
+ va : bits(64),
+ level : PTW_Level) -> bits(64) = {
+ let lsb : range(0,63) = pagesize_bits + level * sv_params.vpn_size_bits;
+ assert (lsb < sizeof(xlen));
+ let mask : bits(64) = zero_extend(ones(sv_params.vpn_size_bits));
+ ((va >> lsb) & mask)
+}
+
+// PRIVATE: Extract offset within page from VA
+function offset_of_va(va : bits(64)) -> bits(PAGESIZE_BITS) = va[pagesize_bits - 1 .. 0]
+
+// Valid xlen-wide values containing virtual addrs must have upper
+// bits equal to the MSB of the virtual address.
+// Virtual address widths depend on the virtual memory mode.
+// PRIVATE
+function is_valid_vAddr(struct { va_size_bits, _ } : SV_Params,
+ vAddr : bits(64)) -> bool =
+ vAddr == sign_extend(vAddr[va_size_bits - 1 .. 0])
+
+// ****************************************************************
+// Results of Page Table Walk (PTW)
+
+// PRIVATE
+union PTW_Result = {
+ PTW_Success: (bits(64), bits(64), bits(64), nat, bool, ext_ptw),
+ PTW_Failure: (PTW_Error, ext_ptw)
+}
+
+// ****************************************************************
+// Page Table Walk (PTW)
+
+// Note: 'pt_walk()' is recursive => needs separate 'val' decls
+
+// PRIVATE
+val pt_walk : (SV_Params,
+ bits(64), // virtual addr
+ AccessType(ext_access_type), // Read/Write/ReadWrite/Execute
+ Privilege, // User/Supervisor/Machine
+ bool, // mstatus.MXR
+ bool, // do_sum
+ bits(64), // PT base addr
+ PTW_Level, // tree level for this recursive call
+ bool, // global translation,
+ ext_ptw) // ext_ptw
+ -> PTW_Result
+
+function pt_walk(sv_params,
+ va,
+ ac,
+ priv,
+ mxr,
+ do_sum,
+ pt_base,
+ level,
+ global,
+ ext_ptw) = {
+ let vpn_j = vpn_j_of_va(sv_params, va, level);
+ let pte_offset = vpn_j << sv_params.log_pte_size_bytes;
+ let pte_addr = pt_base + pte_offset;
+
+ // In Sv32, physical addrs are actually 34 bits, not XLEN(=32) bits.
+ // Below, 'pte_phys_addr' is XLEN bits because it's an arg to
+ // 'mem_read_priv()' [riscv_mem.sail] where it's declared as xlenbits.
+ // That def and this use need to be fixed together (TODO)
+ let pte_phys_addr : xlenbits = pte_addr[(sizeof(xlen) - 1) .. 0];
+
+ // Read this-level PTE from mem
+ let mem_result = mem_read_priv(Read(Data), // AccessType
+ Supervisor, // Privilege
+ pte_phys_addr,
+ 8, // atom (8)
+ false, // aq
+ false, // rl
+ false); // res
+
+ match mem_result {
+ MemException(_) => PTW_Failure(PTW_Access(), ext_ptw),
+ MemValue(pte) => {
+ let pte_flags = Mk_PTE_Flags(pte[7 .. 0]);
+ if pte_is_invalid(pte_flags) then
+ PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
+ else {
+ let ppns : bits(64) = PPNs_of_PTE(sv_params, pte);
+ let global' = global | (pte_flags[G] == 0b1);
+ if pte_is_ptr(pte_flags) then {
+ // Non-Leaf PTE
+ if level > 0 then {
+ // follow the pointer to walk next level
+ let pt_base' : bits(64) = ppns << pagesize_bits;
+ let level' = level - 1;
+ pt_walk(sv_params, va, ac, priv, mxr, do_sum,
+ pt_base', level', global', ext_ptw)
+ }
+ else
+ // level 0 PTE, but contains a pointer instead of a leaf
+ PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
+ }
+ else {
+ // Leaf PTE
+ let ext_pte = msbs_of_PTE(sv_params, pte);
+ let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags,
+ ext_pte, ext_ptw);
+ match pte_check {
+ PTE_Check_Failure(ext_ptw, ext_ptw_fail) =>
+ PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw),
+ PTE_Check_Success(ext_ptw) =>
+ if level > 0 then {
+ // Superpage; construct mask for lower-level PPNs from the PTE
+ let mask_bits = level * sv_params.pte_PPN_j_size_bits;
+ // Clear the lowest `mask_bits` bits.
+ let ppns_masked = (ppns >> mask_bits) << mask_bits;
+ if not(ppns == ppns_masked) then
+ // misaligned superpage mapping
+ PTW_Failure(PTW_Misaligned(), ext_ptw)
+ else {
+ // Compose final PA in superpage:
+ // Superpage PPN + lower VPNs + pagesize_bits page-offset
+ let mask : bits(64) = ~ (ones() << mask_bits);
+ let ppn = ppns | (vpns_of_va(sv_params, va) & mask);
+ let pa = (ppn << pagesize_bits) | zero_extend(offset_of_va(va));
+ PTW_Success(pa, pte, pte_addr, level, global', ext_ptw)
+ }
+ }
+ else {
+ let pa = (ppns << pagesize_bits) | zero_extend(offset_of_va(va));
+ PTW_Success(pa, pte, pte_addr, level, global', ext_ptw)
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+// ****************************************************************
+// Architectural SATP CSR
+
+// PUBLIC: see also riscv_insts_zicsr.sail and other CSR-related files
+register satp : xlenbits
+
+// See riscv_sys_regs.sail for legalize_satp{32,64}().
+// WARNING: those functions legalize Mode but not ASID?
+// PUBLIC: invoked from writeCSR() to fixup WARL fields
+function legalize_satp(a : Architecture,
+ o : xlenbits, // previous value of satp
+ v : xlenbits) // proposed new value of satp
+ -> xlenbits = { // new legal value of satp
+ if sizeof(xlen) == 32 then {
+ // The slice and extend ops below are no-ops when xlen==32,
+ // but appease the type-checker when xlen==64 (when this code is not executed!)
+ let o32 : bits(32) = o[31 .. 0];
+ let v32 : bits(32) = v[31 .. 0];
+ let new_satp : bits(32) = legalize_satp32(a, o32, v32);
+ zero_extend(new_satp);
+ } else if sizeof(xlen) == 64 then {
+ // The extend and truncate ops below are no-ops when xlen==64,
+ // but appease the type-checker when xlen==32 (when this code is not executed!)
+ let o64 : bits(64) = zero_extend(o);
+ let v64 : bits(64) = zero_extend(v);
+ let new_satp : bits(64) = legalize_satp64(a, o64, v64);
+ truncate(new_satp, sizeof(xlen))
+ } else
+ internal_error(__FILE__, __LINE__, "Unsupported xlen" ^ dec_str(sizeof(xlen)))
+}
+
+// ----------------
+// Fields of SATP
+
+// ASID is 9b in Sv32, 16b in Sv39/Sv48/Sv57: we use 16b for both
+// PRIVATE
+function satp_to_asid(satp_val : xlenbits) -> asidbits =
+ if sizeof(xlen) == 32 then zero_extend(Mk_Satp32(satp_val)[Asid])
+ else if sizeof(xlen) == 64 then Mk_Satp64(satp_val)[Asid]
+ else internal_error(__FILE__, __LINE__,
+ "Unsupported xlen" ^ dec_str(sizeof(xlen)))
+
+// Result is 64b to cover both RV32 and RV64 addrs
+// PRIVATE
+function satp_to_PT_base(satp_val : xlenbits) -> bits(64) = {
+ let ppn = if sizeof(xlen) == 32 then zero_extend (64, Mk_Satp32(satp_val)[PPN])
+ else if sizeof(xlen) == 64 then zero_extend (64, Mk_Satp64(satp_val)[PPN])
+ else internal_error(__FILE__, __LINE__,
+ "Unsupported xlen" ^ dec_str(sizeof(xlen)));
+ ppn << pagesize_bits
+}
+
+// Compute address translation mode from SATP register
+// PRIVATE
+function translationMode(priv : Privilege) -> SATPMode = {
+ if priv == Machine then
+ Sbare
+ else if sizeof(xlen) == 32 then
+ match Mk_Satp32(satp)[Mode] {
+ 0b0 => Sbare,
+ 0b1 => Sv32
+ }
+ else if sizeof(xlen) == 64 then {
+ // Translation mode is based on mstatus.SXL, which could be RV32 when xlen==64
+ let arch = architecture(get_mstatus_SXL(mstatus));
+ match arch {
+ Some(RV64) => { let mbits : bits(4) = satp[63 .. 60];
+ match satp64Mode_of_bits(RV64, mbits) { // see riscv_types.sail
+ Some(m) => m,
+ None() => internal_error(__FILE__, __LINE__,
+ "invalid RV64 translation mode in satp")
+ }
+ },
+ Some(RV32) => match Mk_Satp32(satp[31 .. 0])[Mode] { // Note: satp is 64bits here
+ // When xlen is 64, mstatus.SXL (for S privilege) can be RV32
+ 0b0 => Sbare,
+ 0b1 => Sv32
+ },
+ _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch")
+ }
+ }
+ else
+ internal_error(__FILE__, __LINE__, "unsupported xlen")
+}
+
+// ****************************************************************
+// VA to PA translation
+
+// Result of address translation
+
+// PUBLIC
+union TR_Result('paddr : Type, 'failure : Type) = {
+ TR_Address : ('paddr, ext_ptw),
+ TR_Failure : ('failure, ext_ptw)
+}
+
+// This function can be ignored on first reading since TLBs are not
+// part of RISC-V architecture spec (see TLB_NOTE above).
+// PRIVATE: translate on TLB hit, and maintenance of PTE in TLB
+function translate_TLB_hit(sv_params : SV_Params,
+ asid : asidbits,
+ ptb : bits(64),
+ vAddr : bits(64),
+ ac : AccessType(ext_access_type),
+ priv : Privilege,
+ mxr : bool,
+ do_sum : bool,
+ ext_ptw : ext_ptw,
+ tlb_index : nat,
+ ent : TLB_Entry)
+ -> TR_Result(bits(64), PTW_Error) = {
+ let pte = ent.pte;
+ let ext_pte = msbs_of_PTE(sv_params, pte);
+ let pte_flags = Mk_PTE_Flags(pte[7 .. 0]);
+ let pte_check = check_PTE_permission(ac, priv, mxr, do_sum, pte_flags,
+ ext_pte,
+ ext_ptw);
+ match pte_check {
+ PTE_Check_Failure(ext_ptw, ext_ptw_fail) =>
+ TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw),
+ PTE_Check_Success(ext_ptw) =>
+ match update_PTE_Bits(sv_params, pte, ac) {
+ None() => TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw),
+ Some(pte') =>
+ // See riscv_platform.sail
+ if not(plat_enable_dirty_update()) then
+ // pte needs dirty/accessed update but that is not enabled
+ TR_Failure(PTW_PTE_Update(), ext_ptw)
+ else {
+ // Writeback the PTE (which has new A/D bits)
+ let n_ent = {ent with pte=pte'};
+ write_TLB(tlb_index, n_ent);
+ let pte_phys_addr = ent.pteAddr[(sizeof(xlen) - 1) .. 0];
+ let mv = mem_write_value_priv(pte_phys_addr,
+ 8,
+ pte',
+ Supervisor,
+ false,
+ false,
+ false);
+ match mv {
+ MemValue(_) => (),
+ MemException(e) => internal_error(__FILE__, __LINE__,
+ "invalid physical address in TLB")
+ };
+ TR_Address(ent.pAddr | (vAddr & ent.vAddrMask), ext_ptw)
+ }
+ }
+ }
+}
+
+// PRIVATE: translate on TLB miss (do a page-table walk)
+function translate_TLB_miss(sv_params : SV_Params,
+ asid : asidbits,
+ ptb : bits(64),
+ vAddr : bits(64),
+ ac : AccessType(ext_access_type),
+ priv : Privilege,
+ mxr : bool,
+ do_sum : bool,
+ ext_ptw : ext_ptw) -> TR_Result(bits(64), PTW_Error) = {
+ let initial_level = sv_params.levels - 1;
+ let ptw_result = pt_walk(sv_params, vAddr, ac, priv, mxr, do_sum,
+ ptb, initial_level, false, ext_ptw);
+ match ptw_result {
+ PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
+ PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => {
+ let ext_pte = msbs_of_PTE(sv_params, pte);
+ // Without TLBs, this 'match' expression can be replaced simply
+ // by: 'TR_Address(pAddr, ext_ptw)' (see TLB_NOTE above)
+ match update_PTE_Bits(sv_params, pte, ac) {
+ None() => {
+ add_to_TLB(asid, vAddr, pAddr, pte, pteAddr, level, global,
+ sv_params.vpn_size_bits,
+ pagesize_bits);
+ TR_Address(pAddr, ext_ptw)
+ },
+ Some(pte') =>
+ // See riscv_platform.sail
+ if not(plat_enable_dirty_update()) then
+ // pte needs dirty/accessed update but that is not enabled
+ TR_Failure(PTW_PTE_Update(), ext_ptw)
+ else {
+ // Writeback the PTE (which has new A/D bits)
+ let pte_phys_addr = pteAddr[(sizeof(xlen) - 1) .. 0];
+ let mv = mem_write_value_priv(pte_phys_addr, // pteAddr,
+ 8,
+ pte',
+ Supervisor,
+ false,
+ false,
+ false);
+ match mv {
+ MemValue(_) => {
+ add_to_TLB(asid, vAddr, pAddr, pte', pteAddr, level, global,
+ sv_params.vpn_size_bits,
+ pagesize_bits);
+ TR_Address(pAddr, ext_ptw)
+ },
+ MemException(e) =>
+ TR_Failure(PTW_Access(), ext_ptw)
+ }
+ }
+ }
+ }
+ }
+}
+
+// PRIVATE
+function translate(sv_params : SV_Params,
+ asid : asidbits,
+ ptb : bits(64),
+ vAddr_arg : bits(64),
+ ac : AccessType(ext_access_type),
+ priv : Privilege,
+ mxr : bool,
+ do_sum : bool,
+ ext_ptw : ext_ptw)
+ -> TR_Result(bits(64), PTW_Error) = {
+ let va_mask : bits(64) = zero_extend(ones(sv_params.va_size_bits));
+ let vAddr = (vAddr_arg & va_mask);
+
+ // On first reading, assume lookup_TLB returns None(), since TLBs
+ // are not part of RISC-V archticture spec (see TLB_NOTE above)
+ match lookup_TLB(asid, vAddr) {
+ Some(index, ent) => translate_TLB_hit(sv_params, asid, ptb, vAddr, ac, priv,
+ mxr, do_sum, ext_ptw, index, ent),
+ None() => translate_TLB_miss(sv_params, asid, ptb, vAddr, ac, priv,
+ mxr, do_sum, ext_ptw)
+ }
+}
+
+// Top-level addr-translation function
+// PUBLIC: invoked from instr-fetch and load/store/amo
+function translateAddr(vAddr : xlenbits,
+ ac : AccessType(ext_access_type))
+ -> TR_Result(xlenbits, ExceptionType) = {
+ // Internally the vmem code works with 64-bit values, whether xlen==32 or xlen==64
+ // This 'extend' is a no-op when xlen==64 and extends when xlen==32
+ let vAddr_64b : bits(64) = zero_extend(vAddr);
+ // Effective privilege takes into account mstatus.PRV, mstatus.MPP
+ // See riscv_sys_regs.sail for effectivePrivilege() and cur_privilege
+ let effPriv : Privilege = effectivePrivilege(ac, mstatus, cur_privilege);
+ let mode : SATPMode = translationMode(effPriv);
+ let (valid_va, sv_params) : (bool, SV_Params) = match mode {
+ Sbare => return TR_Address(vAddr, init_ext_ptw),
+ Sv32 => (true, sv32_params),
+ Sv39 => (is_valid_vAddr(sv39_params, vAddr_64b), sv39_params),
+ Sv48 => (is_valid_vAddr(sv48_params, vAddr_64b), sv48_params),
+ // Sv57 => (is_valid_vAddr(sv57_params, vAddr_64b), sv57_params), // TODO
+ };
+ if not(valid_va) then
+ TR_Failure(translationException(ac, PTW_Invalid_Addr()), init_ext_ptw)
+ else {
+ let mxr = mstatus.MXR() == 0b1;
+ let do_sum = mstatus.SUM() == 0b1;
+ let asid : asidbits = satp_to_asid(satp);
+ let ptb : bits(64) = satp_to_PT_base(satp);
+ let tr_result1 = translate(sv_params,
+ asid,
+ ptb,
+ vAddr_64b,
+ ac, effPriv, mxr, do_sum,
+ init_ext_ptw);
+ // Fixup result PA or exception
+ match tr_result1 {
+ TR_Address(pa, ext_ptw) => TR_Address(truncate(pa, sizeof(xlen)), ext_ptw),
+ TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw)
+ }
+ }
+}
+
+// ****************************************************************
+// Initialize Virtual Memory state
+
+// PUBLIC: invoked from init_model()
+function init_vmem() -> unit = init_TLB()
+
+// ****************************************************************
diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail
index 375dfa3..d17cb02 100644
--- a/model/riscv_vmem_common.sail
+++ b/model/riscv_vmem_common.sail
@@ -6,162 +6,109 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
-/* Shared definitions for supervisor-mode page-table-entries and permission checks.
- *
- * These definitions are independent of xlen and do not involve
- * accessing physical memory.
- */
-
-/* PageSize */
-
-let PAGESIZE_BITS = 12
-
-/*
- * Definitions for RV32, which has a single address translation mode: Sv32.
- */
-
-type vaddr32 = bits(32)
-type paddr32 = bits(34)
-type pte32 = bits(32)
-
-/* asid */
-type asid32 = bits(9)
-
-function curAsid32(satp : bits(32)) -> asid32 = {
- let s = Mk_Satp32(satp);
- s[Asid]
-}
-
-/* page table base from satp */
-function curPTB32(satp : bits(32)) -> paddr32 = {
- let s : Satp32 = Mk_Satp32(satp);
- shiftl(zero_extend(s[PPN]), PAGESIZE_BITS)
+// ****************************************************************
+// Parameters for VM modes sv32, sv39, sv48 and (TODO) Sv57
+
+// All VM modes use the same page size (4KB, with 12-bit index)
+
+// This two-line idiom constrains the value (2nd line) to be a singleton,
+// which helps in type-checking wherever it is used.
+type PAGESIZE_BITS : Int = 12
+let pagesize_bits = sizeof(PAGESIZE_BITS)
+
+// PRIVATE
+struct SV_Params = {
+ // VA
+ va_size_bits : {32, 39, 48}, // 32 39 48
+ vpn_size_bits : {10, 9}, // 10 9 9
+
+ // PTE
+ levels : { 2, 3, 4}, // 2 3 4
+ log_pte_size_bytes : { 2, 3}, // 2 3 3
+ pte_msbs_lsb_index : {32, 54}, // 32 54 54
+ pte_msbs_size_bits : { 0, 10}, // 0 10 10
+ pte_PPNs_lsb_index : {10}, // 10 10 10
+ pte_PPNs_size_bits : {22, 44}, // 22 44 44
+ pte_PPN_j_size_bits : {10, 9} // 10 9 9
}
-/* Sv32 parameters and bitfield layouts */
-
-let SV32_LEVEL_BITS = 10
-let SV32_LEVELS = 2
-let PTE32_LOG_SIZE = 2
-let PTE32_SIZE = 4
-
-bitfield SV32_Vaddr : vaddr32 = {
- VPNi : 31 .. 12,
- PgOfs : 11 .. 0
+// Current level during a page-table walk (0 to SV_Params.levels - 1)
+type PTW_Level = range(0,3) // range(0,4) when add Sv57 (TODO)
+
+// PRIVATE
+let sv32_params : SV_Params = struct {
+ // VA
+ va_size_bits = 32,
+ vpn_size_bits = 10,
+
+ // PTE
+ levels = 2,
+ log_pte_size_bytes = 2, // 4 Bytes
+ pte_msbs_lsb_index = 32,
+ pte_msbs_size_bits = 0,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 22,
+ pte_PPN_j_size_bits = 10
}
-bitfield SV32_Paddr : paddr32 = {
- PPNi : 33 .. 12,
- PgOfs : 11 .. 0
+// PRIVATE
+let sv39_params : SV_Params = struct {
+ // VA
+ va_size_bits = 39,
+ vpn_size_bits = 9,
+
+ // PTE
+ levels = 3,
+ log_pte_size_bytes = 3, // 8 Bytes
+ pte_msbs_lsb_index = 54,
+ pte_msbs_size_bits = 10,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 44,
+ pte_PPN_j_size_bits = 9
}
-bitfield SV32_PTE : pte32 = {
- PPNi : 31 .. 10,
- RSW : 9 .. 8,
- BITS : 7 .. 0
+// PRIVATE
+let sv48_params : SV_Params = struct {
+ // VA
+ va_size_bits = 48,
+ vpn_size_bits = 9,
+
+ // PTE
+ levels = 4,
+ log_pte_size_bytes = 3, // 8 Bytes
+ pte_msbs_lsb_index = 54,
+ pte_msbs_size_bits = 10,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 44,
+ pte_PPN_j_size_bits = 9
}
+// TODO; not currently used
+// PRIVATE
/*
- * Definitions for RV64, which has two defined address translation modes: Sv39 and Sv48.
- */
-
-/* Sv48 and Sv64 are reserved but not defined. The size of the VPN
- * increases by 9 bits through Sv39, Sv48 and Sv57, but not for Sv64.
- * Also, the 45-bit size of the VPN for Sv57 exceeds the 44-bit size
- * of the PPN in satp64. Due to these corner cases, it is unlikely
- * that definitions can be shared across all four schemes, so separate
- * definitions might eventually be needed for each translation mode.
- *
- * But to keep things simple for now, since Sv39 and Sv48 have the
- * same PPN size, we share some definitions.
- */
-
-type paddr64 = bits(56)
-type pte64 = bits(64)
-
-/* asid */
-
-type asid64 = bits(16)
-
-function curAsid64(satp : bits(64)) -> asid64 = {
- let s = Mk_Satp64(satp);
- s[Asid]
-}
-
-/* page table base from satp */
-function curPTB64(satp : bits(64)) -> paddr64 = {
- let s = Mk_Satp64(satp);
- shiftl(zero_extend(s[PPN]), PAGESIZE_BITS)
-}
-
-/* Sv39 parameters and bitfield layouts */
-
-let SV39_LEVEL_BITS = 9
-let SV39_LEVELS = 3
-let PTE39_LOG_SIZE = 3
-let PTE39_SIZE = 8
-
-type vaddr39 = bits(39)
-
-bitfield SV39_Vaddr : vaddr39 = {
- VPNi : 38 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV39_Paddr : paddr64 = {
- PPNi : 55 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV39_PTE : pte64 = {
- Ext : 63 .. 54,
- PPNi : 53 .. 10,
- RSW : 9 .. 8,
- BITS : 7 .. 0
-}
-
-/* Sv48 parameters and bitfield layouts */
-
-let SV48_LEVEL_BITS = 9
-let SV48_LEVELS = 4
-let PTE48_LOG_SIZE = 3
-let PTE48_SIZE = 8
-
-type vaddr48 = bits(48)
-type pte48 = bits(64)
-
-bitfield SV48_Vaddr : vaddr48 = {
- VPNi : 47 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV48_Paddr : paddr64 = {
- PPNi : 55 .. 12,
- PgOfs : 11 .. 0
-}
-
-bitfield SV48_PTE : pte48 = {
- Ext : 63 .. 54,
- PPNi : 53 .. 10,
- RSW : 9 .. 8,
- BITS : 7 .. 0
-}
-
-/* The types below are parameterized by 'paddr and 'pte to support
- * various architectural widths (e.g. RV32, RV64). ext_ptw supports
- * extensions to the default address translation and page-table-walk.
- */
-
-/* Result of a page-table walk. */
-
-union PTW_Result('paddr : Type, 'pte : Type) = {
- PTW_Success: ('paddr, 'pte, 'paddr, nat, bool, ext_ptw),
- PTW_Failure: (PTW_Error, ext_ptw)
-}
-
-/* Result of address translation */
-
-union TR_Result('paddr : Type, 'failure : Type) = {
- TR_Address : ('paddr, ext_ptw),
- TR_Failure : ('failure, ext_ptw)
+let sv57_params : SV_Params = struct {
+ // VA
+ va_size_bits = 57,
+ vpn_size_bits = 9,
+
+ // PTE
+ levels = 5,
+ log_pte_size_bytes = 3, // 8 Bytes
+ pte_msbs_lsb_index = 54,
+ pte_msbs_size_bits = 10,
+ pte_PPNs_lsb_index = 10,
+ pte_PPNs_size_bits = 44,
+ pte_PPN_j_size_bits = 9
}
+*/
+
+// This 'undefined_SV_Params()' function is not used anywhere, but is
+// currently (2023-12) needed to work around an issue where Sail tries
+// to figure out how it could do
+// let x : SV_Params = undefined
+// even though the code never does this. This has been fixed in Sail.
+// The fix will become available in a new Sail release, at which point
+// this function can be deleted (TODO).
+// PRIVATE
+val undefined_SV_Params : unit -> SV_Params
+function undefined_SV_Params() = sv32_params
diff --git a/model/riscv_vmem_pte.sail b/model/riscv_vmem_pte.sail
new file mode 100644
index 0000000..dfe032c
--- /dev/null
+++ b/model/riscv_vmem_pte.sail
@@ -0,0 +1,135 @@
+/*=======================================================================================*/
+/* This Sail RISC-V architecture model, comprising all files and */
+/* directories except where otherwise noted is subject the BSD */
+/* two-clause license in the LICENSE file. */
+/* */
+/* SPDX-License-Identifier: BSD-2-Clause */
+/*=======================================================================================*/
+
+// ****************************************************************
+// PTE (Page Table Entry) in PTN (Page Table Node)
+
+// PTE MSBs PPNs RSW BITs
+// Sv32 - 31..10 9..8 7..0
+// Sv39 63..54 53..10 9..8 7..0
+// Sv48 63..54 53..10 9..8 7..0
+
+// MSBs of PTE are reserved for RV64 extensions.
+// There are not available bits on RV32, so these bits will be zeros on RV32.
+
+type pte_flags_bits = bits(8)
+
+// For PTW extensions (non-standard)
+type extPte = bits(64)
+
+// PRIVATE: extract msbs of PTE above the PPN
+function msbs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = {
+ let mask : bits(64) = zero_extend(ones(sv_params.pte_msbs_size_bits));
+ (pte >> sv_params.pte_msbs_lsb_index) & mask
+}
+
+// PRIVATE: extract PPNs of PTE
+function PPNs_of_PTE(sv_params : SV_Params, pte : bits(64)) -> bits(64) = {
+ let mask : bits(64) = zero_extend(ones(sv_params.pte_PPNs_size_bits));
+ (pte >> sv_params.pte_PPNs_lsb_index) & mask
+}
+
+// PRIVATE: 8 LSBs of PTEs in Sv32, Sv39, Sv48 and Sv57
+bitfield PTE_Flags : pte_flags_bits = {
+ D : 7, // dirty
+ A : 6, // accessed
+ G : 5, // global
+ U : 4, // User
+ X : 3, // Execute permission
+ W : 2, // Write permission
+ R : 1, // Read permission
+ V : 0 // Valid
+}
+
+// PRIVATE: check if a PTE is a pointer to next level (non-leaf)
+function pte_is_ptr(pte_flags : PTE_Flags) -> bool = (pte_flags[X] == 0b0)
+ & (pte_flags[W] == 0b0)
+ & (pte_flags[R] == 0b0)
+
+// PRIVATE: check if a PTE is valid
+function pte_is_invalid(pte_flags : PTE_Flags) -> bool = (pte_flags[V] == 0b0)
+ | ((pte_flags[W] == 0b1)
+ & (pte_flags[R] == 0b0))
+
+// ----------------
+// Check access permissions in PTE
+
+// For (non-standard) extensions: this function gets the extension-available bits
+// of the PTE in extPte, and the accumulated information of the page-table-walk
+// in ext_ptw. It should return the updated ext_ptw in both success and failure cases.
+
+union PTE_Check = {
+ PTE_Check_Success : ext_ptw,
+ PTE_Check_Failure : (ext_ptw, ext_ptw_fail)
+}
+
+// PRIVATE
+function check_PTE_permission(ac : AccessType(ext_access_type),
+ priv : Privilege,
+ mxr : bool,
+ do_sum : bool,
+ pte_flags : PTE_Flags,
+ ext : extPte,
+ ext_ptw : ext_ptw) -> PTE_Check = {
+ let pte_U = pte_flags[U];
+ let pte_R = pte_flags[R];
+ let pte_W = pte_flags[W];
+ let pte_X = pte_flags[X];
+ let success : bool =
+ match (ac, priv) {
+ (Read(_), User) => (pte_U == 0b1)
+ & ((pte_R == 0b1)
+ | ((pte_X == 0b1 & mxr))),
+ (Write(_), User) => (pte_U == 0b1) & (pte_W == 0b1),
+ (ReadWrite(_, _), User) => (pte_U == 0b1)
+ & (pte_W == 0b1)
+ & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)),
+ (Execute(), User) => (pte_U == 0b1) & (pte_X == 0b1),
+ (Read(_), Supervisor) => ((pte_U == 0b0) | do_sum)
+ & ((pte_R == 0b1) | ((pte_X == 0b1) & mxr)),
+ (Write(_), Supervisor) => ((pte_U == 0b0) | do_sum)
+ & (pte_W == 0b1),
+ (ReadWrite(_, _), Supervisor) => ((pte_U == 0b0) | do_sum)
+ & (pte_W == 0b1)
+ & ((pte_R == 0b1)
+ | ((pte_X == 0b1) & mxr)),
+ (Execute(), Supervisor) => (pte_U == 0b0) & (pte_X == 0b1),
+ (_, Machine) => internal_error(__FILE__, __LINE__,
+ "m-mode mem perm check")};
+ if success then PTE_Check_Success(())
+ else PTE_Check_Failure((), ())
+}
+
+// Update PTE bits if needed; return new PTE if updated
+// PRIVATE
+function update_PTE_Bits(sv_params : SV_Params,
+ pte : bits(64),
+ a : AccessType(ext_access_type))
+ -> option(bits(64)) = {
+ let pte_flags = Mk_PTE_Flags(pte [7 .. 0]);
+
+ // Update 'dirty' bit?
+ let update_d : bool = (pte_flags[D] == 0b0)
+ & (match a {
+ Execute() => false,
+ Read() => false,
+ Write(_) => true,
+ ReadWrite(_, _) => true
+ });
+ // Update 'accessed'-bit?
+ let update_a = (pte_flags[A] == 0b0);
+
+ if update_d | update_a then {
+ let pte_flags = [pte_flags with
+ A = 0b1,
+ D = (if update_d then 0b1 else pte_flags[D])];
+ Some(pte[63 .. 8] @ pte_flags.bits())
+ }
+ else
+ None()
+}
diff --git a/model/riscv_ptw.sail b/model/riscv_vmem_ptw.sail
index a880def..ab73b19 100644
--- a/model/riscv_ptw.sail
+++ b/model/riscv_vmem_ptw.sail
@@ -6,21 +6,27 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
-/* failure modes for address-translation/page-table-walks */
+// ****************************************************************
+// PTW exceptions
+// 'ext_ptw' supports (non-standard) extensions to the default addr-translation and PTW.
+// See riscv_types_ext.sail for definitions.
+
+// Failure modes for address-translation/page-table-walks
+// PRIVATE
union PTW_Error = {
- PTW_Invalid_Addr : unit, /* invalid source address */
- PTW_Access : unit, /* physical memory access error for a PTE */
+ PTW_Invalid_Addr : unit, // invalid source address
+ PTW_Access : unit, // physical memory access error for a PTE
PTW_Invalid_PTE : unit,
PTW_No_Permission : unit,
- PTW_Misaligned : unit, /* misaligned superpage */
- PTW_PTE_Update : unit, /* PTE update needed but not enabled */
- PTW_Ext_Error : ext_ptw_error /* parameterized for errors from extensions */
+ PTW_Misaligned : unit, // misaligned superpage
+ PTW_PTE_Update : unit, // PTE update needed but not enabled
+ PTW_Ext_Error : ext_ptw_error // parameterized for errors from extensions
}
-val ptw_error_to_str : PTW_Error -> string
-function ptw_error_to_str(e) =
- match (e) {
+// PRIVATE: only 'to_str' overload is public
+function ptw_error_to_str(e : PTW_Error) -> string = {
+ match e {
PTW_Invalid_Addr() => "invalid-source-addr",
PTW_Access() => "mem-access-error",
PTW_Invalid_PTE() => "invalid-pte",
@@ -29,19 +35,23 @@ function ptw_error_to_str(e) =
PTW_PTE_Update() => "pte-update-needed",
PTW_Ext_Error(e) => "extension-error"
}
+}
+// PUBLIC
overload to_str = {ptw_error_to_str}
-/* hook for extensions to customize errors reported by page-table
- * walks during address translation; it typically works in conjunction
- * with any customization to checkPTEPermission().
- */
+// hook for (non-standard) extensions to customize errors reported by page-table
+// walks during address translation; it typically works in conjunction
+// with any customization to check_PTE_permission().
+
+// PRIVATE
function ext_get_ptw_error(eptwf : ext_ptw_fail) -> PTW_Error =
PTW_No_Permission()
-/* conversion of these translation/PTW failures into architectural exceptions */
-function translationException(a : AccessType(ext_access_type), f : PTW_Error) -> ExceptionType = {
- let e : ExceptionType =
+// Convert translation/PTW failures into architectural exceptions
+function translationException(a : AccessType(ext_access_type),
+ f : PTW_Error)
+ -> ExceptionType = {
match (a, f) {
(_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)),
(ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(),
@@ -52,8 +62,5 @@ function translationException(a : AccessType(ext_access_type), f : PTW_Error) ->
(Write(_), _) => E_SAMO_Page_Fault(),
(Execute(), PTW_Access()) => E_Fetch_Access_Fault(),
(Execute(), _) => E_Fetch_Page_Fault()
- } in {
-/* print_mem("translationException(" ^ a ^ ", " ^ f ^ ") -> " ^ e); */
- e
}
}
diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail
deleted file mode 100644
index 33cc9c1..0000000
--- a/model/riscv_vmem_rv32.sail
+++ /dev/null
@@ -1,75 +0,0 @@
-/*=======================================================================================*/
-/* This Sail RISC-V architecture model, comprising all files and */
-/* directories except where otherwise noted is subject the BSD */
-/* two-clause license in the LICENSE file. */
-/* */
-/* SPDX-License-Identifier: BSD-2-Clause */
-/*=======================================================================================*/
-
-/* RV32 Supervisor-mode address translation and page-table walks. */
-
-/* Define the architectural satp and its legalizer. */
-
-register satp : xlenbits
-
-function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits =
- legalize_satp32(a, o, v)
-
-/* Compute the address translation mode. */
-
-val translationMode : (Privilege) -> SATPMode
-function translationMode(priv) = {
- if priv == Machine then Sbare
- else {
- let arch = architecture(get_mstatus_SXL(mstatus));
- match arch {
- Some(RV32) => {
- let s = Mk_Satp32(satp[31..0]);
- if s[Mode] == 0b0 then Sbare else Sv32
- },
- _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch")
- }
- }
-}
-
-/* Top-level address translation dispatcher */
-
-val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType)
-function translateAddr_priv(vAddr, ac, effPriv) = {
- let mxr : bool = mstatus[MXR] == 0b1;
- let do_sum : bool = mstatus[SUM] == 0b1;
- let mode : SATPMode = translationMode(effPriv);
-
- let asid = curAsid32(satp);
- let ptb = curPTB32(satp);
-
- /* PTW extensions: initialize the PTW extension state */
- let ext_ptw : ext_ptw = init_ext_ptw;
-
- match mode {
- Sbare => TR_Address(vAddr, ext_ptw),
- Sv32 => match translate32(asid, ptb, vAddr, ac, effPriv, mxr, do_sum, SV32_LEVELS - 1, ext_ptw) {
- TR_Address(pa, ext_ptw) => TR_Address(to_phys_addr(pa), ext_ptw),
- TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw)
- },
- _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme")
- }
-}
-
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType)
-function translateAddr(vAddr, ac) =
- translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege))
-
-val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit
-function flush_TLB(asid_xlen, addr_xlen) -> unit = {
- let asid : option(asid32) =
- match (asid_xlen) {
- None() => None(),
- Some(a) => Some(a[8 .. 0])
- };
- flush_TLB32(asid, addr_xlen)
-}
-
-function init_vmem () -> unit = {
- init_vmem_sv32()
-}
diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail
deleted file mode 100644
index 9ead642..0000000
--- a/model/riscv_vmem_rv64.sail
+++ /dev/null
@@ -1,114 +0,0 @@
-/*=======================================================================================*/
-/* This Sail RISC-V architecture model, comprising all files and */
-/* directories except where otherwise noted is subject the BSD */
-/* two-clause license in the LICENSE file. */
-/* */
-/* SPDX-License-Identifier: BSD-2-Clause */
-/*=======================================================================================*/
-
-/* RV64 Supervisor-mode address translation and page-table walks. */
-
-/* Define the architectural satp and its legalizer. */
-
-register satp : xlenbits
-
-function legalize_satp(a : Architecture, o : xlenbits, v : xlenbits) -> xlenbits =
- legalize_satp64(a, o, v)
-
-/* Define valid source addresses for translation */
-
-function isValidSv39Addr(vAddr : xlenbits) -> bool = {
- vAddr[63 .. 39] == (if vAddr[38] == bitone
- then ones()
- else zeros())
-}
-
-function isValidSv48Addr(vAddr : xlenbits) -> bool = {
- vAddr[63 .. 48] == (if vAddr[47] == bitone
- then ones()
- else zeros())
-}
-
-/* Compute the address translation mode. */
-
-val translationMode : (Privilege) -> SATPMode
-function translationMode(priv) = {
- if priv == Machine then Sbare
- else {
- let arch = architecture(get_mstatus_SXL(mstatus));
- match arch {
- Some(RV64) => {
- let mbits : satp_mode = Mk_Satp64(satp)[Mode];
- match satp64Mode_of_bits(RV64, mbits) {
- Some(m) => m,
- None() => internal_error(__FILE__, __LINE__, "invalid RV64 translation mode in satp")
- }
- },
- Some(RV32) => {
- let s = Mk_Satp32(satp[31..0]);
- if s[Mode] == 0b0 then Sbare else Sv32
- },
- _ => internal_error(__FILE__, __LINE__, "unsupported address translation arch")
- }
- }
-}
-
-/* Top-level address translation dispatcher */
-
-val translateAddr_priv : (xlenbits, AccessType(ext_access_type), Privilege) -> TR_Result(xlenbits, ExceptionType)
-function translateAddr_priv(vAddr, ac, effPriv) = {
- let mxr : bool = mstatus[MXR] == 0b1;
- let do_sum : bool = mstatus[SUM] == 0b1;
- let mode : SATPMode = translationMode(effPriv);
-
- let asid = curAsid64(satp);
- let ptb = curPTB64(satp);
-
- /* PTW extensions: initialize the PTW extension state. */
- let ext_ptw : ext_ptw = init_ext_ptw;
-
- match mode {
- Sbare => TR_Address(vAddr, ext_ptw),
- Sv39 => { if isValidSv39Addr(vAddr)
- then match translate39(asid, ptb, vAddr[38 .. 0], ac, effPriv, mxr, do_sum, SV39_LEVELS - 1, ext_ptw) {
- TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw),
- TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw)
- }
- else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw)
- },
- Sv48 => { if isValidSv48Addr(vAddr)
- then match translate48(asid, ptb, vAddr[47 .. 0], ac, effPriv, mxr, do_sum, SV48_LEVELS - 1, ext_ptw) {
- TR_Address(pa, ext_ptw) => TR_Address(zero_extend(pa), ext_ptw),
- TR_Failure(f, ext_ptw) => TR_Failure(translationException(ac, f), ext_ptw)
- }
- else TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw)
- },
- _ => internal_error(__FILE__, __LINE__, "unsupported address translation scheme")
- }
-}
-
-val translateAddr : (xlenbits, AccessType(ext_access_type)) -> TR_Result(xlenbits, ExceptionType)
-function translateAddr(vAddr, ac) =
- translateAddr_priv(vAddr, ac, effectivePrivilege(ac, mstatus, cur_privilege))
-
-val flush_TLB : (option(xlenbits), option(xlenbits)) -> unit
-function flush_TLB(asid_xlen, addr_xlen) -> unit = {
- /* Flush both Sv39 and Sv48 TLBs. */
- let (addr39, addr48) : (option(vaddr39), option(vaddr48)) =
- match addr_xlen {
- None() => (None(), None()),
- Some(a) => (Some(a[38 .. 0]), Some(a[47 .. 0]))
- };
- let asid : option(asid64) =
- match asid_xlen {
- None() => None(),
- Some(a) => Some(a[15 .. 0])
- };
- flush_TLB39(asid, addr39);
- flush_TLB48(asid, addr48)
-}
-
-function init_vmem() -> unit = {
- init_vmem_sv39();
- init_vmem_sv48()
-}
diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail
deleted file mode 100644
index 1de109c..0000000
--- a/model/riscv_vmem_sv32.sail
+++ /dev/null
@@ -1,200 +0,0 @@
-/*=======================================================================================*/
-/* This Sail RISC-V architecture model, comprising all files and */
-/* directories except where otherwise noted is subject the BSD */
-/* two-clause license in the LICENSE file. */
-/* */
-/* SPDX-License-Identifier: BSD-2-Clause */
-/*=======================================================================================*/
-
-/* Sv32 address translation for RV32. */
-
-/* FIXME: paddr32 is 34-bits, but phys_mem accesses in riscv_mem take 32-bit (xlenbits) addresses.
- * Define a converter for now.
- */
-
-function to_phys_addr(a : paddr32) -> xlenbits = a[31..0]
-
-val walk32 : (vaddr32, AccessType(ext_access_type), Privilege, bool, bool, paddr32, nat, bool, ext_ptw) -> PTW_Result(paddr32, SV32_PTE)
-function walk32(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
- let va = Mk_SV32_Vaddr(vaddr);
- let pt_ofs : paddr32 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV32_LEVEL_BITS))[(SV32_LEVEL_BITS - 1) .. 0]),
- PTE32_LOG_SIZE);
- let pte_addr = ptb + pt_ofs;
- match (mem_read_priv(Read(Data), Supervisor, to_phys_addr(pte_addr), 4, false, false, false)) {
- MemException(_) => {
-/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
- ^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
- ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
- ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))
- ^ ": invalid pte address"); */
- PTW_Failure(PTW_Access(), ext_ptw)
- },
- MemValue(v) => {
- let pte = Mk_SV32_PTE(v);
- let pbits = pte[BITS];
- let ext_pte : extPte = default_sv32_ext_pte;
- let pattr = Mk_PTE_Bits(pbits);
- let is_global = global | (pattr[G] == 0b1);
-/* print("walk32(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
- ^ " pt_base=" ^ BitStr(to_phys_addr(ptb))
- ^ " pt_ofs=" ^ BitStr(to_phys_addr(pt_ofs))
- ^ " pte_addr=" ^ BitStr(to_phys_addr(pte_addr))
- ^ " pte=" ^ BitStr(v)); */
- if isInvalidPTE(pbits, ext_pte) then {
-/* print("walk32: invalid pte"); */
- PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- } else {
- if isPTEPtr(pbits, ext_pte) then {
- if level > 0 then {
- /* walk down the pointer to the next level */
- walk32(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
- } else {
- /* last-level PTE contains a pointer instead of a leaf */
-/* print("walk32: last-level pte contains a ptr"); */
- PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- }
- } else { /* leaf PTE */
- match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
- PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
-/* print("walk32: pte permission check failure"); */
- PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
- },
- PTE_Check_Success(ext_ptw) => {
- if level > 0 then { /* superpage */
- /* fixme hack: to get a mask of appropriate size */
- let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV32_LEVEL_BITS) - 1;
- if (pte[PPNi] & mask) != zero_extend(0b0) then {
- /* misaligned superpage mapping */
-/* print("walk32: misaligned superpage mapping"); */
- PTW_Failure(PTW_Misaligned(), ext_ptw)
- } else {
- /* add the appropriate bits of the VPN to the superpage PPN */
- let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask);
-/* let res = append(ppn, va[PgOfs]);
- print("walk32: using superpage: pte.ppn=" ^ BitStr(pte[PPNi])
- ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
- PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw)
- }
- } else {
- /* normal leaf PTE */
-/* let res = append(pte[PPNi], va[PgOfs]);
- print("walk32: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */
- PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw)
- }
- }
- }
- }
- }
- }
- }
-}
-
-/* TLB management: single entry for now */
-
-// ideally we would use the below form:
-// type TLB32_Entry = TLB_Entry(sizeof(asid32), sizeof(vaddr32), sizeof(paddr32), sizeof(pte32))
-type TLB32_Entry = TLB_Entry(9, 32, 34, 32)
-register tlb32 : option(TLB32_Entry)
-
-val lookup_TLB32 : (asid32, vaddr32) -> option((nat, TLB32_Entry))
-function lookup_TLB32(asid, vaddr) =
- match tlb32 {
- None() => None(),
- Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
- }
-
-val add_to_TLB32 : (asid32, vaddr32, paddr32, SV32_PTE, paddr32, nat, bool) -> unit
-function add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
- let ent : TLB32_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV32_LEVEL_BITS);
- tlb32 = Some(ent)
-}
-
-function write_TLB32(idx : nat, ent : TLB32_Entry) -> unit =
- tlb32 = Some(ent)
-
-val flush_TLB32 : (option(asid32), option(vaddr32)) -> unit
-function flush_TLB32(asid, addr) =
- match (tlb32) {
- None() => (),
- Some(e) => if flush_TLB_Entry(e, asid, addr)
- then tlb32 = None()
- else ()
- }
-
-/* address translation */
-
-val translate32 : (asid32, paddr32, vaddr32, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr32, PTW_Error)
-function translate32(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
- match lookup_TLB32(asid, vAddr) {
- Some(idx, ent) => {
-/* print("translate32: TLB32 hit for " ^ BitStr(vAddr)); */
- let pte = Mk_SV32_PTE(ent.pte);
- let ext_pte : extPte = zeros(); // no reserved bits for extensions
- let pteBits = Mk_PTE_Bits(pte[BITS]);
- match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {
- PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) },
- PTE_Check_Success(ext_ptw) => {
- match update_PTE_Bits(pteBits, ac, ext_pte) {
- None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw),
- Some(pbits, ext) => {
- if not(plat_enable_dirty_update())
- then {
- /* pte needs dirty/accessed update but that is not enabled */
- TR_Failure(PTW_PTE_Update(), ext_ptw)
- } else {
- /* update PTE entry and TLB */
- n_pte = update_BITS(pte, pbits.bits);
- /* ext is unused since there are no reserved bits for extensions */
- n_ent : TLB32_Entry = ent;
- n_ent.pte = n_pte.bits;
- write_TLB32(idx, n_ent);
- /* update page table */
- match mem_write_value_priv(to_phys_addr(zero_extend(ent.pteAddr)), 4, n_pte.bits, Supervisor, false, false, false) {
- MemValue(_) => (),
- MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB")
- };
- TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw)
- }
- }
- }
- }
- }
- },
- None() => {
- match walk32(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {
- PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
- PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => {
- match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, zeros()) {
- None() => {
- add_to_TLB32(asid, vAddr, pAddr, pte, pteAddr, level, global);
- TR_Address(pAddr, ext_ptw)
- },
- Some(pbits, ext) =>
- if not(plat_enable_dirty_update())
- then {
- /* pte needs dirty/accessed update but that is not enabled */
- TR_Failure(PTW_PTE_Update(), ext_ptw)
- } else {
- var w_pte : SV32_PTE = update_BITS(pte, pbits.bits);
- /* ext is unused since there are no reserved bits for extensions */
- match mem_write_value_priv(to_phys_addr(pteAddr), 4, w_pte.bits, Supervisor, false, false, false) {
- MemValue(_) => {
- add_to_TLB32(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
- TR_Address(pAddr, ext_ptw)
- },
- MemException(e) => {
- /* pte is not in valid memory */
- TR_Failure(PTW_Access(), ext_ptw)
- }
- }
- }
- }
- }
- }
- }
- }
-}
-
-function init_vmem_sv32() -> unit = {
- tlb32 = None()
-}
diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail
deleted file mode 100644
index 68f3d55..0000000
--- a/model/riscv_vmem_sv39.sail
+++ /dev/null
@@ -1,194 +0,0 @@
-/*=======================================================================================*/
-/* This Sail RISC-V architecture model, comprising all files and */
-/* directories except where otherwise noted is subject the BSD */
-/* two-clause license in the LICENSE file. */
-/* */
-/* SPDX-License-Identifier: BSD-2-Clause */
-/*=======================================================================================*/
-
-/* Sv39 address translation for RV64. */
-
-val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE)
-function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
- let va = Mk_SV39_Vaddr(vaddr);
- let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
- PTE39_LOG_SIZE);
- let pte_addr = ptb + pt_ofs;
- match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) {
- MemException(_) => {
-/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
- ^ " pt_base=" ^ BitStr(ptb)
- ^ " pt_ofs=" ^ BitStr(pt_ofs)
- ^ " pte_addr=" ^ BitStr(pte_addr)
- ^ ": invalid pte address"); */
- PTW_Failure(PTW_Access(), ext_ptw)
- },
- MemValue(v) => {
- let pte = Mk_SV39_PTE(v);
- let pbits = pte[BITS];
- let ext_pte = pte[Ext];
- let pattr = Mk_PTE_Bits(pbits);
- let is_global = global | (pattr[G] == 0b1);
-/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
- ^ " pt_base=" ^ BitStr(ptb)
- ^ " pt_ofs=" ^ BitStr(pt_ofs)
- ^ " pte_addr=" ^ BitStr(pte_addr)
- ^ " pte=" ^ BitStr(v)); */
- if isInvalidPTE(pbits, ext_pte) then {
-/* print("walk39: invalid pte"); */
- PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- } else {
- if isPTEPtr(pbits, ext_pte) then {
- if level > 0 then {
- /* walk down the pointer to the next level */
- walk39(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
- } else {
- /* last-level PTE contains a pointer instead of a leaf */
-/* print("walk39: last-level pte contains a ptr"); */
- PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- }
- } else { /* leaf PTE */
- match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
- PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
-/* print("walk39: pte permission check failure"); */
- PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
- },
- PTE_Check_Success(ext_ptw) => {
- if level > 0 then { /* superpage */
- /* fixme hack: to get a mask of appropriate size */
- let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV39_LEVEL_BITS) - 1;
- if (pte[PPNi] & mask) != zero_extend(0b0) then {
- /* misaligned superpage mapping */
-/* print("walk39: misaligned superpage mapping"); */
- PTW_Failure(PTW_Misaligned(), ext_ptw)
- } else {
- /* add the appropriate bits of the VPN to the superpage PPN */
- let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask);
-/* let res = append(ppn, va[PgOfs]);
- print("walk39: using superpage: pte.ppn=" ^ BitStr(pte[PPNi])
- ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
- PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw)
- }
- } else {
- /* normal leaf PTE */
-/* let res = append(pte[PPNi], va[PgOfs]);
- print("walk39: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */
- PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw)
- }
- }
- }
- }
- }
- }
- }
-}
-
-/* TLB management: single entry for now */
-
-// ideally we would use the below form:
-// type TLB39_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr39), sizeof(paddr64), sizeof(pte64))
-type TLB39_Entry = TLB_Entry(16, 39, 56, 64)
-register tlb39 : option(TLB39_Entry)
-
-val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry))
-function lookup_TLB39(asid, vaddr) =
- match tlb39 {
- None() => None(),
- Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
- }
-
-val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit
-function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
- let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV39_LEVEL_BITS);
- tlb39 = Some(ent)
-}
-
-function write_TLB39(idx : nat, ent : TLB39_Entry) -> unit =
- tlb39 = Some(ent)
-
-val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit
-function flush_TLB39(asid, addr) =
- match (tlb39) {
- None() => (),
- Some(e) => if flush_TLB_Entry(e, asid, addr)
- then tlb39 = None()
- else ()
- }
-
-/* address translation */
-
-val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error)
-function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
- match lookup_TLB39(asid, vAddr) {
- Some(idx, ent) => {
-/* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */
- let pte = Mk_SV39_PTE(ent.pte);
- let ext_pte = pte[Ext];
- let pteBits = Mk_PTE_Bits(pte[BITS]);
- match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {
- PTE_Check_Failure(ext_ptw, ext_ptw_fail) => { TR_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw) },
- PTE_Check_Success(ext_ptw) => {
- match update_PTE_Bits(pteBits, ac, ext_pte) {
- None() => TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw),
- Some(pbits, ext) => {
- if not(plat_enable_dirty_update())
- then {
- /* pte needs dirty/accessed update but that is not enabled */
- TR_Failure(PTW_PTE_Update(), ext_ptw)
- } else {
- /* update PTE entry and TLB */
- n_pte = update_BITS(pte, pbits.bits);
- n_pte = update_Ext(n_pte, ext);
- n_ent : TLB39_Entry = ent;
- n_ent.pte = n_pte.bits;
- write_TLB39(idx, n_ent);
- /* update page table */
- match mem_write_value_priv(zero_extend(ent.pteAddr), 8, n_pte.bits, Supervisor, false, false, false) {
- MemValue(_) => (),
- MemException(e) => internal_error(__FILE__, __LINE__, "invalid physical address in TLB")
- };
- TR_Address(ent.pAddr | zero_extend(vAddr & ent.vAddrMask), ext_ptw)
- }
- }
- }
- }
- }
- },
- None() => {
- match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {
- PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
- PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => {
- match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) {
- None() => {
- add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global);
- TR_Address(pAddr, ext_ptw)
- },
- Some(pbits, ext) =>
- if not(plat_enable_dirty_update())
- then {
- /* pte needs dirty/accessed update but that is not enabled */
- TR_Failure(PTW_PTE_Update(), ext_ptw)
- } else {
- var w_pte : SV39_PTE = update_BITS(pte, pbits.bits);
- w_pte = update_Ext(w_pte, ext);
- match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) {
- MemValue(_) => {
- add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
- TR_Address(pAddr, ext_ptw)
- },
- MemException(e) => {
- /* pte is not in valid memory */
- TR_Failure(PTW_Access(), ext_ptw)
- }
- }
- }
- }
- }
- }
- }
- }
-}
-
-function init_vmem_sv39() -> unit = {
- tlb39 = None()
-}
diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail
deleted file mode 100644
index 517450a..0000000
--- a/model/riscv_vmem_sv48.sail
+++ /dev/null
@@ -1,156 +0,0 @@
-/*=======================================================================================*/
-/* This Sail RISC-V architecture model, comprising all files and */
-/* directories except where otherwise noted is subject the BSD */
-/* two-clause license in the LICENSE file. */
-/* */
-/* SPDX-License-Identifier: BSD-2-Clause */
-/*=======================================================================================*/
-
-/* Sv48 address translation for RV64. */
-
-val walk48 : (vaddr48, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV48_PTE)
-function walk48(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = {
- let va = Mk_SV48_Vaddr(vaddr);
- let pt_ofs : paddr64 = shiftl(zero_extend(shiftr(va[VPNi], (level * SV48_LEVEL_BITS))[(SV48_LEVEL_BITS - 1) .. 0]),
- PTE48_LOG_SIZE);
- let pte_addr = ptb + pt_ofs;
- match (mem_read_priv(Read(Data), Supervisor, zero_extend(pte_addr), 8, false, false, false)) {
- MemException(_) => {
-/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
- ^ " pt_base=" ^ BitStr(ptb)
- ^ " pt_ofs=" ^ BitStr(pt_ofs)
- ^ " pte_addr=" ^ BitStr(pte_addr)
- ^ ": invalid pte address"); */
- PTW_Failure(PTW_Access(), ext_ptw)
- },
- MemValue(v) => {
- let pte = Mk_SV48_PTE(v);
- let pbits = pte[BITS];
- let ext_pte = pte[Ext];
- let pattr = Mk_PTE_Bits(pbits);
- let is_global = global | (pattr[G] == 0b1);
-/* print("walk48(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ dec_str(level)
- ^ " pt_base=" ^ BitStr(ptb)
- ^ " pt_ofs=" ^ BitStr(pt_ofs)
- ^ " pte_addr=" ^ BitStr(pte_addr)
- ^ " pte=" ^ BitStr(v)); */
- if isInvalidPTE(pbits, ext_pte) then {
-/* print("walk48: invalid pte"); */
- PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- } else {
- if isPTEPtr(pbits, ext_pte) then {
- if level > 0 then {
- /* walk down the pointer to the next level */
- walk48(vaddr, ac, priv, mxr, do_sum, shiftl(zero_extend(pte[PPNi]), PAGESIZE_BITS), level - 1, is_global, ext_ptw)
- } else {
- /* last-level PTE contains a pointer instead of a leaf */
-/* print("walk48: last-level pte contains a ptr"); */
- PTW_Failure(PTW_Invalid_PTE(), ext_ptw)
- }
- } else { /* leaf PTE */
- match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {
- PTE_Check_Failure(ext_ptw, ext_ptw_fail) => {
-/* print("walk48: pte permission check failure"); */
- PTW_Failure(ext_get_ptw_error(ext_ptw_fail), ext_ptw)
- },
- PTE_Check_Success(ext_ptw) => {
- if level > 0 then { /* superpage */
- /* fixme hack: to get a mask of appropriate size */
- let mask = shiftl(pte[PPNi] ^ pte[PPNi] ^ zero_extend(0b1), level * SV48_LEVEL_BITS) - 1;
- if (pte[PPNi] & mask) != zero_extend(0b0) then {
- /* misaligned superpage mapping */
-/* print("walk48: misaligned superpage mapping"); */
- PTW_Failure(PTW_Misaligned(), ext_ptw)
- } else {
- /* add the appropriate bits of the VPN to the superpage PPN */
- let ppn = pte[PPNi] | (zero_extend(va[VPNi]) & mask);
-/* let res = append(ppn, va[PgOfs]);
- print("walk48: using superpage: pte.ppn=" ^ BitStr(pte[PPNi])
- ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */
- PTW_Success(append(ppn, va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw)
- }
- } else {
- /* normal leaf PTE */
-/* let res = append(pte[PPNi], va[PgOfs]);
- print("walk48: pte.ppn=" ^ BitStr(pte[PPNi]) ^ " ppn=" ^ BitStr(pte[PPNi]) ^ " res=" ^ BitStr(res)); */
- PTW_Success(append(pte[PPNi], va[PgOfs]), pte, pte_addr, level, is_global, ext_ptw)
- }
- }
- }
- }
- }
- }
- }
-}
-
-/* TLB management: single entry for now */
-
-// ideally we would use the below form:
-// type TLB48_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr48), sizeof(paddr64), sizeof(pte64))
-type TLB48_Entry = TLB_Entry(16, 48, 56, 64)
-register tlb48 : option(TLB48_Entry)
-
-val lookup_TLB48 : (asid64, vaddr48) -> option((nat, TLB48_Entry))
-function lookup_TLB48(asid, vaddr) =
- match tlb48 {
- None() => None(),
- Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
- }
-
-val add_to_TLB48 : (asid64, vaddr48, paddr64, SV48_PTE, paddr64, nat, bool) -> unit
-function add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global) = {
- let ent : TLB48_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits, level, pteAddr, SV48_LEVEL_BITS);
- tlb48 = Some(ent)
-}
-
-function write_TLB48(idx : nat, ent : TLB48_Entry) -> unit =
- tlb48 = Some(ent)
-
-val flush_TLB48 : (option(asid64), option(vaddr48)) -> unit
-function flush_TLB48(asid, addr) =
- match (tlb48) {
- None() => (),
- Some(e) => if flush_TLB_Entry(e, asid, addr)
- then tlb48 = None()
- else ()
- }
-
-/* address translation */
-
-val translate48 : (asid64, paddr64, vaddr48, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error)
-function translate48(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = {
- match walk48(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {
- PTW_Failure(f, ext_ptw) => TR_Failure(f, ext_ptw),
- PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => {
- match update_PTE_Bits(Mk_PTE_Bits(pte[BITS]), ac, pte[Ext]) {
- None() => {
- add_to_TLB48(asid, vAddr, pAddr, pte, pteAddr, level, global);
- TR_Address(pAddr, ext_ptw)
- },
- Some(pbits, ext) =>
- if not(plat_enable_dirty_update())
- then {
- /* pte needs dirty/accessed update but that is not enabled */
- TR_Failure(PTW_PTE_Update(), ext_ptw)
- } else {
- var w_pte : SV48_PTE = update_BITS(pte, pbits.bits);
- w_pte = update_Ext(w_pte, ext);
- match mem_write_value_priv(zero_extend(pteAddr), 8, w_pte.bits, Supervisor, false, false, false) {
- MemValue(_) => {
- add_to_TLB48(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
- TR_Address(pAddr, ext_ptw)
- },
- MemException(e) => {
- /* pte is not in valid memory */
- TR_Failure(PTW_Access(), ext_ptw)
- }
- }
- }
- }
- }
- }
-}
-
-function init_vmem_sv48() -> unit = {
- tlb48 = None()
-}
diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail
index a0e51ca..828fa72 100644
--- a/model/riscv_vmem_tlb.sail
+++ b/model/riscv_vmem_tlb.sail
@@ -6,53 +6,51 @@
/* SPDX-License-Identifier: BSD-2-Clause */
/*=======================================================================================*/
-/* idealized generic TLB entry to model fence.vm and also speed up simulation. */
-
-struct TLB_Entry('asidlen: Int, 'valen: Int, 'palen: Int, 'ptelen: Int) = {
- asid : bits('asidlen),
- global : bool,
- vAddr : bits('valen), /* VPN */
- pAddr : bits('palen), /* PPN */
- vMatchMask : bits('valen), /* matching mask for superpages */
- vAddrMask : bits('valen), /* selection mask for superpages */
- pte : bits('ptelen), /* PTE */
- pteAddr : bits('palen), /* for dirty writeback */
- age : bits(64)
-}
+// Although a TLB is not part of the RISC-V Architecture
+// specification, we model a simple TLB so that
+// (1) we can meaningfully test SFENCE.VMA which would be a no-op wihout a TLB;
+// (2) we can greatly speed up simulation speed (for Linux boot, can
+// reduce elapsed time from 10s of minutes to few minutes).
+type asidbits = bits(16)
-val make_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen, 'valen > 0.
- (bits('asidlen), bool, bits('valen), bits('palen), bits('ptelen), nat, bits('palen), nat)
- -> TLB_Entry('asidlen, 'valen, 'palen, 'ptelen)
-function make_TLB_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr, levelBitSize) = {
- let shift : nat = PAGESIZE_BITS + (level * levelBitSize);
- /* fixme hack: use a better idiom for masks */
- let vAddrMask : bits('valen) = shiftl(vAddr ^ vAddr ^ zero_extend(0b1), shift) - 1;
- let vMatchMask : bits('valen) = ~ (vAddrMask);
- struct {
- asid = asid,
- global = global,
- pte = pte,
- pteAddr = pteAddr,
- vAddrMask = vAddrMask,
- vMatchMask = vMatchMask,
- vAddr = vAddr & vMatchMask,
- pAddr = shiftl(shiftr(pAddr, shift), shift),
- age = mcycle
- }
+// PRIVATE
+struct TLB_Entry = {
+ asid : asidbits, // address-space id
+ global : bool, // global translation
+ vAddr : bits(64), // VPN
+ pAddr : bits(64), // ppn
+ vMatchMask : bits(64), // matching mask for superpages
+ vAddrMask : bits(64), // selection mask for superpages
+ pte : bits(64), // PTE
+ pteAddr : bits(64), // for dirty writeback
+ age : bits(64) // for replacement policy?
}
-val match_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen.
- (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), bits('asidlen), bits('valen))
- -> bool
-function match_TLB_Entry(ent, asid, vaddr) =
- (ent.global | (ent.asid == asid)) & (ent.vAddr == (ent.vMatchMask & vaddr))
-
-val flush_TLB_Entry : forall 'asidlen 'valen 'palen 'ptelen.
- (TLB_Entry('asidlen, 'valen, 'palen, 'ptelen), option(bits('asidlen)), option(bits('valen)))
- -> bool
-function flush_TLB_Entry(e, asid, addr) = {
- match(asid, addr) {
+// Single-entry TLB (could enlarge this in future for better simulation speed)
+// PRIVATE
+register tlb : option(TLB_Entry) = None()
+
+// PUBLIC: invoked in init_vmem() [riscv_vmem.sail]
+function init_TLB() -> unit =
+ tlb = None()
+
+// PUBLIC: invoked in translate_TLB_hit() [riscv_vmem.sail]
+function write_TLB(idx : nat, ent : TLB_Entry) -> unit =
+ tlb = Some(ent)
+
+// PRIVATE
+function match_TLB_Entry(ent : TLB_Entry,
+ asid : asidbits,
+ vaddr : bits(64)) -> bool =
+ (ent.global | (ent.asid == asid))
+ & (ent.vAddr == (ent.vMatchMask & vaddr))
+
+// PRIVATE
+function flush_TLB_Entry(e : TLB_Entry,
+ asid : option(asidbits),
+ addr : option(bits(64))) -> bool = {
+ match (asid, addr) {
( None(), None()) => true,
( None(), Some(a)) => e.vAddr == (e.vMatchMask & a),
(Some(i), None()) => (e.asid == i) & not(e.global),
@@ -60,3 +58,58 @@ function flush_TLB_Entry(e, asid, addr) = {
& not(e.global))
}
}
+
+// PUBLIC: invoked in translate() [riscv_vmem.sail]
+function lookup_TLB (asid : asidbits, vaddr : bits(64)) -> option((nat, TLB_Entry)) =
+ match tlb {
+ None() => None(),
+ Some(e) => if match_TLB_Entry(e, asid, vaddr) then Some((0, e)) else None()
+ }
+
+// PRIVATE
+function add_to_TLB(asid : asidbits,
+ vAddr : bits(64),
+ pAddr : bits(64),
+ pte : bits(64),
+ pteAddr : bits(64),
+ level : nat,
+ global : bool,
+ levelBitSize : nat,
+ PAGESIZE_BITS : nat) -> unit = {
+ let shift = PAGESIZE_BITS + (level * levelBitSize);
+ assert(shift <= 64);
+ let vAddrMask : bits(64) = zero_extend(ones(shift));
+ let vMatchMask : bits(64) = ~ (vAddrMask);
+ let entry : TLB_Entry = struct{asid = asid,
+ global = global,
+ pte = pte,
+ pteAddr = pteAddr,
+ vAddrMask = vAddrMask,
+ vMatchMask = vMatchMask,
+ vAddr = vAddr & vMatchMask,
+ pAddr = shiftl(shiftr(pAddr, shift), shift),
+ age = mcycle};
+ tlb = Some(entry)
+}
+
+// Top-level TLB flush function
+// PUBLIC: invoked from exec SFENCE_VMA
+function flush_TLB(asid_xlen : option(xlenbits),
+ addr_xlen : option(xlenbits)) -> unit = {
+ let asid : option(asidbits) =
+ match asid_xlen {
+ None() => None(),
+ Some(a) => Some(a[15 .. 0])
+ };
+ let addr_64b : option(bits(64)) =
+ match addr_xlen {
+ None() => None(),
+ Some(a) => Some(zero_extend(a))
+ };
+ match tlb {
+ None() => (),
+ Some(e) => if flush_TLB_Entry(e, asid, addr_64b)
+ then tlb = None()
+ else ()
+ }
+}
generated by cgit v1.1 at 2024-07-10 03:47:59 +0000