merge conflict resovled

.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

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 fromMem(x) = unpack(pack(x));
-  function toMem = error ("toMem not implemented for CapMem");
+  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

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) =

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
+endpackage

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

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()

CHERICapWrapBlarney.py

@@ -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()

Makefile

@@ -45,5 +45,5 @@ clean-counterexamples:
 
 clean:
 	rm -rf $(BUILD_DIR)
-
+	
-full-clean: clean clean-counterexamples
+full-clean: clean clean-counterexamples

assertions.sv

@@ -180,4 +180,3 @@ module assert_prop_setBounds(
   always @(*) begin
     assert(prop_ok);
   end
-endmodule

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

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
+}

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;
+      }
+    );
+}

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
+

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
+

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)
+
+

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
+```