Take into account tag clearing in setBounds.

2025-01-24 17:23:49 +00:00
parent c2fe9cc093
commit 7212f50b4d
1 changed files with 1 additions and 0 deletions
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -91,6 +91,7 @@ function Bool prop_unique(CapAddr base, CapAddr len,
  return baseCap.exact && expectedBaseCap.exact && implies
    ( boundedCap.exact && newBaseCap.exact &&
      finalCap.exact && expectedCap.exact &&
+      isValidCap(finalCap.value) &&
      newBase >= base && {1'b0, newBase} + {1'b0, newLen} <=
                         {1'b0, base}    + {1'b0, len}
    , toMem(expectedCap.value) == toMem(finalCap.value)