saved compile time errors

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

@@ -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
   //////////////////////////////////////////////////////////////////////////////
@@ -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
   //////////////////////////////////////////////////////////////////////////////
 

Makefile

@@ -45,5 +45,5 @@ clean-counterexamples:
 
 clean:
 	rm -rf $(BUILD_DIR)
-
+	
 full-clean: clean clean-counterexamples

assertions.sv

@@ -1,23 +1,23 @@
-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 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 [63 : 0] prop_base,

check.sby

@@ -51,4 +51,3 @@ counterexamples/module_prop_getLength.v
 counterexamples/module_prop_isInBounds.v
 counterexamples/module_prop_setAddr.v
 counterexamples/module_prop_fromToMem.v
-counterexamples/module_prop_setBounds.v