diff --git a/src/cap-description.adoc b/src/cap-description.adoc index 28a6a3b0..c7aba2d6 100644 --- a/src/cap-description.adoc +++ b/src/cap-description.adoc @@ -448,8 +448,8 @@ T[MW - 1:MW - 2] = B[MW - 1:MW - 2] + LCout + LMSB Decoding the bounds: ``` -top: t = { a[MXLEN - 1:E + MW] + ct, T[MW - 1:0] , {E{1'b0}} } -base: b = { a[MXLEN - 1:E + MW] + cb, B[MW - 1:0] , {E{1'b0}} } +top: t = { 1'b0, a[MXLEN - 1:E + MW] + ct, T[MW - 1:0], {E{1'b0}} } +base: b = { a[MXLEN - 1:E + MW] + cb, B[MW - 1:0], {E{1'b0}} } ``` The corrections c~t~ and c~b~ are calculated as as shown below using the definitions in xref:cap_encoding_ct[xrefstyle=short] and @@ -691,7 +691,7 @@ bounds are formed of two or three sections: | EF=1, i.e. E=0 | address[MXLEN:MW] + ct 2+| T[MW - 1:0] |============================================================================== -The top described by xref:comp_addr_bounds[xrefstyle=short] is MXLEN+1 bits +The top bound described by xref:comp_addr_bounds[xrefstyle=short] is MXLEN+1 bits wide to allow capabilities to span the whole address space. The address is zero-extended by one bit. The malformed check (see xref:section_cap_malformed[xrefstyle=short]) ensures that the top never @@ -717,3 +717,7 @@ xref:section_cap_encoding[xrefstyle=short]. This gives useful guarantees, such that if an executed instruction is in <> bounds, then it is also guaranteed that the next linear instruction is _representable_. + +NOTE: Even though address[MXLEN] in xref:comp_addr_bounds[xrefstyle=short] affects + the value of the top bound, it does not have an affect on the _representable range_ + calculation and so can be excluded from the check.