Skip to content

Commit

Permalink
clarify top bound and how it feeds into rep range check
Browse files Browse the repository at this point in the history
  • Loading branch information
tariqkurd-repo committed Jan 30, 2025
1 parent 3d4c1e8 commit 4affbef
Showing 1 changed file with 7 additions and 3 deletions.
10 changes: 7 additions & 3 deletions src/cap-description.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -717,3 +717,7 @@ xref:section_cap_encoding[xrefstyle=short].
This gives useful guarantees, such that if an executed instruction is in
<<pcc>> 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.

0 comments on commit 4affbef

Please sign in to comment.