diff --git a/.github/workflows/check-prop.yml b/.github/workflows/check-prop.yml new file mode 100644 index 0000000..c1a05c3 --- /dev/null +++ b/.github/workflows/check-prop.yml @@ -0,0 +1,16 @@ +name: "check properties" +on: + pull_request: + push: +jobs: + tests: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: cachix/install-nix-action@v27 + with: + github_access_token: ${{ secrets.GITHUB_TOKEN }} + - name: Setup environment + run: nix develop --command make verilog-wrappers verilog-props + - name: Run property checks + run: nix develop --command make check-prop diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv index 7036bd1..6fec091 100644 --- a/CHERICC_Fat.bsv +++ b/CHERICC_Fat.bsv @@ -1,6 +1,6 @@ /* * Copyright (c) 2015-2019 Jonathan Woodruff - * Copyright (c) 2017-2021 Alexandre Joannou + * Copyright (c) 2017-2025 Alexandre Joannou * Copyright (c) 2019 Peter Rugg * Copyright (c) 2021 Dapeng Gao * All rights reserved. @@ -355,7 +355,7 @@ function BoundsInfo#(CapAddrW) getBoundsInfoFat (CapFat cap, TempFields tf) Bit #(TAdd #(MW, 2)) correctTop = {pack (tf.topCorrection), topBits}; // Get the length by subtracting base from top and shifting appropriately, and // saturate in case of big exponent - CapAddrPlus1 length = + CapAddr length = (exp >= resetExp) ? ~0 : zeroExtend (correctTop - correctBase) << exp; // compute repBase @@ -446,12 +446,12 @@ function CapAddrPlus1 getTopFat(CapFat cap, TempFields tf); ret[valueOf(CapAddrW)] = ~ret[valueOf(CapAddrW)]; return ret; endfunction -function CapAddrPlus1 getLengthFat(CapFat cap, TempFields tf); +function CapAddr getLengthFat(CapFat cap, TempFields tf); // Get the top and base bits with the 2 correction bits prepended Bit#(TAdd#(MW,2)) top = {pack(tf.topCorrection),cap.bounds.topBits}; Bit#(TAdd#(MW,2)) base = {pack(tf.baseCorrection),cap.bounds.baseBits}; // Get the length by substracting base from top and shifting appropriately - CapAddrPlus1 length = zeroExtend(top - base) << cap.bounds.exp; + CapAddr length = zeroExtend(top - base) << cap.bounds.exp; // Return a saturated length in case of big exponent // TODO: The saturation behaviour here is short of being correct return (cap.bounds.exp >= resetExp) ? ~0 : length; @@ -679,6 +679,9 @@ function SetBoundsReturn#(CapFat, CapAddrW) setBoundsFat(CapFat cap, Address len Bool resultInBounds = newBaseInBounds && newTopInBounds && !addressWrap; + // Nullify the capability if the result is not in bounds + if (!resultInBounds) ret.isCapability = False; + // Return derived capability return SetBoundsReturn { cap: ret , exact: exact @@ -1126,8 +1129,8 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3), Delta CapabilityInMemory cap = unpack (capMem); return pack (cap.address); endfunction - function fromMem = error ("fromMem not implemented for CapMem"); - function toMem = error ("toMem not implemented for CapMem"); + function fromMem(x) = unpack(pack(x)); + function toMem(x) = unpack(pack(x)); // capability address/offset manipulation ////////////////////////////////////////////////////////////////////////////// @@ -1528,7 +1531,11 @@ instance Cast#(function CapPipe f0(t y), function Bit#(CapAddrW) f1(t x)); endinstance `ifdef CAP64 -typedef 32 VA_Width; +// XXX TODO +// This is probably the wrong fix but allows the code to compile, and the +// code for CAP64 is not used anywhere. +// Need to consider what the right size is. +typedef 31 VA_Width; `else typedef 48 VA_Width; `endif diff --git a/CHERICap.bsv b/CHERICap.bsv index ebf98ae..7258e58 100644 --- a/CHERICap.bsv +++ b/CHERICap.bsv @@ -80,7 +80,7 @@ typedef union tagged { typedef struct { Bit #(addrW) base; Bit #(TAdd #(addrW, 1)) top; - Bit #(TAdd #(addrW, 1)) length; + Bit #(addrW) length; Bit #(addrW) repBase; Bit #(TAdd #(addrW, 1)) repTop; Bit #(TAdd #(addrW, 1)) repLength; @@ -259,7 +259,7 @@ typeclass CHERICap #( type capT // type of the CHERICap capability // Get the top function Bit #(TAdd #(addrW, 1)) getTop (capT cap) = getBoundsInfo(cap).top; // Get the length - function Bit #(TAdd #(addrW, 1)) getLength (capT cap) = + function Bit #(addrW) getLength (capT cap) = getBoundsInfo(cap).length; // Assertion that the capability's address is between its base and top function Bool isInBounds (capT cap, Bool isTopIncluded) = diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv index 839f2c7..fdda65d 100644 --- a/CHERICapProps.bsv +++ b/CHERICapProps.bsv @@ -204,4 +204,4 @@ function Bool prop_setBounds(CapAddr base, CapAddr len, CapAddr addr, CapAddr ne return forallCap(base, len, addr, prop); endfunction -endpackage \ No newline at end of file +endpackage diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv index 0c5402a..0ec9262 100644 --- a/CHERICapWrap.bsv +++ b/CHERICapWrap.bsv @@ -1,5 +1,5 @@ /* - * Copyright (c) 2019 Alexandre Joannou + * Copyright (c) 2019-2025 Alexandre Joannou * All rights reserved. * * This software was developed by SRI International and the University of @@ -30,7 +30,15 @@ package CHERICapWrap; import CHERICap :: *; import CHERICC_Fat :: *; +`ifndef CAPTYPE `define CAPTYPE CapPipe +`endif + +function CapPipe capArg(`CAPTYPE cap) = cast(cap); +function `CAPTYPE capRet(CapPipe cap) = cast(cap); +function Exact#(`CAPTYPE) capExactRet(Exact#(CapPipe) e_cap) = + Exact { exact: e_cap.exact, value: cast(e_cap.value) }; + `ifndef CAP64 `define W(name) wrap128_``name `else @@ -48,41 +56,45 @@ function `CAPTYPE `W(setFlags) (`CAPTYPE cap, Bit#(FlagsW) flags) = setFlags(cap (* noinline *) function HardPerms `W(getHardPerms) (`CAPTYPE cap) = getHardPerms(cap); (* noinline *) -function `CAPTYPE `W(setHardPerms) (`CAPTYPE cap, HardPerms hardperms) = setHardPerms(cap, hardperms); +function `CAPTYPE `W(setHardPerms) (`CAPTYPE cap, HardPerms hardperms) = capRet(setHardPerms(capArg(cap), hardperms)); (* noinline *) -function SoftPerms `W(getSoftPerms) (`CAPTYPE cap) = getSoftPerms(cap); +function SoftPerms `W(getSoftPerms) (`CAPTYPE cap) = getSoftPerms(capArg(cap)); (* noinline *) -function `CAPTYPE `W(setSoftPerms) (`CAPTYPE cap, SoftPerms softperms) = setSoftPerms(cap, softperms); +function `CAPTYPE `W(setSoftPerms) (`CAPTYPE cap, SoftPerms softperms) = capRet(setSoftPerms(capArg(cap), softperms)); (* noinline *) -function Bit#(31) `W(getPerms) (`CAPTYPE cap) = getPerms(cap); +function Bit#(31) `W(getPerms) (`CAPTYPE cap) = getPerms(capArg(cap)); (* noinline *) -function `CAPTYPE `W(setPerms) (`CAPTYPE cap, Bit#(31) perms) = setPerms(cap, perms); +function `CAPTYPE `W(setPerms) (`CAPTYPE cap, Bit#(31) perms) = capRet(setPerms(capArg(cap), perms)); (* noinline *) -function Kind#(OTypeW) `W(getKind) (`CAPTYPE cap) = getKind(cap); +function Kind#(OTypeW) `W(getKind) (`CAPTYPE cap) = getKind(capArg(cap)); (* noinline *) -function `CAPTYPE `W(setKind) (`CAPTYPE cap, Kind#(OTypeW) kind) = setKind(cap, kind); +function `CAPTYPE `W(setKind) (`CAPTYPE cap, Kind#(OTypeW) kind) = capRet(setKind(capArg(cap), kind)); (* noinline *) function Bit#(CapAddrW) `W(getAddr) (`CAPTYPE cap) = getAddr(cap); (* noinline *) -function Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = setAddr(cap, addr); +function `CAPTYPE `W(setAddrUnsafe) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capRet(setAddrUnsafe(capArg(cap), addr)); (* noinline *) -function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(cap); +function `CAPTYPE `W(addAddrUnsafe) (`CAPTYPE cap, Bit#(TSub #(MW, 3)) inc) = capRet(addAddrUnsafe(capArg(cap), inc)); (* noinline *) -function Exact#(`CAPTYPE) `W(modifyOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset, Bool doInc) = modifyOffset (cap, offset, doInc); +function Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capExactRet(setAddr(capArg(cap), addr)); (* noinline *) -function Exact#(`CAPTYPE) `W(setOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset) = setOffset (cap, offset); +function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(capArg(cap)); (* noinline *) -function Exact#(`CAPTYPE) `W(incOffset) (`CAPTYPE cap, Bit#(CapAddrW) inc) = incOffset (cap, inc); +function Exact#(`CAPTYPE) `W(modifyOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset, Bool doInc) = capExactRet(modifyOffset (capArg(cap), offset, doInc)); (* noinline *) -function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(cap); +function Exact#(`CAPTYPE) `W(setOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset) = capExactRet(setOffset (capArg(cap), offset)); (* noinline *) -function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(cap); +function Exact#(`CAPTYPE) `W(incOffset) (`CAPTYPE cap, Bit#(CapAddrW) inc) = capExactRet(incOffset (capArg(cap), inc)); (* noinline *) -function Bit#(TAdd#(CapAddrW, 1)) `W(getLength) (`CAPTYPE cap) = getLength(cap); +function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(capArg(cap)); (* noinline *) -function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(cap, isTopIncluded); +function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(capArg(cap)); (* noinline *) -function Exact#(`CAPTYPE) `W(setBounds) (`CAPTYPE cap, Bit#(CapAddrW) length) = setBounds(cap, length); +function Bit#(CapAddrW) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap)); +(* noinline *) +function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(capArg(cap), isTopIncluded); +(* noinline *) +function Exact#(`CAPTYPE) `W(setBounds) (`CAPTYPE cap, Bit#(CapAddrW) length) = capExactRet(setBounds(capArg(cap), length)); (* noinline *) function `CAPTYPE `W(nullWithAddr) (Bit#(CapAddrW) addr) = nullWithAddr(addr); (* noinline *) @@ -95,5 +107,15 @@ function Bool `W(validAsType) (`CAPTYPE dummy, Bit#(CapAddrW) checkType) = valid function `CAPTYPE `W(fromMem) (Tuple2#(Bool, Bit#(CapW)) mem_cap) = fromMem(mem_cap); (* noinline *) function Tuple2#(Bool, Bit#(CapW)) `W(toMem) (`CAPTYPE cap) = toMem(cap); +(* noinline *) +function Bit#(CapAddrW) `W(getRepresentableAlignmentMask) (`CAPTYPE dummy, Bit#(CapAddrW) length) = alignmentMask (capArg(dummy), length); +(* noinline *) +function Bit#(CapAddrW) `W(getRepresentableLength) (`CAPTYPE dummy, Bit#(CapAddrW) length) = roundLength (capArg(dummy), length); +(* noinline *) +function Bit#(2) `W(getBaseAlignment) (`CAPTYPE cap) = getBaseAlignment(capArg(cap)); +(* noinline *) +function Bool `W(isDerivable) (`CAPTYPE cap) = isDerivable(capArg(cap)); + + endpackage diff --git a/CHERICapWrap.py b/CHERICapWrap.py new file mode 100755 index 0000000..30659fb --- /dev/null +++ b/CHERICapWrap.py @@ -0,0 +1,261 @@ +#! /usr/bin/env python3 + +import argparse +import re +from abc import ABC, abstractmethod + +parser = argparse.ArgumentParser(description= + '''Generates a Blarney wrapper for the given Bluespec generated verilog file + containing a module definition of a purely combinational CHERI function. + ''') +parser.add_argument('verilog_files', metavar='VERILOG_FILE', type=str, nargs='+', + help='The file(s) to process') +parser.add_argument('--output', '-o', metavar='OUTPUT_FILE', type=str, nargs='?', + default="", + help='The output Blarney Haskell module to generate') +parser.add_argument('--generator', metavar='GENERATOR', type=str, nargs='?', + choices=['blarney','sv','systemverilog'], default='blarney', + help='The generator to be used') +args = parser.parse_args() + +# Generic wrapper for a Verilog module +class Wrapper: + def __init__(self, size, name, ins, out): + self.size = size + self.name = name + self.ins = ins + self.out = out + def verilogModuleName(self): + return "module_wrap{:d}_{:s}".format(self.size, self.name) + def verilogInputNames(self): + return ["wrap{:d}_{:s}_{:s}".format(self.size, self.name, nm) + for nm in [x[0] for x in self.ins]] + def verilogOutputName(self): + return "wrap{:d}_{:s}".format(self.size, self.name) + + +# Generic generator class +# Describes the minimum functionality that a generator needs to implement. +# A generator takes some list of Verilog modules (which includes information +# about the module name, inputs, outputs, etc) and generates a list of file +# contents that should be written. +class Generator(ABC): + # namehint is a hint for naming, and each specific generator subclass will + # interpret it in its own way. In many cases it may be the single generated + # filename + def __init__(self, namehint, mods = None): + self.namehint = namehint + if mods is not None: + self.modules = mods + else: + self.modules = list() + + def addVerilogModule(self, mod): + self.modules.append(mod) + + # Generates a list of tuples containing output file names and output file + # contents to be written to disk + @abstractmethod + def emit(self): + pass + +# Generates Blarney files +# When the namehint is not empty, it is used as the filename and .hs is appended +# otherwise the old default filename of CHERIBlarneyWrappers.hs is used +class BlarneyGenerator(Generator): + def emit(self): + modname = "CHERIBlarneyWrappers" + filename = modname + ".hs" + if self.namehint is not None and self.namehint != "": + modname = self.namehint + filename = self.namehint + ".hs" + + contents = "module " + modname + " where\n\n" + contents += "import Blarney\n" + contents += "import Blarney.Core.BV\n" + for mod in self.modules: + print(mod.name) + contents += "\n" + ins_names = [x[0] for x in mod.ins] + ins_wdths = [x[1] for x in mod.ins] + str_type = "{:s} :: {:s}{:s}{:s}".format( + mod.name, + " -> ".join(["Bit {:d}".format(n) for n in ins_wdths]), + " -> " if mod.ins else "", + "Bit {:d}".format(mod.out[1])) + str_decl = "{:s} {:s} = FromBV $\n makePrim1 (Custom \"{:s}\" [{:s}] [{:s}] [] False Nothing) [{:s}]".format( + mod.name, " ".join(ins_names), + mod.verilogModuleName(), + ", ".join(["(\"{:s}\", {:d})".format(n, w) + for (n, w) in zip(mod.verilogInputNames(), + ins_wdths)]), + "(\"{:s}\", {:d})".format(mod.verilogOutputName(), mod.out[1]), + ", ".join(["toBV {:s}".format(nm) for nm in ins_names])) + contents += "{:s}\n{:s}".format(str_type, str_decl) + contents += "\n".format(str_decl) + + + return [(filename, contents)] + +# generates SystemVerilog files +# when the namehint is non-empty it is used as a prefix for the file name +# generates a _pkg.sv file containing: +# a typedef of cheri_cap_t which is an "opaque" capability +# a typedef of cheri_cap_dec_t which is a decompressed capability +# generates a _mod.sv file containing a module which combinationally takes an "opaque" +# capability as the input and gives a decompressed capability as the output +# In the filename, "cheri" is appended with the in-memory capability width +# (i.e. the filename will be "cheri64_pkg.sv") so that differently sized capabilities +# can exist +class SystemVerilogGenerator(Generator): + def emit(self): + # get the size of in-memory capability by assuming that the name of the + # modules matches "module_wrap$SIZE_..." and taking just the size part + in_mem_cap_size = self.modules[0].verilogModuleName()[11:] + in_mem_cap_size = in_mem_cap_size[:in_mem_cap_size.find("_")] + + cap_type_name = "cheri_cap_t" # the name of the opaque cap type + cap_dec_type_name = "cheri_cap_dec_t" # the name of the expanded cap type + cap_dec_mod_name = "cheri{:s}_cap_expander".format(in_mem_cap_size) # the name of the expanding module + cap_in_signal_name = "cap_i" # the name of the input signal to the expanding module + cap_out_signal_name = "cap_o" # the name of the output signal to the expanding module + cap_search_string = "cap" # the string required for inferring capability width + + + # this wrapper generator is intended to make access to the "getter" + # modules (i.e. getAddr, getTop, etc) easier/cleaner + # ideally, to access the field it is cleaner to say "cap.address" rather than + # "cap.getAddress" or "cap.validCap" rather than "cap.isValidCap" + # the following is a list of "keywords" to remove from the field names + keywords_to_remove = ["get", "is"] + def mod_name_to_field_name(modname): + for kw in keywords_to_remove: + if modname.startswith(kw): + # remove the keyword from the start + modname = modname[len(kw):] + # make first letter lowercase + modname = modname[0].lower() + modname[1:] + # return after removing the first found keyword + return modname + return modname + + pkg_file_name = "cheri{:s}_pkg.sv".format(in_mem_cap_size) + module_file_name = "{:s}.sv".format(cap_dec_mod_name) + + # prepend namehint if non-empty + if self.namehint is not None and self.namehint != "": + pkg_file_name = self.namehint + "_" + pkg_file_name + module_file_name = self.namehint + "_" + module_file_name + + pkg_name = pkg_file_name[:-3] + dec_mod_name = module_file_name[:-3] + + # find the size of a capability by assuming that any no-input modules + # with "cap" in the name have a capability output + cap_size = None + for mod in self.modules: + if len(mod.ins) != 0 or cap_search_string not in mod.name.lower(): + continue + cap_size = mod.out[1] + break + + if cap_size == None: + # the above method failed to find a capability size + # to fix, can either implement a better method or just hard-code the capability size + raise NotImplementedError("Unable to determine capability size from input files") + + + cap_type_def_text = " typedef logic [{:d}:0] {:s};\n".format(cap_size-1, cap_type_name) + + # assume all modules with one capability-sized input are "getters" + # these will be the fields of the decompressed capability struct + struct_elems = list() + for mod in self.modules: + if len(mod.ins) == 1 and mod.ins[0][1] == cap_size: + struct_elems.append(mod) + + # structure definition + struct_def_text = " typedef struct packed {\n" + for mod in struct_elems: + struct_def_text += " logic [{:d}:{:d}] {:s};\n".format(mod.out[1]-1, 0, mod_name_to_field_name(mod.name)) + struct_def_text += " }} {:s};\n".format(cap_dec_type_name) + + # package definition + pkg_def_text = "package {:s};\n".format(pkg_name) + pkg_def_text += cap_type_def_text + pkg_def_text += struct_def_text + pkg_def_text += "endpackage\n" + + # module definition + module_def_text = "module {:s} (\n".format(cap_dec_mod_name) + module_def_text += " input {:s}::{:s} {:s},\n".format(pkg_name, cap_type_name, cap_in_signal_name) + module_def_text += " output {:s}::{:s} {:s}\n".format(pkg_name, cap_dec_type_name, cap_out_signal_name) + module_def_text += ");\n" + module_def_text += " import {:s}::*;\n".format(pkg_name) + + # module instantiations + for mod in struct_elems: + module_def_text += " {:s} {:s}_mod (\n".format(mod.verilogModuleName(), mod.name) + module_def_text += " .{:s}({:s}),\n".format(mod.verilogInputNames()[0], cap_in_signal_name) + module_def_text += " .{:s}({:s}.{:s})\n".format(mod.verilogOutputName(), cap_out_signal_name, mod_name_to_field_name(mod.name)) + module_def_text += " );\n" + + module_def_text += "endmodule\n" + + return [(pkg_file_name, pkg_def_text), + (module_file_name, module_def_text)] + +def main(): + # define module regexp + modDecl = re.compile("^module\s+module_wrap(\d+)_(\w+)\(") + # TODO handle size 1 + # + # gather the list of modules + wrappers = [] + for fname in args.verilog_files: + size = 0 + name = None + ins = [] + out = ("",0) + with open(fname, "r") as f: + for ln in f: + modM = modDecl.match(ln) + if modM: + size = int(modM.group(1)) + name = modM.group(2) + break + if not name: + print("Couldn't find a valid Verilog module definition") + exit(-1) + # define input/output regexp + inDecl = re.compile("^\s*input(\s+\[(\d+)\s+:\s+0\])?\s+wrap(\d+)_"+name+"_(\w+);") + outDecl = re.compile("^\s*output(\s+\[(\d+)\s+:\s+0\])?\s+wrap(\d+)_"+name+";") + + for ln in f: + inM = inDecl.match(ln) + outM = outDecl.match(ln) + if inM: + ins.append((inM.group(4), (int(inM.group(2)) + 1) if inM.group(1) else 1)) + elif outM: + out = (name, (int(outM.group(2)) + 1) if outM.group(1) else 1) + #else: + # print("===>> no match for line: {:s}".format(ln)) + wrappers.append(Wrapper(size, name, ins, out)) + + # choose the right generator based on the input argument + gen = None + if args.generator.lower() in ["systemverilog", "sv"]: + gen = SystemVerilogGenerator(args.output, wrappers) + elif args.generator.lower() in ["blarney"]: + gen = BlarneyGenerator(args.output, wrappers) + else: + print("Invalid generator selected; exiting") + return + + for out in gen.emit(): + with open(out[0], "w") as f: + f.write(out[1]) + + +if __name__ == "__main__": + main() diff --git a/CHERICapWrapBlarney.py b/CHERICapWrapBlarney.py deleted file mode 100755 index 43f5aa8..0000000 --- a/CHERICapWrapBlarney.py +++ /dev/null @@ -1,93 +0,0 @@ -#! /usr/bin/env python3 - -import argparse -import re - -parser = argparse.ArgumentParser(description= - '''Generates a Blarney wrapper for the given Bluespec generated verilog file - containing a module definition of a purely combinational CHERI function. - ''') -parser.add_argument('verilog_files', metavar='VERILOG_FILE', type=str, nargs='+', - help='The file(s) to process') -parser.add_argument('--output', '-o', metavar='OUTPUT_FILE', type=str, nargs='?', - default="CHERIBlarneyWrappers", - help='The output Blarney Haskell module to generate') -args = parser.parse_args() - -class BlarneyWrapper: - def __init__(self, size, name, ins, out): - self.size = size - self.name = name - self.ins = ins - self.out = out - def verilogModuleName(self): - return "module_wrap{:d}_{:s}".format(self.size, self.name) - def verilogInputNames(self): - return ["wrap{:d}_{:s}_{:s}".format(self.size, self.name, nm) - for nm in [x[0] for x in self.ins]] - def verilogOutputName(self): - return "wrap{:d}_{:s}".format(self.size, self.name) - def emitBlarney(self): - ins_names = [x[0] for x in self.ins] - ins_wdths = [x[1] for x in self.ins] - str_type = "{:s} :: {:s}{:s}{:s}".format( - self.name, - " -> ".join(["Bit {:d}".format(n) for n in ins_wdths]), - " -> " if self.ins else "", - "Bit {:d}".format(self.out[1])) - str_decl = "{:s} {:s} = FromBV $\n makePrim1 (Custom \"{:s}\" [{:s}] [{:s}] [] False Nothing) [{:s}]".format( - self.name, " ".join(ins_names), - self.verilogModuleName(), - ", ".join(["(\"{:s}\", {:d})".format(n, w) - for (n, w) in zip(self.verilogInputNames(), - ins_wdths)]), - "(\"{:s}\", {:d})".format(self.verilogOutputName(), self.out[1]), - ", ".join(["toBV {:s}".format(nm) for nm in ins_names])) - return "{:s}\n{:s}".format(str_type, str_decl) - -def main(): - # define module regexp - modDecl = re.compile("^module\s+module_wrap(\d+)_(\w+)\(") - # TODO handle size 1 - # - wrappers = [] - for fname in args.verilog_files: - size = 0 - name = None - ins = [] - out = ("",0) - with open(fname, "r") as f: - for ln in f: - modM = modDecl.match(ln) - if modM: - size = int(modM.group(1)) - name = modM.group(2) - break - if not name: - print("Couldn't find a valid Verilog module definition") - exit(-1) - # define input/output regexp - inDecl = re.compile("^\s*input(\s+\[(\d+)\s+:\s+0\])?\s+wrap(\d+)_"+name+"_(\w+);") - outDecl = re.compile("^\s*output(\s+\[(\d+)\s+:\s+0\])?\s+wrap(\d+)_"+name+";") - - for ln in f: - inM = inDecl.match(ln) - outM = outDecl.match(ln) - if inM: - ins.append((inM.group(4), (int(inM.group(2)) + 1) if inM.group(1) else 1)) - elif outM: - out = (name, (int(outM.group(2)) + 1) if outM.group(1) else 1) - #else: - # print("===>> no match for line: {:s}".format(ln)) - wrappers.append(BlarneyWrapper(size, name, ins, out)) - - with open(args.output+".hs", "w") as f: - #print("module CHERI{:d} where\n".format(size)) - f.write("module "+args.output+" where\n\n") - f.write("import Blarney\n") - f.write("import Blarney.Core.BV\n") - for w in wrappers: - f.write("\n{:s}\n".format(w.emitBlarney())) - -if __name__ == "__main__": - main() diff --git a/Makefile b/Makefile index 8b9af20..eda4a13 100644 --- a/Makefile +++ b/Makefile @@ -45,5 +45,5 @@ clean-counterexamples: clean: rm -rf $(BUILD_DIR) - -full-clean: clean clean-counterexamples \ No newline at end of file + +full-clean: clean clean-counterexamples diff --git a/assertions.sv b/assertions.sv index e0301c3..d538ec3 100644 --- a/assertions.sv +++ b/assertions.sv @@ -180,4 +180,3 @@ module assert_prop_setBounds( always @(*) begin assert(prop_ok); end -endmodule \ No newline at end of file diff --git a/check.sby b/check.sby index 54008e7..1362b2d 100644 --- a/check.sby +++ b/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 \ No newline at end of file diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..4b8e412 --- /dev/null +++ b/flake.lock @@ -0,0 +1,61 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1738579205, + "narHash": "sha256-o6BeeanSUALvz8oL2CHOikVjCf7j+HqlA0WGvKOUX3Q=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "be5cf18b3d26ba2db938a72ade93ac8a9a7462ff", + "type": "github" + }, + "original": { + "owner": "NixOS", + "ref": "release-24.11", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..c47f7bc --- /dev/null +++ b/flake.nix @@ -0,0 +1,25 @@ +{ + inputs = { + nixpkgs.url = "github:NixOS/nixpkgs/release-24.11"; + flake-utils.url = "github:numtide/flake-utils"; + }; + outputs = { self, nixpkgs, flake-utils }: + flake-utils.lib.eachDefaultSystem (system: + let # helper bindings + # imported nix packages + pkgs = import nixpkgs { inherit system; }; + # shell environment + dfltShell = pkgs.mkShell { + buildInputs = with pkgs; [ + sby + boolector + haskellPackages.sv2v + bluespec + ]; + }; + # output attribute set + in { + devShells.default = dfltShell; + } + ); +} diff --git a/fusesoc/cheri-cap-lib-test.core b/fusesoc/cheri-cap-lib-test.core new file mode 100644 index 0000000..48a03bd --- /dev/null +++ b/fusesoc/cheri-cap-lib-test.core @@ -0,0 +1,56 @@ +CAPI=2: +name: "ucam:cheri:cheri-cap-lib-test" +description: "Targets to test cheri-cap-lib generator" + +# different parameterizations of the generator, one is 64bit and the other is 128bit +generate: + cheri-cap-lib-64: + generator: cheri-cap-lib-gen + parameters: + capwidth : "CAP64" + + cheri-cap-lib-128: + generator: cheri-cap-lib-gen + parameters: + capwidth : "CAP128" + +# cores need to explicitly depend on the generator, so an empty fileset with +# a dependency on the generator's core is needed, like so: +filesets: + cheri-cap-lib-dep: + depend: + - ucam:cheri:cheri-cap-lib-verilog-generator + +# the filelist can then be placed in the filesets section of the dependant core +# to add the dependency, so that fusesoc can find the generator + +targets: + test64: + description: "Default target that generates 64bit versions" + default_tool: verilator + # this adds a dependency on the generator, so that it appears on the + # dependency tree + filesets: + - cheri-cap-lib-dep + # this invokes the 64bit parameterization of the generator which is + # declared above + generate: + - cheri-cap-lib-64 + test128: + description: "Default target that generates 128bit versions" + default_tool: verilator + filesets: + - cheri-cap-lib-dep + generate: + - cheri-cap-lib-128 + test: + description: "Default target that generates both 64bit and 128bit versions" + default_tool: verilator + filesets: + - cheri-cap-lib-dep + # this invokes both the 64bit and 128bit parameterizations of the generator + # which is declared above + generate: + - cheri-cap-lib-64 + - cheri-cap-lib-128 + diff --git a/fusesoc/cheri-cap-lib-verilog-generator.core b/fusesoc/cheri-cap-lib-verilog-generator.core new file mode 100644 index 0000000..f9c7d9b --- /dev/null +++ b/fusesoc/cheri-cap-lib-verilog-generator.core @@ -0,0 +1,15 @@ +CAPI=2: +name: "ucam:cheri:cheri-cap-lib-verilog-generator" +description: "Generates Verilog versions of the cheri-cap-lib functions" + +# the only parameter that this generator takes from the yaml file is +# capwidth, which will be defined as a macro during bluespec compilation +# the generated core file will have the name: +# "ucam:cheri:cheri-cap-lib-verilog-autogen-$WIDTH" +# where $WIDTH is the number after CAP in the capwidth parameter +generators: + cheri-cap-lib-gen: + interpreter: python3 + command: fusesoc-script.py + # TODO caching? for now, no + diff --git a/fusesoc/fusesoc-script.py b/fusesoc/fusesoc-script.py new file mode 100644 index 0000000..59a7522 --- /dev/null +++ b/fusesoc/fusesoc-script.py @@ -0,0 +1,124 @@ +import yaml +import subprocess +import argparse +import shutil +import os +import glob + +# get yaml file location from single argument +argparser = argparse.ArgumentParser() +argparser.add_argument('yaml_file') + +args = argparser.parse_args() + +# load yaml file +with open(args.yaml_file, "r") as yamlfile: + try: + print(yamlfile) + yamlcfg = yaml.safe_load(yamlfile) + except yaml.YAMLError as exc: + print(exc) + + +# TODO debug +print(yamlcfg) +print(yamlcfg['parameters']['capwidth']) + +# use capwidth if provided, or default to CAP64 +cfgwidth = yamlcfg["parameters"]["capwidth"] +capwidth = "CAP64" if cfgwidth in [None, ""] else cfgwidth + +# TODO debug +print("capwidth:") +print(capwidth) + +# get current working directory for file generation +workdir = os.getcwd() + +# location of source files is actually one level above the location of the core file +bsv_src_root = os.path.join(os.path.dirname(__file__), "..") +print("bsv_src_root") +print(bsv_src_root) + +# set up bluespec command + arguments +bscargs = list() +bscargs.extend(["bsc"]) +bscargs.extend(["-vdir", workdir]) +bscargs.extend(["-bdir", workdir]) +bscargs.extend(["-simdir", workdir]) +bscargs.extend(["-D", "{}".format(capwidth)]) +bscargs.extend(["-D", "RISCV"]) +bscargs.extend(["-verilog"]) +bscargs.extend(["-u"]) +bscargs.extend(["CHERICapWrap.bsv"]) +# TODO debug +print(bscargs) + +# blocking call to bsc to generate verilog files +subprocess.call(bscargs, cwd=bsv_src_root) + + + + +print("CCL AUTOGEN NAME:") +print("cheri-cap-lib-verilog-autogen-{}.core".format(capwidth[3:])) + + +# collect verilog files +vfiles = glob.glob(os.path.join(os.getcwd(), "*.v")) +print("verilog files:") +print(vfiles) + +# generate systemverilog files +subprocess.call(["python3", bsv_src_root + "/CHERICapWrap.py", "--generator", "sv"] + vfiles, cwd=workdir) + +# collect systemverilog files and package files +pkgfiles = glob.glob(os.path.join(os.getcwd(), "*_pkg.sv")) +svfiles = glob.glob(os.path.join(os.getcwd(), "*.sv")) +# +# remove package files from systemverilog files +for pkgfile in pkgfiles: + svfiles.remove(pkgfile) + +print("svfiles and pkgfiles:") +print(svfiles) +print(pkgfiles) + +# write core file +with open("cheri-cap-lib-verilog-autogen-{}.core".format(capwidth[3:]), 'w') as f: + txt = 'CAPI=2:\n' + txt += 'name: "ucam:cheri:cheri-cap-lib-verilog-autogen-{}"\n'.format(capwidth[3:]) + txt += 'description: "Autogenerated Verilog & SystemVerilog versions of the cheri-cap-lib functions"\n\n' + + txt += 'filesets:\n' + txt += ' files_pkg:\n' + txt += ' files:\n' + txt += ' - ' + txt += '\n - '.join([os.path.basename(file) for file in pkgfiles]) + txt += '\n' + txt += ' file_type: systemVerilogSource\n' + txt += ' files_v:\n' + txt += ' files:\n' + txt += ' - ' + txt += '\n - '.join([os.path.basename(file) for file in vfiles]) + txt += '\n' + txt += ' file_type: verilogSource\n' + txt += ' files_sv:\n' + txt += ' files:\n' + txt += ' - ' + txt += '\n - '.join([os.path.basename(file) for file in svfiles]) + txt += '\n' + txt += ' file_type: systemVerilogSource\n' + txt += '\n' + + txt += 'targets:\n' + txt += ' default:\n' + txt += ' description: "Default target that contains the Verilog files"\n' + txt += ' filesets:\n' + txt += ' - files_v\n' + txt += ' - files_pkg\n' + txt += ' - files_sv\n' + + f.write(txt) + + diff --git a/readme.adoc b/readme.adoc index 5dcd9be..3f2faa1 100644 --- a/readme.adoc +++ b/readme.adoc @@ -48,3 +48,41 @@ toc::[] == The CHERI CAP LIB API include::CHERI_CAP_API.adoc[] + +== FuseSoC + +``cheri-cap-lib`` supports being used as a generator within FuseSoC. The scripts +and cores for this are within the ``fusesoc`` directory, and the file +``cheri-cap-lib-test.core`` shows how a core can declare a dependency on and +use the ``cheri-cap-lib`` generator. + +The FuseSoC generator will generate Verilog modules for each of the functions +in ``CHERICapWrap.bsv``, as well as a SystemVerilog package and module to +make working with these modules _slightly_ simpler in SystemVerilog. + +To generate both the 64bit and 128bit wrappers and packages, run +``fusesoc --cores-root . run --target test --setup ucam:cheri:cheri-cap-lib-test`` + +The files will be generated in +``build/ucam_cheri_cheri-cap-lib-test_0/src/ucam_cheri_cheri-cap-lib-verilog-autogen-64_0/`` +and +``build/ucam_cheri_cheri-cap-lib-test_0/src/ucam_cheri_cheri-cap-lib-verilog-autogen-128_0/`` + +These fusesoc cores and instructions work using fusesoc 0.3 as installed +by running +``pip3 install -r python-requirements.txt`` +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 +```