2 Commits

Author SHA1 Message Date
ed366654f0 saved compile time errors
Some checks failed
check properties / tests (push) Has been cancelled
2026-02-17 15:34:56 +00:00
b8f7b51e8a added latest changes 2026-02-17 14:49:00 +00:00
2 changed files with 30 additions and 18 deletions

View File

@@ -261,6 +261,7 @@ function Capability packCap(CapFat fat);
, flags: fat.flags , flags: fat.flags
, reserved: fat.reserved , reserved: fat.reserved
, otype: fat.otype , otype: fat.otype
, delta: fat.delta
, bounds: encBounds(fat.format,fat.bounds) , bounds: encBounds(fat.format,fat.bounds)
, address: fat.address }; , address: fat.address };
return pack(thin); return pack(thin);
@@ -886,6 +887,7 @@ instance DefaultValue #(CapFat);
, flags : 0 , flags : 0
, reserved : 0 , reserved : 0
, otype : otype_unsealed , otype : otype_unsealed
, delta : 0
, format : EmbeddedExp , format : EmbeddedExp
, bounds : defaultValue , bounds : defaultValue
, address : 0 , address : 0
@@ -898,6 +900,7 @@ CapFat null_cap = CapFat {
, flags : 0 , flags : 0
, reserved : 0 , reserved : 0
, otype : otype_unsealed , otype : otype_unsealed
, delta : 0
, format : EmbeddedExp , format : EmbeddedExp
, bounds : defaultValue , bounds : defaultValue
, address : 0 , address : 0
@@ -1166,6 +1169,10 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta
////////////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////
function setBoundsCombined = function setBoundsCombined =
error ("setBoundsCombined not implemented for CapMem"); 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 setBounds = error ("setBounds not implemented for CapMem");
//function roundLength = error ("roundLength not implemented for CapMem"); //function roundLength = error ("roundLength not implemented for CapMem");
//function alignmentMask = error ("alignmentMask not implemented for CapMem"); //function alignmentMask = error ("alignmentMask not implemented for CapMem");
@@ -1337,6 +1344,10 @@ instance CHERICap #(CapReg, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta
// capability derivation (bounds set) // capability derivation (bounds set)
////////////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////////////
function setBoundsCombined (cap, length) = error ("setBoundsCombined not implemented for CapReg"); 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 setBounds = error ("setBounds not implemented for CapReg");
//function roundLength = error ("roundLength not implemented for CapReg"); //function roundLength = error ("roundLength not implemented for CapReg");
//function alignmentMask = error ("alignmentMask not implemented for CapReg"); //function alignmentMask = error ("alignmentMask not implemented for CapReg");

View File

@@ -1,23 +1,23 @@
module assert_prop_unique( // module assert_prop_unique(
input wire [63 : 0] prop_base, // input wire [63 : 0] prop_base,
input wire [63 : 0] prop_len, // input wire [63 : 0] prop_len,
input wire [63 : 0] prop_newBase, // input wire [63 : 0] prop_newBase,
input wire [63 : 0] prop_newLen // input wire [63 : 0] prop_newLen
); // );
wire prop_ok; // wire prop_ok;
module_prop_unique module_prop_unique_inst ( // module_prop_unique module_prop_unique_inst (
.prop_unique_base(prop_base), // .prop_unique_base(prop_base),
.prop_unique_len(prop_len), // .prop_unique_len(prop_len),
.prop_unique_newBase(prop_newBase), // .prop_unique_newBase(prop_newBase),
.prop_unique_newLen(prop_newLen), // .prop_unique_newLen(prop_newLen),
.prop_unique(prop_ok) // .prop_unique(prop_ok)
); // );
always @(*) begin // always @(*) begin
assert(prop_ok); // assert(prop_ok);
end // end
endmodule // endmodule
module assert_prop_exact( module assert_prop_exact(
input wire [63 : 0] prop_base, input wire [63 : 0] prop_base,
@@ -180,3 +180,4 @@ module assert_prop_setBounds(
always @(*) begin always @(*) begin
assert(prop_ok); assert(prop_ok);
end end
endmodule