From 91efb5462c63be649aadbfb986de4db15844558b Mon Sep 17 00:00:00 2001 From: Rishiyur Nikhil Date: Fri, 1 Dec 2023 14:58:04 -0500 Subject: [PATCH] Replace old virtual memory code with new (details follow) Old code had much 'cut-and-paste' replication for RV32 (Sv32) and 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_common.sail riscv_pte.sail riscv_ptw.sail riscv_vmem_rv32.sail riscv_vmem_rv64.sail riscv_vmem_sv32.sail riscv_vmem_sv39.sail riscv_vmem_sv48.sail Added 1 new file, where the main vmem code sits: riscv_vmem.sail Modified (to be compatible with new code, and to isolate TLB stuff into one file, since TLBs are not part of RISC-V Architecture Spec) riscv_vmem_tlb.sail Added documentation on new vmem code: doc/notes_Virtual_Memory.adoc Deleted older vmem files. --- Makefile | 23 +- doc/figs/notes_Virtual_Memory_Fig1.svg | 1027 ++++++++++++++++++++++++ doc/notes_Virtual_Memory.adoc | 111 +++ model/riscv_pte.sail | 154 ---- model/riscv_ptw.sail | 121 --- model/riscv_vmem.sail | 871 ++++++++++++++++++++ model/riscv_vmem_common.sail | 229 ------ model/riscv_vmem_rv32.sail | 137 ---- model/riscv_vmem_rv64.sail | 176 ---- model/riscv_vmem_sv32.sail | 262 ------ model/riscv_vmem_sv39.sail | 256 ------ model/riscv_vmem_sv48.sail | 218 ----- model/riscv_vmem_tlb.sail | 288 ++++--- 13 files changed, 2204 insertions(+), 1669 deletions(-) create mode 100644 doc/figs/notes_Virtual_Memory_Fig1.svg create mode 100644 doc/notes_Virtual_Memory.adoc delete mode 100644 model/riscv_pte.sail delete mode 100644 model/riscv_ptw.sail create mode 100644 model/riscv_vmem.sail delete mode 100644 model/riscv_vmem_common.sail delete mode 100644 model/riscv_vmem_rv32.sail delete mode 100644 model/riscv_vmem_rv64.sail delete mode 100644 model/riscv_vmem_sv32.sail delete mode 100644 model/riscv_vmem_sv39.sail delete mode 100644 model/riscv_vmem_sv48.sail diff --git a/Makefile b/Makefile index 9140065bd..ba5d242ea 100644 --- a/Makefile +++ b/Makefile @@ -68,15 +68,20 @@ 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 +# Virtual Memory support: (2023-11) OLD VM CODE replaced by NEW VM CODE +# (see doc/notes_Virtual_Memory.adoc) +# OLD VM CODE +# 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 +# NEW VM CODE +SAIL_VM_SRCS += riscv_vmem_tlb.sail +SAIL_VM_SRCS += riscv_vmem.sail # Non-instruction sources PRELUDE = prelude.sail prelude_mapping.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 000000000..4c5b2249c --- /dev/null +++ b/doc/figs/notes_Virtual_Memory_Fig1.svg @@ -0,0 +1,1027 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + image/svg+xml + + + + + + + + + + + registersatp + + readCSR() + writeCSR() + Exec Fetch + Exec SFENCE.VMA + PUBLIC + legalize_satp() + + + + translateAddr() + union TR_Result + + + + + PRIVATE + + translate() + add_to_TLB() + write_TLB() + mem_read_priv() + mem_write_value_priv() + + PRIVATE + PUBLIC + + + registertlb + + translate_TLB_miss() + translate_TLB_hit() + lookup_TLB() + init_vmem() + init_TLB() + + + init_model() + + + + pt_walk() + + make_TLB_Entry() + match_TLB_Entry() + flush_TLB() + + flush_TLB_Entry() + + + + + + riscv_vmem.sail + riscv_vmem_tlb.sail + satp64Mode_of_Bits() + cur_privilege + effectivePrivilege() + Exec Load/Store/AMO + + plat_enable_dirty_update() + + + diff --git a/doc/notes_Virtual_Memory.adoc b/doc/notes_Virtual_Memory.adoc new file mode 100644 index 000000000..3285a0241 --- /dev/null +++ b/doc/notes_Virtual_Memory.adoc @@ -0,0 +1,111 @@ += 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 vmem +specification code is in one file: + + model/riscv_vmem.sail + +There are two more files, of less relevance for the specification: + + model/riscv_vmem_tlb.sail + model/riscv_vmem_types.sail + +`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 an outline of the 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 + +* 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 ++ +The current code is primarily in these files: ++ + riscv_vmem.sail (New) + riscv_vmem_tlb.sail (Modified) + riscv_vmem_types.sail (Unchanged) diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail deleted file mode 100644 index 90345cc93..000000000 --- a/model/riscv_pte.sail +++ /dev/null @@ -1,154 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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_ptw.sail b/model/riscv_ptw.sail deleted file mode 100644 index 2b7ef4541..000000000 --- a/model/riscv_ptw.sail +++ /dev/null @@ -1,121 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* failure modes for address-translation/page-table-walks */ - -union PTW_Error = { - 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 */ -} - -val ptw_error_to_str : PTW_Error -> string -function ptw_error_to_str(e) = - match (e) { - PTW_Invalid_Addr() => "invalid-source-addr", - PTW_Access() => "mem-access-error", - PTW_Invalid_PTE() => "invalid-pte", - PTW_No_Permission() => "no-permission", - PTW_Misaligned() => "misaligned-superpage", - PTW_PTE_Update() => "pte-update-needed", - PTW_Ext_Error(e) => "extension-error" - } - -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(). - */ -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 = - match (a, f) { - (_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)), - (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), - (ReadWrite(_), _) => E_SAMO_Page_Fault(), - (Read(_), PTW_Access()) => E_Load_Access_Fault(), - (Read(_), _) => E_Load_Page_Fault(), - (Write(_), PTW_Access()) => E_SAMO_Access_Fault(), - (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.sail b/model/riscv_vmem.sail new file mode 100644 index 000000000..69b8a2435 --- /dev/null +++ b/model/riscv_vmem.sail @@ -0,0 +1,871 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + +// **************************************************************** +// 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. +// Sizes with '_b' are for bits, '_B' are for Bytes + +// 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. + +// **************************************************************** +// Useful 64-bit numeric constants + +// PRIVATE +let zero_64b : bits(64) = zero_extend(0b0) +let one_64b : bits(64) = zero_extend(0b1) + +// **************************************************************** +// Parameters for VM modes sv32, sv39 and sv48 + +// All VM modes use the same page size (4KB, with 12-bit index) + +let PAGESIZE_BITS : nat = 12 + +// PRIVATE +struct SV_Params = { + // SATP CSR // Sv32 Sv39 Sv48 + satp_asid_size_b : nat, // 9 16 16 + satp_asid_lsb_index : nat, // 22 44 44 + + // SATP PPN + satp_ppn_size_b : nat, // 22 44 44 + satp_ppn_lsb_index : nat, // 0 0 0 + + // VA // Sv32 Sv39 Sv48 + va_size_b : nat, // 32 39 48 + vpn_size_b : nat, // 10 9 9 + + // PTE // Sv32 Sv39 Sv48 + levels : nat, // 2 3 4 + log_pte_size_B : nat, // 2 3 3 + pte_msbs_lsb_index : nat, // 32 54 54 + pte_msbs_size_b : nat, // 0 10 10 + pte_PPNs_lsb_index : nat, // 10 10 10 + pte_PPNs_size_b : nat, // 22 44 44 + pte_PPN_j_size_b : nat // 10 9 9 +} + +// PRIVATE +let sv32_params : SV_Params = struct { + // SATP CSR + satp_asid_size_b = 9, + satp_asid_lsb_index = 22, + + // SATP PPN + satp_ppn_size_b = 22, + satp_ppn_lsb_index = 0, + + // VA + va_size_b = 32, + vpn_size_b = 10, + + // PTE + levels = 2, + log_pte_size_B = 2, // 4 Bytes + pte_msbs_lsb_index = 32, + pte_msbs_size_b = 0, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_b = 22, + pte_PPN_j_size_b = 10 +} + +// PRIVATE +let sv39_params : SV_Params = struct { + // SATP CSR + satp_asid_size_b = 16, + satp_asid_lsb_index = 44, + + // SATP PPN + satp_ppn_size_b = 44, + satp_ppn_lsb_index = 0, + + // VA + va_size_b = 39, + vpn_size_b = 9, + + // PTE + levels = 3, + log_pte_size_B = 3, // 8 Bytes + pte_msbs_lsb_index = 54, + pte_msbs_size_b = 10, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_b = 44, + pte_PPN_j_size_b = 9 +} + +// PRIVATE +let sv48_params : SV_Params = struct { + // SATP CSR + satp_asid_size_b = 16, + satp_asid_lsb_index = 44, + + // SATP PPN + satp_ppn_size_b = 44, + satp_ppn_lsb_index = 0, + + // VA + va_size_b = 48, + vpn_size_b = 9, + + // PTE + levels = 4, + log_pte_size_B = 3, // 8 Bytes + pte_msbs_lsb_index = 54, + pte_msbs_size_b = 10, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_b = 44, + pte_PPN_j_size_b = 9 +} + +// For future; not currently used +let sv57_params : SV_Params = struct { + // SATP CSR + satp_asid_size_b = 16, + satp_asid_lsb_index = 44, + + // SATP PPN + satp_ppn_size_b = 44, + satp_ppn_lsb_index = 0, + + // VA + va_size_b = 57, + vpn_size_b = 9, + + // PTE + levels = 5, + log_pte_size_B = 3, // 8 Bytes + pte_msbs_lsb_index = 54, + pte_msbs_size_b = 10, + pte_PPNs_lsb_index = 10, + pte_PPNs_size_b = 44, + pte_PPN_j_size_b = 9 +} + +// **************************************************************** +// 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) = (one_64b << sv_params.va_size_b) - one_64b; + (va & mask) >> PAGESIZE_BITS +} + +// PRIVATE: Extract VPN[level] from VA +function vpn_j_of_va(sv_params : SV_Params, + va : bits(64), + level : nat) -> bits(64) = { + let lsb : nat = PAGESIZE_BITS + level * sv_params.vpn_size_b; + let mask : bits(64) = (one_64b << sv_params.vpn_size_b) - 1; + ((va >> lsb) & mask) +} + +// PRIVATE: Extract offset within page from VA +function offset_of_va(va : bits(64)) -> bits(64) = { + let mask : bits(64) = (one_64b << PAGESIZE_BITS) - 1; + va & mask +} + +// 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 isValidVAddr(sv_params : SV_Params, vAddr : bits(64)) -> bool = { + let index = sv_params.va_size_b - 1; + assert((0 <= index) & (index < 64)); + let upper_bits = vAddr >> (sv_params.va_size_b); + let va_msb = vAddr[index]; + if va_msb == bitzero then + upper_bits == zeros() + else + upper_bits == ones() >> (sv_params.va_size_b) +} + +// **************************************************************** +// 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 no available bits on RV32, so these bits will be zeros on RV32. + +// 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) = (one_64b << sv_params.pte_msbs_size_b) - one_64b; + (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) = (one_64b << sv_params.pte_PPNs_size_b) - one_64b; + (pte >> sv_params.pte_PPNs_lsb_index) & mask +} + +// PRIVATE: extract LSBs (including permissions) of PTE +function D_of_PTE(pte : bits(64)) -> bit = pte[7] +function A_of_PTE(pte : bits(64)) -> bit = pte[6] +function G_of_PTE(pte : bits(64)) -> bit = pte[5] +function U_of_PTE(pte : bits(64)) -> bit = pte[4] +function X_of_PTE(pte : bits(64)) -> bit = pte[3] +function W_of_PTE(pte : bits(64)) -> bit = pte[2] +function R_of_PTE(pte : bits(64)) -> bit = pte[1] +function V_of_PTE(pte : bits(64)) -> bit = pte[0] + +// PRIVATE: check if a PTE is a pointer to next level (non-leaf) +function pte_is_ptr(pte : bits(64)) -> bool = { + let x = X_of_PTE(pte); + let w = W_of_PTE(pte); + let r = R_of_PTE(pte); + (x == bitzero) & (w == bitzero) & (r == bitzero) +} + +// PRIVATE: check if a PTE is valid +function pte_is_invalid(pte : bits(64)) -> bool = { + let w = W_of_PTE(pte); + let r = R_of_PTE(pte); + let v = V_of_PTE(pte); + (v == bitzero) | ((w == bitone) & (r == bitzero)) +} + +// ---------------- +// 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 checkPTEPermission(ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + pte_U : bit, + pte_X : bit, + pte_W : bit, + pte_R : bit, + ext : extPte, + ext_ptw : ext_ptw) -> PTE_Check = { + let b : bool = + match (ac, priv) { + (Read(_), User) => ((pte_U == bitone) + & ((pte_R == bitone) | ((pte_X == bitone & mxr)))), + (Write(_), User) => ((pte_U == bitone) & (pte_W == bitone)), + (ReadWrite(_, _), User) => ((pte_U == bitone) + & (pte_W == bitone) + & ((pte_R == bitone) | ((pte_X == bitone) & mxr))), + (Execute(), User) => ((pte_U == bitone) & (pte_X == bitone)), + (Read(_), Supervisor) => (((pte_U == bitzero) | do_sum) + & ((pte_R == bitone) | ((pte_X == bitone) & mxr))), + (Write(_), Supervisor) => (((pte_U == bitzero) | do_sum) & (pte_W == bitone)), + (ReadWrite(_, _), Supervisor) => (((pte_U == bitzero) | do_sum) + & (pte_W == bitone) + & ((pte_R == bitone) | ((pte_X == bitone) & mxr))), + (Execute(), Supervisor) => ((pte_U == bitzero) & (pte_X == bitone)), + (_, Machine) => internal_error(__FILE__, __LINE__, + "m-mode mem perm check")}; + if b 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), + ext : extPte) + -> option(bits(64)) = { + // Update 'dirty' bit? + let update_d = (D_of_PTE (pte) == bitzero) + & (match a { + Execute() => false, + Read() => false, + Write(_) => true, + ReadWrite(_,_) => true + }); + // Update 'accessed'-bit? + let update_a = A_of_PTE(pte) == bitzero; + if update_d | update_a then { + let pte1 = pte | (one_64b << 6); + let pte2 = if update_d then (pte1 | (one_64b << 7)) else pte1; + Some(pte2 | (ext << sv_params.pte_msbs_lsb_index)) + } + else + None() +} + +// **************************************************************** +// Results of Page Table Walk (PTW) + +// 'ext_ptw' supports (non-standard) extensions to the default addr-translation and PTW. + +// 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_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 +} + +// 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", + PTW_No_Permission() => "no-permission", + PTW_Misaligned() => "misaligned-superpage", + PTW_PTE_Update() => "pte-update-needed", + PTW_Ext_Error(e) => "extension-error" + } + +// PUBLIC +overload to_str = {ptw_error_to_str} + +// 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 checkPTEPermission(). + +// PRIVATE +function ext_get_ptw_error(eptwf : ext_ptw_fail) -> PTW_Error = + PTW_No_Permission() + +// Convert translation/PTW failures into architectural exceptions +function translationException(a : AccessType(ext_access_type), + f : PTW_Error) + -> ExceptionType = { + let e : ExceptionType = + match (a, f) { + (_, PTW_Ext_Error(e)) => E_Extension(ext_translate_exception(e)), + (ReadWrite(_), PTW_Access()) => E_SAMO_Access_Fault(), + (ReadWrite(_), _) => E_SAMO_Page_Fault(), + (Read(_), PTW_Access()) => E_Load_Access_Fault(), + (Read(_), _) => E_Load_Page_Fault(), + (Write(_), PTW_Access()) => E_SAMO_Access_Fault(), + (Write(_), _) => E_SAMO_Page_Fault(), + (Execute(), PTW_Access()) => E_Fetch_Access_Fault(), + (Execute(), _) => E_Fetch_Page_Fault() + }; + e +} + +// 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 => cannot merge 'val' and 'function' decls + +// PRIVATE +val pt_walk : (SV_Params, + bits(64), // virtual addr + AccessType(ext_access_type), // Read/Write/ReadWWrite/Execute + Privilege, // User/Supervisor/Machine + bool, // mstatus.MXR + bool, // do_sum + bits(64), // PT base addr + nat, // 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_B; + let pte_addr = pt_base + pte_offset; + 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 + + let ptw_result : PTW_Result = + match (mem_result) { + MemException(_) => PTW_Failure (PTW_Access(), ext_ptw), + MemValue(pte) => { + let ppns : bits(64) = PPNs_of_PTE(sv_params, pte); + let ext_pte = msbs_of_PTE(sv_params, pte); + let global' = global | (G_of_PTE(pte) == bitone); + if pte_is_invalid(pte) then + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + else { + // Non-Leaf PTE + if pte_is_ptr(pte) then { + if level > 0 then { + // follow the pointer to walk next level + let pt_base' : bits(64) = shiftl(ppns, PAGESIZE_BITS); + let level' = level - 1; + let ptw_result = pt_walk(sv_params, va, ac, priv, mxr, do_sum, + pt_base', level', global', ext_ptw); + ptw_result + } + else + // level 0 PTE, but contains a pointer instead of a leaf + PTW_Failure(PTW_Invalid_PTE(), ext_ptw) + } + // Leaf PTE + else { + let pte_check = checkPTEPermission(ac, priv, mxr, do_sum, + U_of_PTE(pte), + X_of_PTE(pte), + W_of_PTE(pte), + R_of_PTE(pte), + 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 + mask_PPN_j : bits(64) = (one_64b << sv_params.pte_PPN_j_size_b) - one_64b; + mask : bits(64) = zero_64b; + foreach (j from 0 to (level - 1)) + mask = ((mask << sv_params.pte_PPN_j_size_b) | mask_PPN_j); + // Lower-level PPNs must be zero (for aligned superpage) + if not((ppns & mask) == zero_64b) 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 ppn = ppns | (vpns_of_va (sv_params, va) & mask); + let pa = ((ppn << PAGESIZE_BITS) | offset_of_va(va)); + PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) + } + } + else { + let pa = ((ppns << PAGESIZE_BITS) | offset_of_va (va)); + PTW_Success(pa, pte, pte_addr, level, global', ext_ptw) + } + } + } + } + } + }; + ptw_result +} + +// **************************************************************** +// 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" ^ string_of_int(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(sv_params : SV_Params, satp_val : xlenbits) -> bits(16) = { + // This extend op is a no-op when xlen==64, extends when xlen==32 + let satp_64b : bits(64) = zero_extend (satp_val); + let mask_64b : bits(64) = (one_64b << sv_params.satp_asid_size_b) - one_64b; + let asid_64b : bits(64) = (satp_64b >> sv_params.satp_asid_lsb_index) & mask_64b; + asid_64b[15 .. 0] +} + +// Result is 64b to cover both RV32 and RV64 addrs +// PRIVATE +function satp_to_PT_base(sv_params : SV_Params, satp_val : xlenbits) -> bits(64) = { + // This extend op is a no-op when xlen==64, extends when xlen==32 + let satp_64b : bits(64) = zero_extend (satp_val); + let mask_64b : bits(64) = (one_64b << sv_params.satp_ppn_size_b) - one_64b; + let ppn_64b : bits(64) = (satp_64b >> sv_params.satp_ppn_lsb_index) & mask_64b; + ppn_64b << PAGESIZE_BITS +} + +// Compute address translation mode from SATP +// TODO: shouldn't we look at mstatus_UXL if priv is User? + +// PRIVATE +function translationMode(priv : Privilege) -> SATPMode = { + if priv == Machine then + Sbare + else if sizeof(xlen) == 32 then + match satp[31] { + bitzero => Sbare, + bitone => Sv32 + } + else if sizeof(xlen) == 64 then { + // This extend op is a no-op when xlen==64, + // but appeases the type-checker when xlen==32 (when this code is not executed!) + let satp_64b : bits(64) = zero_extend(satp); + // 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 satp[31] { + // When xlen is 64, mstatus.SXL/UXL (for S, U privileges) can be RV32 + bitzero => Sbare, + bitone => 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 : bits(16), + ptb : bits(64), + vAddr : bits(64), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + level : nat, + 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_check = checkPTEPermission(ac, priv, mxr, do_sum, + U_of_PTE(pte), + X_of_PTE(pte), + W_of_PTE(pte), + R_of_PTE(pte), + ext_pte, + ext_ptw); + let tr_result : TR_Result(bits(64), PTW_Error) + = 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, ext_pte) { + 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) + n_ent : TLB_Entry = ent; + n_ent.pte = pte'; + write_TLB(tlb_index, n_ent); + let pte_phys_addr : xlenbits = 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) + } + } + }; + tr_result +} + +// PRIVATE: translate on TLB miss (do a page-table walk) +function translate_TLB_miss(sv_params : SV_Params, + asid : bits(16), + ptb : bits(64), + vAddr : bits(64), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + level : nat, + ext_ptw : ext_ptw) -> TR_Result(bits(64), PTW_Error) = { + let ptw_result = pt_walk(sv_params, vAddr, ac, priv, mxr, do_sum, + ptb, 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, ext_pte) { + None() => { + add_to_TLB(asid, vAddr, pAddr, pte, pteAddr, level, global, + sv_params.vpn_size_b, // TODO: ppn_size_b? + 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 : xlenbits = 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_b, // TODO: ppn_size_b? + PAGESIZE_BITS); + TR_Address(pAddr, ext_ptw) + }, + MemException(e) => + TR_Failure(PTW_Access(), ext_ptw) + } + } + } + } + } +} + +// PRIVATE +function translate(sv_params : SV_Params, + asid : bits(16), + ptb : bits(64), + vAddr_arg : bits(64), + ac : AccessType(ext_access_type), + priv : Privilege, + mxr : bool, + do_sum : bool, + level : nat, + ext_ptw : ext_ptw) + -> TR_Result(bits(64), PTW_Error) = { + let va_mask = (one_64b << sv_params.va_size_b) - 1; + 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, level, ext_ptw, index, ent), + None() => translate_TLB_miss(sv_params, asid, ptb, vAddr, ac, priv, + mxr, do_sum, level, 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 op 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); + // PTW extensions (non-standard): initialize the PTW extension state + let ext_ptw : ext_ptw = init_ext_ptw; + + let tr_result : TR_Result(xlenbits, ExceptionType) = + if mode == Sbare then + TR_Address(vAddr, ext_ptw) + else { + let (valid_va, sv_params) : (bool, SV_Params) + = match (mode) { + Sv32 => (true, sv32_params), + Sv39 => (isValidVAddr(sv39_params, vAddr_64b), sv39_params), + Sv48 => (isValidVAddr(sv48_params, vAddr_64b), sv48_params), + // Sv57 => (isValidVAddr(sv57_params, vAddr_64b), sv57_params), // TODO + _ => internal_error(__FILE__, __LINE__, + "unsupported address translation mode") + }; + if not(valid_va) then + TR_Failure(translationException(ac, PTW_Invalid_Addr()), ext_ptw) + else { + let mxr : bool = mstatus.MXR() == 0b1; + let do_sum : bool = mstatus.SUM() == 0b1; + let asid : bits(16) = satp_to_asid(sv_params, satp); + let ptb : bits(64) = satp_to_PT_base(sv_params, satp); + let init_level = sv_params.levels - 1; + assert(init_level >= 0); // allows init_level to be passed as 'nat' type + let tr_result1 = translate (sv_params, + asid, + ptb, + vAddr_64b, + ac, effPriv, mxr, do_sum, + init_level, + 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) + } + } + }; + tr_result +} + +// **************************************************************** +// Initialize Virtul 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 deleted file mode 100644 index 46134d2d9..000000000 --- a/model/riscv_vmem_common.sail +++ /dev/null @@ -1,229 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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) -} - -/* 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 -} - -bitfield SV32_Paddr : paddr32 = { - PPNi : 33 .. 12, - PgOfs : 11 .. 0 -} - -bitfield SV32_PTE : pte32 = { - PPNi : 31 .. 10, - RSW : 9 .. 8, - BITS : 7 .. 0 -} - -/* - * 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) -} diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail deleted file mode 100644 index 3478be4da..000000000 --- a/model/riscv_vmem_rv32.sail +++ /dev/null @@ -1,137 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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 18d099192..000000000 --- a/model/riscv_vmem_rv64.sail +++ /dev/null @@ -1,176 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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 72def151a..000000000 --- a/model/riscv_vmem_sv32.sail +++ /dev/null @@ -1,262 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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=" ^ string_of_int(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=" ^ string_of_int(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 25378a8dc..000000000 --- a/model/riscv_vmem_sv39.sail +++ /dev/null @@ -1,256 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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=" ^ string_of_int(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=" ^ string_of_int(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 64c7a542a..000000000 --- a/model/riscv_vmem_sv48.sail +++ /dev/null @@ -1,218 +0,0 @@ -/*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ -/*=======================================================================================*/ - -/* 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=" ^ string_of_int(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=" ^ string_of_int(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 27b63ba37..99e2e8ce9 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -1,124 +1,198 @@ /*=======================================================================================*/ -/* RISCV Sail Model */ -/* */ -/* This Sail RISC-V architecture model, comprising all files and */ -/* directories except for the snapshots of the Lem and Sail libraries */ -/* in the prover_snapshots directory (which include copies of their */ -/* licences), is subject to the BSD two-clause licence below. */ -/* */ -/* Copyright (c) 2017-2023 */ -/* Prashanth Mundkur */ -/* Rishiyur S. Nikhil and Bluespec, Inc. */ -/* Jon French */ -/* Brian Campbell */ -/* Robert Norton-Wright */ -/* Alasdair Armstrong */ -/* Thomas Bauereiss */ -/* Shaked Flur */ -/* Christopher Pulte */ -/* Peter Sewell */ -/* Alexander Richardson */ -/* Hesham Almatary */ -/* Jessica Clarke */ -/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ -/* Peter Rugg */ -/* Aril Computer Corp., for contributions by Scott Johnson */ -/* Philipp Tomsich */ -/* VRULL GmbH, for contributions by its employees */ -/* */ -/* All rights reserved. */ -/* */ -/* This software was developed by the above within the Rigorous */ -/* Engineering of Mainstream Systems (REMS) project, partly funded by */ -/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ -/* Edinburgh. */ -/* */ -/* This software was developed by SRI International and the University of */ -/* Cambridge Computer Laboratory (Department of Computer Science and */ -/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ -/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ -/* SSITH research programme. */ -/* */ -/* This project has received funding from the European Research Council */ -/* (ERC) under the European Union’s Horizon 2020 research and innovation */ -/* programme (grant agreement 789108, ELVER). */ -/* */ -/* */ -/* Redistribution and use in source and binary forms, with or without */ -/* modification, are permitted provided that the following conditions */ -/* are met: */ -/* 1. Redistributions of source code must retain the above copyright */ -/* notice, this list of conditions and the following disclaimer. */ -/* 2. Redistributions in binary form must reproduce the above copyright */ -/* notice, this list of conditions and the following disclaimer in */ -/* the documentation and/or other materials provided with the */ -/* distribution. */ -/* */ -/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ -/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ -/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ -/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ -/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ -/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ -/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ -/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ -/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ -/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ -/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ -/* SUCH DAMAGE. */ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ /*=======================================================================================*/ -/* idealized generic TLB entry to model fence.vm and also speed up simulation. */ +// 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. -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) +// PRIVATE +struct TLB_Entry = { + asid : bits(16), // 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? } +// Single-entry TLB (could enlarge this in future for better simulation speed) +// PRIVATE +register tlb : option(TLB_Entry) -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) = { +// 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 make_TLB_Entry(asid : bits(16), + global : bool, + vAddr : bits(64), + pAddr : bits(64), + pte : bits(64), + level : nat, + pteAddr : bits(64), + levelBitSize : nat, + PAGESIZE_BITS : nat) -> TLB_Entry = { 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 - } + // fixme hack: use a better idiom for masks + // let vAddrMask : bits(64) = shiftl(vAddr ^ vAddr ^ one_64b, shift) - 1; + let one_64b : bits(64) = zero_extend(0b1); + let vAddrMask : bits(64) = (one_64b << shift) - one_64b; + let vMatchMask : bits(64) = ~ (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} } -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)) +// PRIVATE +function match_TLB_Entry(ent : TLB_Entry, + asid : bits(16), + vaddr : bits(64)) -> bool = + (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) { +// PRIVATE +function flush_TLB_Entry(e : TLB_Entry, + asid : option(bits(16)), + 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), (Some(i), Some(a)) => ( (e.asid == i) & (e.vAddr == (a & e.vMatchMask)) - & not(e.global)) + & not(e.global)) + } +} + +// PUBLIC: invoked in translate() [riscv_vmem.sail] +function lookup_TLB (asid : bits(16), 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 : bits(16), + vAddr : bits(64), + pAddr : bits(64), + pte : bits(64), + pteAddr : bits(64), + level : nat, + global : bool, + levelBitSize : nat, + PAGESIZE_BITS : nat) -> unit = { + let ent : TLB_Entry = make_TLB_Entry(asid, + global, + vAddr, + pAddr, + pte, + level, + pteAddr, + levelBitSize, + PAGESIZE_BITS); + tlb = Some(ent) +} + +// 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(bits(16)) = + 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 () } }