diff options
| author | Alasdair | 2020-05-15 12:04:23 +0100 |
|---|---|---|
| committer | Alasdair | 2020-05-15 12:04:23 +0100 |
| commit | 865c48950cdf0e35ad83e7ea7560241d24971ec4 (patch) | |
| tree | 95d97e5bd73831d1df92efb7691b1b5a415edbdb /sailcov | |
| parent | 14f97c2e34e31b3d19d88ea277e7507c123182e9 (diff) | |
Move riscv_vmem_sv39 example to a separate page so it renders nicely
Diffstat (limited to 'sailcov')
| -rw-r--r-- | sailcov/README.md | 2 | ||||
| -rw-r--r-- | sailcov/riscv_vmem_sv39.html | 196 |
2 files changed, 1 insertions, 197 deletions
diff --git a/sailcov/README.md b/sailcov/README.md index 7eabc9fd..68ab0924 100644 --- a/sailcov/README.md +++ b/sailcov/README.md @@ -38,5 +38,5 @@ sailcov -a all_branches -t sail_coverage my_model.sail which produces a `my_model.html` file. Multiple sail files can be passed to the tool, and it will produce html for each -individually. See [riscv_vmem_sv39.html](riscv_vmem_sv_39.html) for an +individually. See [riscv_vmem_sv39.html](https://alasdair.github.io/riscv_vmem_sv39.html) for an example of the output. diff --git a/sailcov/riscv_vmem_sv39.html b/sailcov/riscv_vmem_sv39.html deleted file mode 100644 index f90c1380..00000000 --- a/sailcov/riscv_vmem_sv39.html +++ /dev/null @@ -1,196 +0,0 @@ -<!DOCTYPE html> -<html lang="en"> -<head> -<meta charset="utf-8"> -<title>riscv_vmem_sv39</title></head> -<body> -<code style="display: block"> -/* Sv39 address translation for RV64. */<br> -<br> -val walk39 : (vaddr39, AccessType(ext_access_type), Privilege, bool, bool, paddr64, nat, bool, ext_ptw) -> PTW_Result(paddr64, SV39_PTE) effect {rmem, rmemt, rreg, escape}<br> -function walk39(vaddr, ac, priv, mxr, do_sum, ptb, level, global, ext_ptw) = <span style="background-color: #c0FFc0">{<br> - let va = Mk_SV39_Vaddr(vaddr);<br> - let pt_ofs : paddr64 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),<br> - PTE39_LOG_SIZE);<br> - let pte_addr = ptb + pt_ofs;<br> - match (mem_read(ac, EXTZ(pte_addr), 8, false, false, false)) {<br> - MemException(_) => <span style="background-color: #FFc0c0">{<br> -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)<br> - ^ " pt_base=" ^ BitStr(ptb)<br> - ^ " pt_ofs=" ^ BitStr(pt_ofs)<br> - ^ " pte_addr=" ^ BitStr(pte_addr)<br> - ^ ": invalid pte address"); */<br> - PTW_Failure(PTW_Access(), ext_ptw)<br> - }</span>,<br> - MemValue(v) => <span style="background-color: #a0FFa0">{<br> - let pte = Mk_SV39_PTE(v);<br> - let pbits = pte.BITS();<br> - let ext_pte = pte.Ext();<br> - let pattr = Mk_PTE_Bits(pbits);<br> - let is_global = global | (pattr.G() == 0b1);<br> -/* print("walk39(vaddr=" ^ BitStr(vaddr) ^ " level=" ^ string_of_int(level)<br> - ^ " pt_base=" ^ BitStr(ptb)<br> - ^ " pt_ofs=" ^ BitStr(pt_ofs)<br> - ^ " pte_addr=" ^ BitStr(pte_addr)<br> - ^ " pte=" ^ BitStr(v)); */<br> - if isInvalidPTE(pbits, ext_pte) then <span style="background-color: #80FF80">{<br> -/* print("walk39: invalid pte"); */<br> - PTW_Failure(PTW_Invalid_PTE(), ext_ptw)<br> - }</span> else <span style="background-color: #80FF80">{<br> - if isPTEPtr(pbits, ext_pte) then <span style="background-color: #60FF60">{<br> - if level > 0 then <span style="background-color: #40FF40">{<br> - /* walk down the pointer to the next level */<br> - walk39(vaddr, ac, priv, mxr, do_sum, shiftl(EXTZ(pte.PPNi()), PAGESIZE_BITS), level - 1, is_global, ext_ptw)<br> - }</span> else <span style="background-color: #FFc0c0">{<br> - /* last-level PTE contains a pointer instead of a leaf */<br> -/* print("walk39: last-level pte contains a ptr"); */<br> - PTW_Failure(PTW_Invalid_PTE(), ext_ptw)<br> - }</span><br> - }</span> else <span style="background-color: #60FF60">{ /* leaf PTE */<br> - match checkPTEPermission(ac, priv, mxr, do_sum, pattr, ext_pte, ext_ptw) {<br> - PTE_Check_Failure(ext_ptw) => <span style="background-color: #40FF40">{<br> -/* print("walk39: pte permission check failure"); */<br> - PTW_Failure(PTW_No_Permission(), ext_ptw)<br> - }</span>,<br> - PTE_Check_Success(ext_ptw) => <span style="background-color: #40FF40">{<br> - if level > 0 then <span style="background-color: #20FF20">{ /* superpage */<br> - /* fixme hack: to get a mask of appropriate size */<br> - let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;<br> - if (pte.PPNi() & mask) != EXTZ(0b0) then <span style="background-color: #0FF0">{<br> - /* misaligned superpage mapping */<br> -/* print("walk39: misaligned superpage mapping"); */<br> - PTW_Failure(PTW_Misaligned(), ext_ptw)<br> - }</span> else <span style="background-color: #0FF0">{<br> - /* add the appropriate bits of the VPN to the superpage PPN */<br> - let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);<br> -/* let res = append(ppn, va.PgOfs());<br> - print("walk39: using superpage: pte.ppn=" ^ BitStr(pte.PPNi())<br> - ^ " ppn=" ^ BitStr(ppn) ^ " res=" ^ BitStr(res)); */<br> - PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw)<br> - }</span><br> - }</span> else <span style="background-color: #20FF20">{<br> - /* normal leaf PTE */<br> -/* let res = append(pte.PPNi(), va.PgOfs());<br> - print("walk39: pte.ppn=" ^ BitStr(pte.PPNi()) ^ " ppn=" ^ BitStr(pte.PPNi()) ^ " res=" ^ BitStr(res)); */<br> - PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global, ext_ptw)<br> - }</span><br> - }</span><br> - }<br> - }</span><br> - }</span><br> - }</span><br> - }<br> -}</span><br> -<br> -/* TLB management: single entry for now */<br> -<br> -// ideally we would use the below form:<br> -// type TLB39_Entry = TLB_Entry(sizeof(asid64), sizeof(vaddr39), sizeof(paddr64), sizeof(pte64))<br> -type TLB39_Entry = TLB_Entry(16, 39, 56, 64)<br> -register tlb39 : option(TLB39_Entry)<br> -<br> -val lookup_TLB39 : (asid64, vaddr39) -> option((nat, TLB39_Entry)) effect {rreg}<br> -function lookup_TLB39(asid, vaddr) =<br> - <span style="background-color: #c0FFc0">match tlb39 {<br> - None() => <span style="background-color: #a0FFa0">None()</span>,<br> - Some(e) => <span style="background-color: #a0FFa0">if match_TLB_Entry(e, asid, vaddr) then <span style="background-color: #80FF80">Some((0, e))</span> else <span style="background-color: #80FF80">None()</span></span><br> - }</span><br> -<br> -val add_to_TLB39 : (asid64, vaddr39, paddr64, SV39_PTE, paddr64, nat, bool) -> unit effect {wreg, rreg}<br> -function add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global) = <span style="background-color: #c0FFc0">{<br> - let ent : TLB39_Entry = make_TLB_Entry(asid, global, vAddr, pAddr, pte.bits(), level, pteAddr, SV39_LEVEL_BITS);<br> - tlb39 = Some(ent)<br> -}</span><br> -<br> -function write_TLB39(idx : nat, ent : TLB39_Entry) -> unit =<br> - <span style="background-color: #FFc0c0">tlb39 = Some(ent)</span><br> -<br> -val flush_TLB39 : (option(asid64), option(vaddr39)) -> unit effect {rreg, wreg}<br> -function flush_TLB39(asid, addr) =<br> - <span style="background-color: #c0FFc0">match (tlb39) {<br> - None() => <span style="background-color: #a0FFa0">()</span>,<br> - Some(e) => <span style="background-color: #a0FFa0">if flush_TLB_Entry(e, asid, addr)<br> - then <span style="background-color: #80FF80">tlb39 = None()</span><br> - else <span style="background-color: #80FF80">()</span></span><br> - }</span><br> -<br> -/* address translation */<br> -<br> -val translate39 : (asid64, paddr64, vaddr39, AccessType(ext_access_type), Privilege, bool, bool, nat, ext_ptw) -> TR_Result(paddr64, PTW_Error) effect {rreg, wreg, wmv, wmvt, escape, rmem, rmemt}<br> -function translate39(asid, ptb, vAddr, ac, priv, mxr, do_sum, level, ext_ptw) = <span style="background-color: #c0FFc0">{<br> - match lookup_TLB39(asid, vAddr) {<br> - Some(idx, ent) => <span style="background-color: #a0FFa0">{<br> -/* print("translate39: TLB39 hit for " ^ BitStr(vAddr)); */<br> - let pte = Mk_SV39_PTE(ent.pte);<br> - let ext_pte = pte.Ext();<br> - let pteBits = Mk_PTE_Bits(pte.BITS());<br> - match checkPTEPermission(ac, priv, mxr, do_sum, pteBits, ext_pte, ext_ptw) {<br> - PTE_Check_Failure(ext_ptw) => <span style="background-color: #FFc0c0">{ TR_Failure(PTW_No_Permission(), ext_ptw) }</span>,<br> - PTE_Check_Success(ext_ptw) => <span style="background-color: #80FF80">{<br> - match update_PTE_Bits(pteBits, ac, ext_pte) {<br> - None() => <span style="background-color: #60FF60">TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw)</span>,<br> - Some(pbits, ext) => <span style="background-color: #60FF60">{<br> - if ~ (plat_enable_dirty_update ())<br> - then <span style="background-color: #40FF40">{<br> - /* pte needs dirty/accessed update but that is not enabled */<br> - TR_Failure(PTW_PTE_Update(), ext_ptw)<br> - }</span> else <span style="background-color: #FFc0c0">{<br> - /* update PTE entry and TLB */<br> - n_pte = update_BITS(pte, pbits.bits());<br> - n_pte = update_Ext(n_pte, ext);<br> - n_ent : TLB39_Entry = ent;<br> - n_ent.pte = n_pte.bits();<br> - write_TLB39(idx, n_ent);<br> - /* update page table */<br> - match mem_write_value(EXTZ(ent.pteAddr), 8, n_pte.bits(), false, false, false) {<br> - MemValue(_) => <span style="background-color: #FFa0a0">()</span>,<br> - MemException(e) => <span style="background-color: #FFa0a0">internal_error("invalid physical address in TLB")</span><br> - };<br> - TR_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask), ext_ptw)<br> - }</span><br> - }</span><br> - }<br> - }</span><br> - }<br> - }</span>,<br> - None() => <span style="background-color: #a0FFa0">{<br> - match walk39(vAddr, ac, priv, mxr, do_sum, ptb, level, false, ext_ptw) {<br> - PTW_Failure(f, ext_ptw) => <span style="background-color: #80FF80">TR_Failure(f, ext_ptw)</span>,<br> - PTW_Success(pAddr, pte, pteAddr, level, global, ext_ptw) => <span style="background-color: #80FF80">{<br> - match update_PTE_Bits(Mk_PTE_Bits(pte.BITS()), ac, pte.Ext()) {<br> - None() => <span style="background-color: #60FF60">{<br> - add_to_TLB39(asid, vAddr, pAddr, pte, pteAddr, level, global);<br> - TR_Address(pAddr, ext_ptw)<br> - }</span>,<br> - Some(pbits, ext) =><br> - <span style="background-color: #60FF60">if ~ (plat_enable_dirty_update ())<br> - then <span style="background-color: #40FF40">{<br> - /* pte needs dirty/accessed update but that is not enabled */<br> - TR_Failure(PTW_PTE_Update(), ext_ptw)<br> - }</span> else <span style="background-color: #FFc0c0">{<br> - w_pte : SV39_PTE = update_BITS(pte, pbits.bits());<br> - w_pte : SV39_PTE = update_Ext(w_pte, ext);<br> - match mem_write_value(EXTZ(pteAddr), 8, w_pte.bits(), false, false, false) {<br> - MemValue(_) => <span style="background-color: #FFa0a0">{<br> - add_to_TLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);<br> - TR_Address(pAddr, ext_ptw)<br> - }</span>,<br> - MemException(e) => <span style="background-color: #FFa0a0">{<br> - /* pte is not in valid memory */<br> - TR_Failure(PTW_Access(), ext_ptw)<br> - }</span><br> - }<br> - }</span></span><br> - }<br> - }</span><br> - }<br> - }</span><br> - }<br> -}</span><br> -<br> -function init_vmem_sv39() -> unit = <span style="background-color: #c0FFc0">{<br> - tlb39 = None()<br> -}</span><br> -</code> -</body> -</html>
\ No newline at end of file |
