satp.PPN's WARLness is separate from physical address validity

2 files changed, 8 insertions, 7 deletions

diff --git a/src/hypervisor.tex b/src/hypervisor.tex
index 305f5dd..3c34ce6 100644
--- a/src/hypervisor.tex
+++ b/src/hypervisor.tex
@@ -905,9 +905,7 @@ In these modes, the lowest two bits of the physical page number (PPN) in
 An implementation that supports only the defined paged virtual-memory schemes
 and/or Bare may hardwire PPN[1:0] to zero.
 
-The number of supervisor physical address bits is implementation-defined; any
-unimplemented address bits are hardwired to zero in {\tt hgatp}.PPN.
-The number of VMID bits is also implementation-defined and may be zero.
+The number of VMID bits is \unspecified\ and may be zero.
 The number of implemented VMID bits, termed {\mbox {\em VMIDLEN}}, may be
 determined by writing one to every bit position in the VMID field, then reading
 back the value in {\tt hgatp} to see which bit positions in the VMID field hold
diff --git a/src/supervisor.tex b/src/supervisor.tex
index 7763751..1168aa0 100644
--- a/src/supervisor.tex
+++ b/src/supervisor.tex
@@ -814,6 +814,12 @@ register are described in Section~\ref{virt-control}.
 \begin{commentary}
 Storing a PPN in {\tt satp}, rather than a physical address, supports
 a physical address space larger than \wunits{4}{GiB} for RV32.
+
+The {\tt satp}.PPN field might not be capable of holding all physical page
+numbers.
+Some platforms might place constraints on the values {\tt satp}.PPN may
+assume, e.g., by requiring that all physical page numbers corresponding to
+main memory be representable.
 \end{commentary}
 
 \begin{figure}[h!]
@@ -906,9 +912,7 @@ Value  & Name & Description \\
 \label{tab:satp-mode}
 \end{table}
 
-The number of supervisor physical address bits is \unspecified; any
-unimplemented address bits are hardwired to zero in the {\tt satp} register.
-The number of ASID bits is also \unspecified\ and may be zero.  The
+The number of ASID bits is \unspecified\ and may be zero.  The
 number of implemented ASID bits, termed {\mbox {\em ASIDLEN}}, may be
 determined by writing one to every bit position in the ASID field, then
 reading back the value in {\tt satp} to see which bit positions in the ASID
@@ -916,7 +920,6 @@ field hold a one.  The least-significant bits of ASID are implemented first:
 that is, if ASIDLEN~$>$~0, ASID[ASIDLEN-1:0] is writable.  The maximal value
 of ASIDLEN, termed ASIDMAX, is 9 for Sv32 or 16 for Sv39 and Sv48.
 
-
 \begin{commentary}
 For many applications, the choice of page size has a substantial
 performance impact.  A large page size increases TLB reach and loosens