Compute deltaAddrUpper correctly in setAddress

The new version is formally verified to comply with the Sail specification.
This commit is contained in:
Dapeng Gao
2021-02-02 21:36:18 +08:00
committed by GitHub
parent 6e8df02532
commit 762f4a6a48

View File

@@ -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};