Some properties that pass through SymbiYosys

CHERICC_Fat.bsv

@@ -61,6 +61,8 @@ export SetBoundsReturn;
 export CapTrim;
 export trimCap;
 export untrimCap;
+export CapAddr;
+export CapAddrPlus1;
 
 // ===============================================================================
 

CHERICapProps.bsv

@@ -0,0 +1,180 @@
+/*
+ * Copyright (c) 2024 Matthew Naylor
+ * All rights reserved.
+ *
+ * This software was developed by SRI International and the University of
+ * Cambridge Computer Laboratory under DARPA/AFRL contract FA8750-10-C-0237
+ * ("CTSRD"), as part of the DARPA CRASH research programme.
+ *
+ * @BERI_LICENSE_HEADER_START@
+ *
+ * Licensed to BERI Open Systems C.I.C. (BERI) under one or more contributor
+ * license agreements.  See the NOTICE file distributed with this work for
+ * additional information regarding copyright ownership.  BERI licenses this
+ * file to you under the BERI Hardware-Software License, Version 1.0 (the
+ * "License"); you may not use this file except in compliance with the
+ * License.  You may obtain a copy of the License at:
+ *
+ *   http://www.beri-open-systems.org/legal/license-1-0.txt
+ *
+ * Unless required by applicable law or agreed to in writing, Work distributed
+ * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
+ * CONDITIONS OF ANY KIND, either express or implied.  See the License for the
+ * specific language governing permissions and limitations under the License.
+ *
+ * @BERI_LICENSE_HEADER_END@
+ */
+
+package CHERICapProps;
+
+import CHERICap :: *;
+import CHERICC_Fat :: *;
+
+// Helpers
+// =======
+
+// Bluespec does not seem to provide a boolean implication operator
+// (and Bool is not in Ord).
+
+function Bool implies(Bool x, Bool y) = !x || y;
+
+// Enumerating valid capabilities
+// ==============================
+
+// We assume that valid capabilities of all possible bounds are reachable
+// by calling setBounds on the almighty capability with arbitrary base and
+// length, ignoring those calls that return capabilities with inexact
+// bounds. (One possible exception is the almighty capability itself.) This
+// assumption is justified later.
+
+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)
+    );
+endfunction
+
+// Furthermore, every valid capability can be reached by calling setAddr on
+// the result with an arbitrary address. (Only caring about bounds and
+// addresses of capabilities here.)
+
+function Bool forallCap(CapAddr base, CapAddr len, CapAddr addr,
+                              function Bool prop(CapPipe cap));
+  function forall(cap);
+    Exact#(CapPipe) arbitraryCap = setAddr(cap, addr);
+    return implies(arbitraryCap.exact, prop(arbitraryCap.value));
+  endfunction
+  return forallBaseAndLen(base, len, forall);
+endfunction
+
+// The following two properties help justify the above assumption.
+
+// First, if we call setBounds twice in succession (starting from
+// almighty), then we end up with a capability that could have been
+// determined with a single setBounds call (also starting from almighty).
+// In other words, we can repeatedly shorten chain of setBounds calls to a
+// single call starting from almighty.
+
+(* noinline *)
+function Bool prop_unique(CapAddr base, CapAddr len,
+                          CapAddr newBase, CapAddr newLen);
+  Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
+  Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
+  Exact#(CapPipe) newBaseCap = setAddr(boundedCap.value, newBase);
+  Exact#(CapPipe) finalCap = setBounds(newBaseCap.value, newLen);
+  Exact#(CapPipe) expectedBaseCap = setAddr(almightyCap, newBase);
+  Exact#(CapPipe) expectedCap =
+    setBounds(expectedBaseCap.value, newLen);
+  return baseCap.exact && expectedBaseCap.exact && implies
+    ( boundedCap.exact && newBaseCap.exact &&
+      finalCap.exact && expectedCap.exact &&
+      newBase >= base && {1'b0, newBase} + {1'b0, newLen} <=
+                         {1'b0, base}    + {1'b0, len}
+    , toMem(expectedCap.value) == toMem(finalCap.value)
+    );
+endfunction
+
+// Second, if setBounds returns a capability with inexact bounds, then
+// there exists a different call to setBounds that returns the same
+// capability with exact bounds.
+
+(* noinline *)
+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));
+  return baseCap.exact && baseCap2.exact && implies
+           ( truncateLSB(length) == 1'b0
+           , boundedCap2.exact
+           );
+endfunction
+
+// There are certain conditions under which setBounds must return a
+// capability with exact bounds.
+
+(* noinline *)
+function Bool prop_exactConditions(CapAddr base, CapAddr len);
+  SetBoundsReturn#(CapPipe, CapAddrW) sb = setBoundsCombined(nullCap, len);
+  Exact#(CapPipe) baseCap = setAddr(almightyCap, base & sb.mask);
+  Exact#(CapPipe) boundedCap = setBounds(baseCap.value, sb.length);
+  return baseCap.exact && boundedCap.exact;
+endfunction
+
+// Properties
+// ==========
+
+(* noinline *)
+function Bool prop_getBase(CapAddr base, CapAddr len, CapAddr addr);
+  function prop(cap) = getBase(cap) == base;
+  return forallCap(base, len, addr, prop);
+endfunction
+
+(* noinline *)
+function Bool prop_getTop(CapAddr base, CapAddr len, CapAddr addr);
+  function prop(cap) = getTop(cap) == zeroExtend(base) + zeroExtend(len);
+  return forallCap(base, len, addr, prop);
+endfunction
+
+(* noinline *)
+function Bool prop_getLength(CapAddr base, CapAddr len, CapAddr addr);
+  function prop(cap) = getLength(cap) == zeroExtend(len);
+  return forallCap(base, len, addr, prop);
+endfunction
+
+(* noinline *)
+function Bool prop_setAddr(CapAddr base, CapAddr len, CapAddr addr);
+  Integer tolerance = 32; /* How far out-of-bounds can we go in general? */
+  function prop(cap);
+    Exact#(CapPipe) tmp = setAddr(cap, addr);
+    Int#(TAdd#(CapAddrW,2)) addrInt = unpack(zeroExtend(addr));
+    Int#(TAdd#(CapAddrW,2)) baseInt = unpack(zeroExtend(base));
+    Int#(TAdd#(CapAddrW,2)) lenInt = unpack(zeroExtend(len));
+    let low = baseInt - fromInteger(tolerance);
+    let high = baseInt + lenInt + fromInteger(tolerance);
+    return implies( addrInt >= low && addrInt <= high
+                  , tmp.exact && getAddr(tmp.value) == addr );
+  endfunction
+  return forallBaseAndLen(base, len, prop);
+endfunction
+
+(* noinline *)
+function Bool prop_isInBounds(CapAddr base, CapAddr len, CapAddr addr);
+  function prop(cap);
+    // TODO: the nowrap condition is required (but probably should not be)
+    Bool nowrap = truncateLSB({1'b0, base} + {1'b0, len}) == 1'b0;
+    return implies
+             ( nowrap
+             , isInBounds(cap, False) ==
+                 (getAddr(cap) >= getBase(cap) &&
+                    zeroExtend(getAddr(cap)) < getTop(cap))
+             );
+  endfunction
+  return forallCap(base, len, addr, prop);
+endfunction
+
+endpackage

Makefile

@@ -15,6 +15,9 @@ all: verilog-wrappers blarney-wrappers
 verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
 	bsc $(BSCFLAGS) -verilog -u $<
 
+verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
+	bsc $(BSCFLAGS) -verilog -u $<
+
 blarney-wrappers: CHERICapWrap.py verilog-wrappers
 	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
 

assertions.sv

@@ -0,0 +1,147 @@
+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_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
+
+module assert_prop_exact(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_len
+       );
+  wire prop_ok;
+
+  module_prop_exact module_prop_exact_inst (
+    .prop_exact_base(prop_base),
+    .prop_exact_len(prop_len),
+    .prop_exact(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
+
+module assert_prop_exactConditions(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_len
+       );
+  wire prop_ok;
+
+  module_prop_exactConditions module_prop_exactConditions_inst (
+    .prop_exactConditions_base(prop_base),
+    .prop_exactConditions_len(prop_len),
+    .prop_exactConditions(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
+
+module assert_prop_getBase(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_len
+       );
+  wire prop_ok;
+
+  module_prop_getBase module_prop_getBase_inst(
+    .prop_getBase_base(prop_base),
+    .prop_getBase_len(prop_len),
+    .prop_getBase(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
+
+module assert_prop_getTop(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_len,
+         input wire [31 : 0] prop_addr
+       );
+  wire prop_ok;
+
+  module_prop_getTop module_prop_getTop_inst(
+    .prop_getTop_base(prop_base),
+    .prop_getTop_len(prop_len),
+    .prop_getTop_addr(prop_addr),
+    .prop_getTop(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
+
+module assert_prop_getLength(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_addr,
+         input wire [31 : 0] prop_len
+       );
+  wire prop_ok;
+
+  module_prop_getLength module_prop_getLength_inst(
+    .prop_getLength_base(prop_base),
+    .prop_getLength_len(prop_len),
+    .prop_getLength_addr(prop_addr),
+    .prop_getLength(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
+
+module assert_prop_isInBounds(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_len,
+         input wire [31 : 0] prop_addr
+       );
+  wire prop_ok;
+
+  module_prop_isInBounds module_prop_isInBounds_inst(
+    .prop_isInBounds_base(prop_base),
+    .prop_isInBounds_len(prop_len),
+    .prop_isInBounds_addr(prop_addr),
+    .prop_isInBounds(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
+
+module assert_prop_setAddr(
+         input wire [31 : 0] prop_base,
+         input wire [31 : 0] prop_len,
+         input wire [31 : 0] prop_addr
+       );
+  wire prop_ok;
+
+  module_prop_setAddr module_prop_setAddr_inst(
+    .prop_setAddr_base(prop_base),
+    .prop_setAddr_len(prop_len),
+    .prop_setAddr_addr(prop_addr),
+    .prop_setAddr(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule

check.sby

@@ -0,0 +1,46 @@
+[tasks]
+prop_unique
+prop_exact
+prop_exactConditions
+prop_getBase
+prop_getTop
+prop_getLength
+prop_isInBounds
+prop_setAddr
+
+[options]
+depth 1
+mode bmc
+
+[engines]
+smtbmc boolector
+
+[script]
+read -formal assertions.sv
+read -formal module_prop_unique.v
+read -formal module_prop_exact.v
+read -formal module_prop_exactConditions.v
+read -formal module_prop_getBase.v
+read -formal module_prop_getTop.v
+read -formal module_prop_getLength.v
+read -formal module_prop_isInBounds.v
+read -formal module_prop_setAddr.v
+prop_getBase: prep -top assert_prop_getBase
+prop_getTop: prep -top assert_prop_getTop
+prop_getLength: prep -top assert_prop_getLength
+prop_isInBounds: prep -top assert_prop_isInBounds
+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
+
+[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

readme.adoc

@@ -74,4 +74,15 @@ by running
 within the OpenTitan GitHub repository as of commit
 https://github.com/lowRISC/opentitan/commit/2438b17afe4fef0d815be2e890763c288c449918
 
+== Formal Verification
 
+A small number of properties have been specified in `CHERICapProp.bsv`.
+These can be verfied using SymbiYosys, e.g.
+
+```
+wget https://github.com/YosysHQ/oss-cad-suite-build/releases/download/2024-07-17/oss-cad-suite-linux-x64-20240717.tgz
+tar xzf oss-cad-suite-linux-x64-20240717.tgz
+export PATH=`pwd`/oss-cad-suite/bin:$PATH
+make verilog-props
+sby -f check.sby
+```