saved compile time errors

These were hardwired for RV64, but I'm assuming having too many
bits will not be a problem for RV32?

.github/workflows/check-prop.yml

@@ -0,0 +1,16 @@
+name: "check properties"
+on:
+  pull_request:
+  push:
+jobs:
+  tests:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - uses: cachix/install-nix-action@v27
+      with:
+        github_access_token: ${{ secrets.GITHUB_TOKEN }}
+    - name: Setup environment
+      run: nix develop --command make verilog-wrappers verilog-props
+    - name: Run property checks
+      run: nix develop --command make check-prop

.gitignore

@@ -0,0 +1,2 @@
+build/
+counterexamples/

CHERICC_Fat.bsv

@@ -40,6 +40,8 @@ export CapPipe;
 export CapFat;
 export MW;
 export OTypeW;
+export Delta;
+export setDeltaValue;
 export FlagsW;
 export Perms;
 export ResW;
@@ -59,8 +61,8 @@ export Exp;
 export MetaInfo;
 export SetBoundsReturn;
 export CapTrim;
-export trimCap;
-export untrimCap;
+// export trimCap;
+// export untrimCap;
 export CapAddr;
 export CapAddrPlus1;
 
@@ -84,17 +86,20 @@ typedef 0  UPermW;
 typedef 8  MW;
 typedef 6  ExpW;
 typedef 4  OTypeW;
+typedef 24  Delta;
 typedef `FLAGSW FlagsW;
 typedef 32 CapAddrW;
-typedef 64 CapW;
+typedef 88 CapW;
 `else // CAP128 is default
 typedef 4   UPermW;
 typedef 14  MW;
 typedef 6   ExpW;
 typedef 18  OTypeW;
+typedef 44  Delta;
 typedef `FLAGSW FlagsW;
 typedef 64  CapAddrW;
-typedef 128 CapW;
+// The capability width changes
+typedef 172 CapW;
 `endif
 
 // The Address type is used to represent the full sized address returned to the
@@ -139,8 +144,9 @@ typedef SizeOf#(Perms) PermsW;
 // The reserved bits
 typedef TSub#(CapW, TAdd#( CapAddrW
                          , TAdd#( OTypeW
-                                , TAdd#( CBoundsW
-                                       , TAdd#(PermsW, FlagsW))))) ResW;
+                                , TAdd#( Delta
+                                    , TAdd#( CBoundsW
+                                       , TAdd#(PermsW, FlagsW)))))) ResW;
 // The full capability structure, including the "tag" bit.
 typedef struct {
   Bool         isCapability;
@@ -148,6 +154,7 @@ typedef struct {
   Bit#(ResW)   reserved;
   Bit#(FlagsW) flags;
   Bit#(OTypeW) otype;
+  Bit#(Delta) delta;
   CBounds      bounds;
   CapAddr      address;
 } CapabilityInMemory deriving (Bits, Eq, FShow); // CapW + 1 (tag bit)
@@ -183,6 +190,7 @@ typedef struct {
   Bit#(FlagsW)   flags;
   Bit#(ResW)     reserved;
   Bit#(OTypeW)   otype;
+  Bit#(Delta)    delta;
   Format         format;
   Bounds         bounds;
 } CapFat deriving (Bits);
@@ -229,6 +237,7 @@ function CapFat unpackCap(Capability thin);
   fat.flags        = memCap.flags;
   fat.reserved     = memCap.reserved;
   fat.otype        = memCap.otype;
+  fat.delta        = memCap.delta;
   match {.f, .b}   = decBounds(memCap.bounds);
   fat.format       = f;
   fat.bounds       = b;
@@ -252,6 +261,7 @@ function Capability packCap(CapFat fat);
     , flags:        fat.flags
     , reserved:     fat.reserved
     , otype:        fat.otype
+    , delta:        fat.delta
     , bounds:       encBounds(fat.format,fat.bounds)
     , address:      fat.address };
   return pack(thin);
@@ -346,7 +356,7 @@ function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf)
   Bit #(TAdd #(MW, 2)) correctTop  = {pack (tf.topCorrection), topBits};
   // Get the length by subtracting base from top and shifting appropriately, and
   // saturate in case of big exponent
-  CapAddrPlus1 length =
+  CapAddr length =
     (exp >= resetExp) ? ~0 : zeroExtend (correctTop - correctBase) << exp;
 
   // compute repBase
@@ -437,12 +447,12 @@ function CapAddrPlus1 getTopFat(CapFat cap, TempFields tf);
     ret[valueOf(CapAddrW)] = ~ret[valueOf(CapAddrW)];
   return ret;
 endfunction
-function CapAddrPlus1 getLengthFat(CapFat cap, TempFields tf);
+function CapAddr getLengthFat(CapFat cap, TempFields tf);
   // Get the top and base bits with the 2 correction bits prepended
   Bit#(TAdd#(MW,2)) top  = {pack(tf.topCorrection),cap.bounds.topBits};
   Bit#(TAdd#(MW,2)) base = {pack(tf.baseCorrection),cap.bounds.baseBits};
   // Get the length by substracting base from top and shifting appropriately
-  CapAddrPlus1 length = zeroExtend(top - base) << cap.bounds.exp;
+  CapAddr length = zeroExtend(top - base) << cap.bounds.exp;
   // Return a saturated length in case of big exponent
   // TODO: The saturation behaviour here is short of being correct
   return (cap.bounds.exp >= resetExp) ? ~0 : length;
@@ -691,6 +701,13 @@ function CapFat unseal(CapFat cap, x _);
   ret.otype = otype_unsealed;
   return ret;
 endfunction
+// TODOD Creating Cap function to all delta value 
+// function CapFat addDelta(CapFat cap, x _);
+//   CapFat ret = cap;
+//   ret.delta = x;
+//   return ret;
+// endfunction
+
 function VnD#(CapFat) incOffsetFat( CapFat cap
                                   , CapAddr pointer
                                   , CapAddr offset // this is the increment in inc offset, and the offset in set offset
@@ -870,6 +887,7 @@ instance DefaultValue #(CapFat);
     , flags       : 0
     , reserved    : 0
     , otype       : otype_unsealed
+    , delta       : 0
     , format      : EmbeddedExp
     , bounds      : defaultValue
     , address     : 0
@@ -882,6 +900,7 @@ CapFat null_cap = CapFat {
   , flags       : 0
   , reserved    : 0
   , otype       : otype_unsealed
+  , delta       : 0
   , format      : EmbeddedExp
   , bounds      : defaultValue
   , address     : 0
@@ -1038,7 +1057,7 @@ typedef struct {
 // Note: commented out methods have a provided default implementation in the
 //       CHERICap typeclass definition
 
-instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
+instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta);
 
   // capability validity
   //////////////////////////////////////////////////////////////////////////////
@@ -1106,6 +1125,7 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
            , pack (cap.reserved)
            , pack (cap.flags)
            , pack (cap.otype)
+           , pack (cap.delta)
            , pack (cap.bounds) };
   endfunction
   function getAddr (capMem);
@@ -1149,6 +1169,10 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
   //////////////////////////////////////////////////////////////////////////////
   function setBoundsCombined =
     error ("setBoundsCombined not implemented for CapMem");
+
+  // Create function to set delta value 
+  function setDeltaValue (CapPipe cap, Bit#(Delta) delta) = error ("setDeltaValue not implemented for CapReg");
+
   //function setBounds = error ("setBounds not implemented for CapMem");
   //function roundLength = error ("roundLength not implemented for CapMem");
   //function alignmentMask = error ("alignmentMask not implemented for CapMem");
@@ -1196,7 +1220,7 @@ endinstance
 // Note: commented out methods have a provided default implementation in the
 //       CHERICap typeclass definition
 
-instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
+instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta);
 
   // capability validity
   //////////////////////////////////////////////////////////////////////////////
@@ -1320,6 +1344,10 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
   // capability derivation (bounds set)
   //////////////////////////////////////////////////////////////////////////////
   function setBoundsCombined (cap, length) = error ("setBoundsCombined not implemented for CapReg");
+
+  // Create function to set delta value 
+  function setDeltaValue (CapPipe cap, Bit#(Delta) delta) = error ("setDeltaValue not implemented for CapReg");
+
   //function setBounds = error ("setBounds not implemented for CapReg");
   //function roundLength = error ("roundLength not implemented for CapReg");
   //function alignmentMask = error ("alignmentMask not implemented for CapReg");
@@ -1344,7 +1372,7 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
 
 endinstance
 
-instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
+instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3), Delta);
 
   //Functions supported by CapReg are just passed through
 
@@ -1392,6 +1420,15 @@ instance CHERICap #(CapPipe, OTypeW, FlagsW, CapAddrW, CapW, TSub#(MW, 3));
       , mask: result.mask };
   endfunction
 
+  // Create function to set delta value 
+  function setDeltaValue (CapPipe cap, Bit#(Delta) delta);
+    // let result = setDelta(cap.capFat, delta);
+    cap.capFat.delta = delta;
+    return cap;
+  endfunction
+
+
+
   function nullWithAddr (addr);
     CapReg res = nullWithAddr(addr);
     return CapPipe { capFat: res, tempFields: getTempFields(res) };
@@ -1518,33 +1555,36 @@ typedef 48 VA_Width;
 typedef struct {
   Perms        perms;
   Bit#(FlagsW) flags;
+  Bit#(Delta)  delta;
   CBounds      bounds;
   Bit#(VA_Width)     address;
   Bool         validAddress;
 } CapTrim deriving(Bits, Eq, FShow);
-function CapTrim  trimCap(CapMem cm);
-  CapabilityInMemory cap = unpack(cm);
-  Bit#(TSub#(CapAddrW,VA_Width)) addr_upper = truncateLSB(cap.address);
-  return CapTrim{perms: cap.perms,
-                 flags: cap.flags,
-                 bounds: cap.bounds,
-                 address: truncate(cap.address),
-                 validAddress: (addr_upper==signExtend(cap.address[valueOf(VA_Width)-1]))
-  };
-endfunction
-function CapMem untrimCap(CapTrim ct);
-  // Encode an invalid address as the bit above the last valid bit being different.
-  Bit#(1) addressMsb = ct.address[valueOf(VA_Width)-1];
-  if (!ct.validAddress) addressMsb = ^addressMsb;
-  return pack(CapabilityInMemory{
-                isCapability: True,
-                perms: ct.perms,
-                reserved: 0,
-                flags: ct.flags,
-                otype: otype_unsealed,
-                bounds: ct.bounds,
-                address: signExtend({addressMsb,ct.address})
-  });
-endfunction
+// function CapTrim  trimCap(CapMem cm);
+//   CapabilityInMemory cap = unpack(cm);
+//   Bit#(TSub#(CapAddrW,VA_Width)) addr_upper = truncateLSB(cap.address);
+//   return CapTrim{perms: cap.perms,
+//                  flags: cap.flags,
+//                  delta: cap.delta,
+//                  bounds: cap.bounds,  
+//                  address: truncate(cap.address),
+//                  validAddress: (addr_upper==signExtend(cap.address[valueOf(VA_Width)-1]))
+//   };
+// endfunction
+// function CapMem untrimCap(CapTrim ct);
+//   // Encode an invalid address as the bit above the last valid bit being different.
+//   Bit#(1) addressMsb = ct.address[valueOf(VA_Width)-1];
+//   if (!ct.validAddress) addressMsb = ^addressMsb;
+//   return pack(CapabilityInMemory{
+//                 isCapability: True,
+//                 perms: ct.perms,
+//                 reserved: 0,
+//                 flags: ct.flags,
+//                 otype: otype_unsealed,
+//                 delta: ct.delta,
+//                 bounds: ct.bounds,
+//                 address: signExtend({addressMsb,ct.address})
+//   });
+// endfunction
 
 endpackage

CHERICap.bsv

@@ -80,7 +80,7 @@ typedef union tagged {
 typedef struct {
   Bit #(addrW) base;
   Bit #(TAdd #(addrW, 1)) top;
-  Bit #(TAdd #(addrW, 1)) length;
+  Bit #(addrW) length;
   Bit #(addrW) repBase;
   Bit #(TAdd #(addrW, 1)) repTop;
   Bit #(TAdd #(addrW, 1)) repLength;
@@ -119,7 +119,7 @@ endfunction
 
 // XXX TODO augment with all architectural bounds/ repbounds ?
 function Fmt showCHERICap (capT cap)
-  provisos (CHERICap #(capT , otypeW, flgW, addrW, inMemW, maskableW));
+  provisos (CHERICap #(capT , otypeW, flgW, addrW, inMemW, maskableW, delta));
   return $format( "Valid: 0x%0x", isValidCap(cap)) +
          $format(" Perms: 0x%0x", getPerms(cap)) +
          $format(" Kind: ", fshow(getKind(cap))) +
@@ -153,8 +153,9 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
                     , numeric type addrW     // width of the address
                     , numeric type inMemW    // width of the capability in mem
                     , numeric type maskableW // width of maskable bits
+                    , numeric type delta     // size of delta (tlb bypass)
                     )
-  dependencies (capT determines (otypeW, flgW, addrW, inMemW, maskableW));
+  dependencies (capT determines (otypeW, flgW, addrW, inMemW, maskableW, delta));
 
   // capability validity
   //////////////////////////////////////////////////////////////////////////////
@@ -258,7 +259,7 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
   // Get the top
   function Bit #(TAdd #(addrW, 1)) getTop (capT cap) = getBoundsInfo(cap).top;
   // Get the length
-  function Bit #(TAdd #(addrW, 1)) getLength (capT cap) =
+  function Bit #(addrW) getLength (capT cap) =
     getBoundsInfo(cap).length;
   // Assertion that the capability's address is between its base and top
   function Bool isInBounds (capT cap, Bool isTopIncluded) =
@@ -320,6 +321,9 @@ typeclass CHERICap #( type capT              // type of the CHERICap capability
   // the null capability (requires a dummy proxy)
   function capT nullCapFromDummy (capT dummy);
 
+  // define set delta function
+  function capT setDeltaValue (capT cap, Bit #(delta) length);
+
   // Assert that the encoding is valid
   //////////////////////////////////////////////////////////////////////////////
 

CHERICapProps.bsv

@@ -49,12 +49,18 @@ function Bool implies(Bool x, Bool y) = !x || y;
 
 function Bool forallBaseAndLen(CapAddr base, CapAddr len,
                                  function Bool prop(CapPipe cap));
-  Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
-  Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
-  return baseCap.exact && implies
-    ( boundedCap.exact 
-    , prop(boundedCap.value)
-    );
+  Bool ret = ?;
+  if (base == 0 && ~len == 0) begin
+    ret = prop(almightyCap);
+  end else begin
+    Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
+    Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
+    ret = baseCap.exact && implies
+      ( boundedCap.exact
+      , prop(boundedCap.value)
+      );
+  end
+  return ret;
 endfunction
 
 // Furthermore, every valid capability can be reached by calling setAddr on
@@ -107,10 +113,10 @@ function Bool prop_exact(CapAddr base, CapAddr len);
   Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
   Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
   Exact#(CapPipe) baseCap2 = setAddr(almightyCap, getBase(boundedCap.value));
-  CapAddrPlus1 length = getLength(boundedCap.value);
-  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, truncate(length));
+  CapAddr length = getLength(boundedCap.value);
+  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, length);
   return baseCap.exact && baseCap2.exact && implies
-           ( truncateLSB(length) == 1'b0
+           ( ~length != 0
            , boundedCap2.exact
            );
 endfunction
@@ -137,7 +143,8 @@ endfunction
 
 (* noinline *)
 function Bool prop_getTop(CapAddr base, CapAddr len, CapAddr addr);
-  function prop(cap) = getTop(cap) == zeroExtend(base) + zeroExtend(len);
+  Bool reqAlmighty = ~len == 0;
+  function prop(cap) = getTop(cap) == zeroExtend(base) + (reqAlmighty ? {1'b1, 0} : zeroExtend(len));
   return forallCap(base, len, addr, prop);
 endfunction
 
@@ -185,4 +192,16 @@ function Bool prop_fromToMem(CapMem in);
   return (cm == in);
 endfunction
 
+(* noinline *)
+function Bool prop_setBounds(CapAddr base, CapAddr len, CapAddr addr, CapAddr new_len);
+  function prop(cap);
+    let new_cap = setBounds(cap,new_len).value;
+    return implies( isValidCap(new_cap),
+                    getBase(cap) <= getBase(new_cap)
+                    && getTop(cap) >= getTop(new_cap)
+                  );
+  endfunction
+  return forallCap(base, len, addr, prop);
+endfunction
+
 endpackage

CHERICapWrap.bsv

@@ -74,6 +74,8 @@ function Bit#(CapAddrW) `W(getAddr) (`CAPTYPE cap) = getAddr(cap);
 (* noinline *)
 function `CAPTYPE `W(setAddrUnsafe) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capRet(setAddrUnsafe(capArg(cap), addr));
 (* noinline *)
+function `CAPTYPE `W(addAddrUnsafe) (`CAPTYPE cap, Bit#(TSub #(MW, 3)) inc) = capRet(addAddrUnsafe(capArg(cap), inc));
+(* noinline *)
 function Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capExactRet(setAddr(capArg(cap), addr));
 (* noinline *)
 function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(capArg(cap));
@@ -88,7 +90,7 @@ function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(capArg(cap));
 (* noinline *)
 function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(capArg(cap));
 (* noinline *)
-function Bit#(TAdd#(CapAddrW, 1)) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
+function Bit#(CapAddrW) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
 (* noinline *)
 function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(capArg(cap), isTopIncluded);
 (* noinline *)

Makefile

@@ -1,4 +1,4 @@
-CAP ?= 64
+CAP ?= 128
 ifeq ($(CAP), 128)
 BSCFLAGS = -D CAP128
 else
@@ -13,27 +13,37 @@ ifeq ($(ARCH), RISCV)
 BSCFLAGS += -D RISCV
 endif
 
+BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)/build/
+BUILD_DIR = $(BSV_VERILOG_WRAPPERS_DIR)
+COUNTEREXAMPLE_DIR = $(CURDIR)/counterexamples/
+BSCFLAGS += -bdir $(BUILD_DIR)
+
 all: verilog-wrappers blarney-wrappers
 
-verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(BUILD_DIR):
+	mkdir -p $@
 
-verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(COUNTEREXAMPLE_DIR):
+	mkdir -p $@
 
-check-prop: assertions.sv verilog-wrappers verilog-props
-	sby -f check.sby
+verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR)
+	bsc $(BSCFLAGS) -vdir $(BSV_VERILOG_WRAPPERS_DIR) -verilog -u $<
 
-blarney-wrappers: CHERICapWrap.py verilog-wrappers
-	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
+verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR) $(COUNTEREXAMPLE_DIR)
+	bsc $(BSCFLAGS) -vdir $(COUNTEREXAMPLE_DIR) -verilog -u $<
 
-.PHONY: clean clean-verilog-wrappers
+check-prop: assertions.sv verilog-props $(COUNTEREXAMPLE_DIR)
+	sby --prefix $(COUNTEREXAMPLE_DIR) -f check.sby
 
-clean-verilog-wrappers: clean
-	rm -f *.v
+blarney-wrappers: CHERICapWrap.py verilog-wrappers $(BUILD_DIR)
+	./CHERICapWrap.py -o $(BUILD_DIR)/CHERIBlarneyWrappers $(BUILD_DIR)/*.v
 
-clean-blarney-wrappers: clean
-	rm -f *.hs
+.PHONY: clean clean-counterexamples full-clean
+
+clean-counterexamples:
+	rm -rf $(COUNTEREXAMPLE_DIR)
 
 clean:
-	rm -f *.bo
+	rm -rf $(BUILD_DIR)
+	
+full-clean: clean clean-counterexamples

assertions.sv

@@ -1,27 +1,27 @@
-module assert_prop_unique(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_newBase,
-         input wire [31 : 0] prop_newLen
-       );
-  wire prop_ok;
+// module assert_prop_unique(
+//          input wire [63 : 0] prop_base,
+//          input wire [63 : 0] prop_len,
+//          input wire [63 : 0] prop_newBase,
+//          input wire [63 : 0] prop_newLen
+//        );
+//   wire prop_ok;
 
-  module_prop_unique module_prop_unique_inst (
-    .prop_unique_base(prop_base),
-    .prop_unique_len(prop_len),
-    .prop_unique_newBase(prop_newBase),
-    .prop_unique_newLen(prop_newLen),
-    .prop_unique(prop_ok)
-  );
+//   module_prop_unique module_prop_unique_inst (
+//     .prop_unique_base(prop_base),
+//     .prop_unique_len(prop_len),
+//     .prop_unique_newBase(prop_newBase),
+//     .prop_unique_newLen(prop_newLen),
+//     .prop_unique(prop_ok)
+//   );
 
-  always @(*) begin
-    assert(prop_ok);
-  end
-endmodule
+//   always @(*) begin
+//     assert(prop_ok);
+//   end
+// endmodule
 
 module assert_prop_exact(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -37,8 +37,8 @@ module assert_prop_exact(
 endmodule
 
 module assert_prop_exactConditions(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -54,8 +54,8 @@ module assert_prop_exactConditions(
 endmodule
 
 module assert_prop_getBase(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -71,9 +71,9 @@ module assert_prop_getBase(
 endmodule
 
 module assert_prop_getTop(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
        );
   wire prop_ok;
 
@@ -90,9 +90,9 @@ module assert_prop_getTop(
 endmodule
 
 module assert_prop_getLength(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_addr,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -109,9 +109,9 @@ module assert_prop_getLength(
 endmodule
 
 module assert_prop_isInBounds(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
        );
   wire prop_ok;
 
@@ -128,9 +128,9 @@ module assert_prop_isInBounds(
 endmodule
 
 module assert_prop_setAddr(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
        );
   wire prop_ok;
 
@@ -160,3 +160,24 @@ module assert_prop_fromToMem(
     assert(prop_ok);
   end
 endmodule
+
+module assert_prop_setBounds(
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_new_len
+       );
+  wire prop_ok;
+
+  module_prop_setBounds module_prop_setBounds_inst(
+    .prop_setBounds_base(prop_base),
+    .prop_setBounds_len(prop_len),
+    .prop_setBounds_addr(prop_addr),
+    .prop_setBounds_new_len(prop_new_len),
+    .prop_setBounds(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule

check.sby

@@ -8,6 +8,7 @@ prop_getLength
 prop_isInBounds
 prop_setAddr
 prop_fromToMem
+prop_setBounds
 
 [options]
 depth 1
@@ -27,6 +28,7 @@ read -formal module_prop_getLength.v
 read -formal module_prop_isInBounds.v
 read -formal module_prop_setAddr.v
 read -formal module_prop_fromToMem.v
+read -formal module_prop_setBounds.v
 prop_getBase: prep -top assert_prop_getBase
 prop_getTop: prep -top assert_prop_getTop
 prop_getLength: prep -top assert_prop_getLength
@@ -36,15 +38,16 @@ prop_exact: prep -top assert_prop_exact
 prop_exactConditions: prep -top assert_prop_exactConditions
 prop_setAddr: prep -top assert_prop_setAddr
 prop_fromToMem: prep -top assert_prop_fromToMem
+prop_setBounds: prep -top assert_prop_setBounds
 
 [files]
 assertions.sv
-module_prop_unique.v
-module_prop_exact.v
-module_prop_exactConditions.v
-module_prop_getBase.v
-module_prop_getTop.v
-module_prop_getLength.v
-module_prop_isInBounds.v
-module_prop_setAddr.v
-module_prop_fromToMem.v
+counterexamples/module_prop_unique.v
+counterexamples/module_prop_exact.v
+counterexamples/module_prop_exactConditions.v
+counterexamples/module_prop_getBase.v
+counterexamples/module_prop_getTop.v
+counterexamples/module_prop_getLength.v
+counterexamples/module_prop_isInBounds.v
+counterexamples/module_prop_setAddr.v
+counterexamples/module_prop_fromToMem.v

flake.lock

@@ -0,0 +1,61 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1738579205,
+        "narHash": "sha256-o6BeeanSUALvz8oL2CHOikVjCf7j+HqlA0WGvKOUX3Q=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "be5cf18b3d26ba2db938a72ade93ac8a9a7462ff",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "release-24.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}

flake.nix

@@ -0,0 +1,25 @@
+{
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/release-24.11";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let # helper bindings
+        # imported nix packages
+        pkgs = import nixpkgs { inherit system; };
+        # shell environment
+        dfltShell = pkgs.mkShell {
+          buildInputs = with pkgs; [
+            sby
+            boolector
+            haskellPackages.sv2v
+            bluespec
+          ];
+        };
+      # output attribute set
+      in {
+        devShells.default = dfltShell;
+      }
+    );
+}