diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index 05bd946..ea0a314 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -178,4 +178,11 @@ function Bool prop_isInBounds(CapAddr base, CapAddr len, CapAddr addr);
   return forallCap(base, len, addr, prop);
 endfunction
 
+(* noinline *)
+function Bool prop_fromToMem(CapMem in);
+  CapPipe cp = fromMem(unpack(in));
+  CapMem cm = pack(toMem(cp));
+  return (cm == in);
+endfunction
+
 endpackage
diff --git a/assertions.sv b/assertions.sv
index c362e87..64a06f2 100644
--- a/assertions.sv
+++ b/assertions.sv
@@ -145,3 +145,18 @@ module assert_prop_setAddr(
     assert(prop_ok);
   end
 endmodule
+
+module assert_prop_fromToMem(
+         input wire [128 : 0] prop_in,
+       );
+  wire prop_ok;
+
+  module_prop_fromToMem module_fromToMem(
+    .prop_fromToMem_in(prop_in),
+    .prop_fromToMem(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
diff --git a/check.sby b/check.sby
index c72b68e..9e26204 100644
--- a/check.sby
+++ b/check.sby
@@ -7,6 +7,7 @@ prop_getTop
 prop_getLength
 prop_isInBounds
 prop_setAddr
+prop_fromToMem
 
 [options]
 depth 1
@@ -25,6 +26,7 @@ read -formal module_prop_getTop.v
 read -formal module_prop_getLength.v
 read -formal module_prop_isInBounds.v
 read -formal module_prop_setAddr.v
+read -formal module_prop_fromToMem.v
 prop_getBase: prep -top assert_prop_getBase
 prop_getTop: prep -top assert_prop_getTop
 prop_getLength: prep -top assert_prop_getLength
@@ -33,6 +35,7 @@ prop_unique: prep -top assert_prop_unique
 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
 
 [files]
 assertions.sv
@@ -44,3 +47,4 @@ module_prop_getTop.v
 module_prop_getLength.v
 module_prop_isInBounds.v
 module_prop_setAddr.v
+module_prop_fromToMem.v