diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv index ed6b2e4..b48bf47 100644 --- a/CHERICC_Fat.bsv +++ b/CHERICC_Fat.bsv @@ -61,6 +61,8 @@ export SetBoundsReturn; export CapTrim; export trimCap; export untrimCap; +export CapAddr; +export CapAddrPlus1; // =============================================================================== diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv new file mode 100644 index 0000000..ad89ec4 --- /dev/null +++ b/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 diff --git a/Makefile b/Makefile index d6d327a..635c7bc 100644 --- a/Makefile +++ b/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 diff --git a/assertions.sv b/assertions.sv new file mode 100644 index 0000000..c362e87 --- /dev/null +++ b/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 diff --git a/check.sby b/check.sby new file mode 100644 index 0000000..c72b68e --- /dev/null +++ b/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 diff --git a/readme.adoc b/readme.adoc index 5f64d2a..3f2faa1 100644 --- a/readme.adoc +++ b/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 +```