From 762f4a6a48e4916077596c40cea125083761bbc1 Mon Sep 17 00:00:00 2001
From: Dapeng Gao <31944689+dpgao@users.noreply.github.com>
Date: Tue, 2 Feb 2021 21:36:18 +0800
Subject: [PATCH] Compute deltaAddrUpper correctly in setAddress

The new version is formally verified to comply with the Sail specification.
---
 CHERICC_Fat.bsv | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index 1e52b70..49fda6b 100644
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -655,7 +655,7 @@ function VnD#(CapFat) setAddress(CapFat cap, CapAddr address, TempFields tf);
   Bit#(TSub#(CapAddrW,MW)) deltaAddrHi = signExtend({1'b0,pack(newAddrHi)} - {1'b0,pack(tf.addrHi)}) << e;
   // Calculate the actual difference between the upper bits of the new address and the original address.
   Bit#(TSub#(CapAddrW,MW)) mask = -1 << e;
-  Bit#(TSub#(CapAddrW,MW)) deltaAddrUpper = (truncateLSB(cap.address)&mask) - (truncateLSB(address)&mask);
+  Bit#(TSub#(CapAddrW,MW)) deltaAddrUpper = (truncateLSB(address)&mask) - (truncateLSB(cap.address)&mask);
   Bool inRepBounds = deltaAddrHi == deltaAddrUpper;
   if (!inRepBounds) ret.isCapability = False;
   return VnD {v: inRepBounds, d: ret};