From 49de0f90f0d71c27c45a022e2296a51c5c1afb08 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Mon, 2 Oct 2023 17:29:40 +0100
Subject: [PATCH 01/32] Reduce VA_Width to allow compilation

This is almost certainly not the right fix but allows the code to
compile and the trim code is not used anywhere with CAP64
---
 CHERICC_Fat.bsv | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index 2527c84..451ce38 100644
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -1500,7 +1500,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

From 2d6864bbf30c0da49f51147bf42d2fc686d662c2 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Fri, 13 Jan 2023 16:07:31 +0000
Subject: [PATCH 02/32] New wrap script to support more languages (inc SV)

At the moment, the original Blarney support is kept and support for a
SystemVerilog wrapper is added.
---
 CHERICapWrap.py        | 235 +++++++++++++++++++++++++++++++++++++++++
 CHERICapWrapBlarney.py |  93 ----------------
 2 files changed, 235 insertions(+), 93 deletions(-)
 create mode 100755 CHERICapWrap.py
 delete mode 100755 CHERICapWrapBlarney.py

diff --git a/CHERICapWrap.py b/CHERICapWrap.py
new file mode 100755
index 0000000..a220a97
--- /dev/null
+++ b/CHERICapWrap.py
@@ -0,0 +1,235 @@
+#! /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="",
+                    help='The output Blarney Haskell module to generate')
+parser.add_argument('--generator', metavar='GENERATOR', type=str, nargs='?',
+                    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)
+  def emit(self):
+    raise NotImplementedError("Please Implement this method")
+
+
+# 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:
+  # 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
+  def emit(self):
+    raise NotImplementedError("Method not implemented in subclass")
+
+# 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
+class SystemVerilogGenerator(Generator):
+  def emit(self):
+    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_cap_expander" # 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
+
+    pkg_file_name = "cheri_pkg.sv"
+    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)
+    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)
+      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()

From a6664e512cc6368beae22506e4abb6c067791616 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Wed, 18 Jan 2023 18:04:52 +0000
Subject: [PATCH 03/32] Implement changes suggested by @gameboo + bugfix

Uses argparse's "choices" argument, remove unused method and use abc and
for abstract methods.
Also updates the python filename in the Makefile
---
 CHERICapWrap.py | 10 +++++-----
 Makefile        |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/CHERICapWrap.py b/CHERICapWrap.py
index a220a97..d59b52e 100755
--- a/CHERICapWrap.py
+++ b/CHERICapWrap.py
@@ -2,6 +2,7 @@
 
 import argparse
 import re
+from abc import ABC, abstractmethod
 
 parser = argparse.ArgumentParser(description=
   '''Generates a Blarney wrapper for the given Bluespec generated verilog file
@@ -13,7 +14,7 @@ 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='?',
-                    default='Blarney',
+                    choices=['blarney','sv','systemverilog'], default='blarney',
                     help='The generator to be used')
 args = parser.parse_args()
 
@@ -31,8 +32,6 @@ class Wrapper:
                 for nm in [x[0] for x in self.ins]]
   def verilogOutputName(self):
     return "wrap{:d}_{:s}".format(self.size, self.name)
-  def emit(self):
-    raise NotImplementedError("Please Implement this method")
 
 
 # Generic generator class
@@ -40,7 +39,7 @@ class Wrapper:
 # 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:
+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
@@ -56,8 +55,9 @@ class Generator:
 
   # Generates a list of tuples containing output file names and output file
   # contents to be written to disk
+  @abstractmethod
   def emit(self):
-    raise NotImplementedError("Method not implemented in subclass")
+    pass
 
 # Generates Blarney files
 # When the namehint is not empty, it is used as the filename and .hs is appended
diff --git a/Makefile b/Makefile
index 10591f2..d6d327a 100644
--- a/Makefile
+++ b/Makefile
@@ -15,8 +15,8 @@ all: verilog-wrappers blarney-wrappers
 verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
 	bsc $(BSCFLAGS) -verilog -u $<
 
-blarney-wrappers: CHERICapWrapBlarney.py verilog-wrappers
-	./CHERICapWrapBlarney.py -o CHERIBlarneyWrappers *.v
+blarney-wrappers: CHERICapWrap.py verilog-wrappers
+	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
 
 .PHONY: clean clean-verilog-wrappers
 

From fcadf1aead7dbed08673c2b60ea2d8ddd405a7d8 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Sat, 30 Sep 2023 16:52:15 +0100
Subject: [PATCH 04/32] Add barebones fusesoc generator core

This adds a fusesoc generator to create the verilog files from the
bluespec source.
---
 fusesoc/cheri-cap-lib-verilog-generator.core | 15 ++++
 fusesoc/fusesoc-script.py                    | 92 ++++++++++++++++++++
 2 files changed, 107 insertions(+)
 create mode 100644 fusesoc/cheri-cap-lib-verilog-generator.core
 create mode 100644 fusesoc/fusesoc-script.py

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..72b80fa
--- /dev/null
+++ b/fusesoc/fusesoc-script.py
@@ -0,0 +1,92 @@
+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 = yamlcfg["files_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)
+
+# 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_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 += '\n'
+
+  txt += 'targets:\n'
+  txt += '  default:\n'
+  txt += '    description: "Default target that contains the Verilog files"\n'
+  txt += '    filesets:\n'
+  txt += '      - files_v\n'
+
+  f.write(txt)
+

From 61e7b3e668bf5f0c82466d0d4e10151b872d10bc Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Sat, 30 Sep 2023 17:09:56 +0100
Subject: [PATCH 05/32] Add test core and targets

To test, run:
fusesoc --cores-root . run --setup --target test ucam:cheri:cheri-cap-lib-test
---
 fusesoc/cheri-cap-lib-test.core | 50 +++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 fusesoc/cheri-cap-lib-test.core

diff --git a/fusesoc/cheri-cap-lib-test.core b/fusesoc/cheri-cap-lib-test.core
new file mode 100644
index 0000000..ffadd87
--- /dev/null
+++ b/fusesoc/cheri-cap-lib-test.core
@@ -0,0 +1,50 @@
+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
+    filesets:
+      - cheri-cap-lib-dep
+    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
+    generate:
+      - cheri-cap-lib-64
+      - cheri-cap-lib-128
+

From fd1f7c12a297c0f50f4533578b1261c3de05eb6c Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Sat, 30 Sep 2023 18:01:28 +0100
Subject: [PATCH 06/32] Add SystemVerilog wrappers to generator

---
 fusesoc/fusesoc-script.py | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/fusesoc/fusesoc-script.py b/fusesoc/fusesoc-script.py
index 72b80fa..a3b066a 100644
--- a/fusesoc/fusesoc-script.py
+++ b/fusesoc/fusesoc-script.py
@@ -67,6 +67,21 @@ 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'
@@ -74,12 +89,24 @@ with open("cheri-cap-lib-verilog-autogen-{}.core".format(capwidth[3:]), 'w') as
   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'
@@ -87,6 +114,9 @@ with open("cheri-cap-lib-verilog-autogen-{}.core".format(capwidth[3:]), 'w') as
   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)
 
+

From 06eff948d9461082ed7bba385d335b05c8e1a220 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Sat, 30 Sep 2023 18:24:52 +0100
Subject: [PATCH 07/32] Fix bsv_src_root

files_root is actually the directory where the fusesoc command was
executed, but what we want here is the location of the python file being
executed so we can find the bluespec sources
---
 fusesoc/fusesoc-script.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/fusesoc/fusesoc-script.py b/fusesoc/fusesoc-script.py
index a3b066a..59a7522 100644
--- a/fusesoc/fusesoc-script.py
+++ b/fusesoc/fusesoc-script.py
@@ -36,7 +36,9 @@ print(capwidth)
 workdir = os.getcwd()
 
 # location of source files is actually one level above the location of the core file
-bsv_src_root = yamlcfg["files_root"] + "/.."
+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()

From a8898154d4661803db0c8a6eafc85ab734d4d5d5 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Sat, 30 Sep 2023 18:27:35 +0100
Subject: [PATCH 08/32] Add functions to CHERICapWrap.bsv

---
 CHERICapWrap.bsv | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv
index 0c5402a..53b297b 100644
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -95,5 +95,11 @@ 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 (dummy, length);
+(* noinline *)
+function Bit#(CapAddrW) `W(getRepresentableLength) (`CAPTYPE dummy, Bit#(CapAddrW) length) = roundLength (dummy, length);
+(* noinline *)
+function Bit#(2) `W(getBaseAlignment) (`CAPTYPE cap) = getBaseAlignment(cap);
 
 endpackage

From ed0e4dfa65bdbeaef7526bfe18966f2ab565a930 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Mon, 2 Oct 2023 17:25:31 +0100
Subject: [PATCH 09/32] Add capability size to name of modules and files

---
 CHERICapWrap.py | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/CHERICapWrap.py b/CHERICapWrap.py
index d59b52e..5ce9dfc 100755
--- a/CHERICapWrap.py
+++ b/CHERICapWrap.py
@@ -104,16 +104,24 @@ class BlarneyGenerator(Generator):
 #   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):
-    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_cap_expander" # 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
+    # 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("_")]
 
-    pkg_file_name = "cheri_pkg.sv"
+    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
+
+    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

From e4e1ed4c69831e51a2fe3ec460460687abaaf29a Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Mon, 2 Oct 2023 18:03:06 +0100
Subject: [PATCH 10/32] Add some documentation regarding FuseSoC

---
 fusesoc/cheri-cap-lib-test.core |  6 ++++++
 readme.adoc                     | 19 +++++++++++++++++++
 2 files changed, 25 insertions(+)

diff --git a/fusesoc/cheri-cap-lib-test.core b/fusesoc/cheri-cap-lib-test.core
index ffadd87..48a03bd 100644
--- a/fusesoc/cheri-cap-lib-test.core
+++ b/fusesoc/cheri-cap-lib-test.core
@@ -28,8 +28,12 @@ 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:
@@ -44,6 +48,8 @@ targets:
     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/readme.adoc b/readme.adoc
index 5dcd9be..d803cef 100644
--- a/readme.adoc
+++ b/readme.adoc
@@ -48,3 +48,22 @@ 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/test-verilator/generated/ucam_cheri_cheri-cap-lib-test-cheri-cap-lib-64_0/``
+and
+``build/ucam_cheri_cheri-cap-lib-test_0/test-verilator/generated/ucam_cheri_cheri-cap-lib-test-cheri-cap-lib-128_0/``

From f3284354d2d4ec9457ad66c18e2e07dc1acb590e Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Wed, 4 Oct 2023 19:58:48 +0100
Subject: [PATCH 11/32] Remove "is" and "get" from generated SV fields

This should make using the fields a little prettier
---
 CHERICapWrap.py | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/CHERICapWrap.py b/CHERICapWrap.py
index 5ce9dfc..30659fb 100755
--- a/CHERICapWrap.py
+++ b/CHERICapWrap.py
@@ -121,6 +121,24 @@ class SystemVerilogGenerator(Generator):
     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)
 
@@ -159,7 +177,7 @@ class SystemVerilogGenerator(Generator):
     # 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)
+      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
@@ -179,7 +197,7 @@ class SystemVerilogGenerator(Generator):
     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)
+      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"

From 321c985fc8ad852c8557f81134886937cd4bdc05 Mon Sep 17 00:00:00 2001
From: Ivan Ribeiro <ivanmgribeiro@gmail.com>
Date: Sun, 8 Oct 2023 14:06:04 +0100
Subject: [PATCH 12/32] Update fusesoc docs per version of OT repo used

The previous documentation was using the python requirements from the
ibex repository rather than the OpenTitan repo.
---
 readme.adoc | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/readme.adoc b/readme.adoc
index d803cef..2980af3 100644
--- a/readme.adoc
+++ b/readme.adoc
@@ -64,6 +64,14 @@ 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/test-verilator/generated/ucam_cheri_cheri-cap-lib-test-cheri-cap-lib-64_0/``
+``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/test-verilator/generated/ucam_cheri_cheri-cap-lib-test-cheri-cap-lib-128_0/``
+``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
+
+

From 7d229ec7d50ef500b8087e11e8902d2bf07be640 Mon Sep 17 00:00:00 2001
From: Yuecheng Wang <yw737@cl.cam.ac.uk>
Date: Mon, 2 Sep 2024 13:42:51 +0100
Subject: [PATCH 13/32] added isDerivable to verilog wrapper

---
 CHERICapWrap.bsv | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv
index 53b297b..6714a76 100644
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -101,5 +101,9 @@ function Bit#(CapAddrW) `W(getRepresentableAlignmentMask) (`CAPTYPE dummy, Bit#(
 function Bit#(CapAddrW) `W(getRepresentableLength) (`CAPTYPE dummy, Bit#(CapAddrW) length) = roundLength (dummy, length);
 (* noinline *)
 function Bit#(2) `W(getBaseAlignment) (`CAPTYPE cap) = getBaseAlignment(cap);
+(* noinline *) 
+function Bool `W(isDerivable) (`CAPTYPE cap) = isDerivable(cap);
+
+
 
 endpackage

From 354a67386ed26a357f3f8f48dfb6d760887f17c1 Mon Sep 17 00:00:00 2001
From: Marvel Renju <marvelrenju1@gmail.com>
Date: Mon, 9 Sep 2024 12:45:12 +0100
Subject: [PATCH 14/32] Fix setBounds not clearing tag (#12)

Ensure tag is cleared if the result is not in bounds
---
 CHERICC_Fat.bsv | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index 451ce38..ed6b2e4 100644
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -668,6 +668,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

From b29845fd65288947ac9d3d8f948ebf227807dbe2 Mon Sep 17 00:00:00 2001
From: PeterRugg <pdr32@cam.ac.uk>
Date: Fri, 10 Jan 2025 16:58:15 +0000
Subject: [PATCH 15/32] Fix readme python-requirements typo

Spotted by @jonwoodruff
---
 readme.adoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/readme.adoc b/readme.adoc
index 2980af3..5f64d2a 100644
--- a/readme.adoc
+++ b/readme.adoc
@@ -70,7 +70,7 @@ and
 
 These fusesoc cores and instructions work using fusesoc 0.3 as installed
 by running
-``pip3 install -r python_requirements.txt``
+``pip3 install -r python-requirements.txt``
 within the OpenTitan GitHub repository as of commit
 https://github.com/lowRISC/opentitan/commit/2438b17afe4fef0d815be2e890763c288c449918
 

From d9e2fb788a64c68dfea3f1121ff8d9dd1d551ed9 Mon Sep 17 00:00:00 2001
From: Matthew Naylor <mn416@cam.ac.uk>
Date: Wed, 17 Jul 2024 10:01:27 +0100
Subject: [PATCH 16/32] Some properties that pass through SymbiYosys

---
 CHERICC_Fat.bsv   |   2 +
 CHERICapProps.bsv | 180 ++++++++++++++++++++++++++++++++++++++++++++++
 Makefile          |   3 +
 assertions.sv     | 147 +++++++++++++++++++++++++++++++++++++
 check.sby         |  46 ++++++++++++
 readme.adoc       |  11 +++
 6 files changed, 389 insertions(+)
 create mode 100644 CHERICapProps.bsv
 create mode 100644 assertions.sv
 create mode 100644 check.sby

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

From c2fe9cc0936da09313299d6546c1730df5ae03ab Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jdw57@cam.ac.uk>
Date: Fri, 24 Jan 2025 15:20:14 +0000
Subject: [PATCH 17/32] Add rule in makefile to perform the formal property
 checks.

---
 Makefile | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 635c7bc..25f1985 100644
--- a/Makefile
+++ b/Makefile
@@ -18,6 +18,9 @@ verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
 verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
 	bsc $(BSCFLAGS) -verilog -u $<
 
+check-prop: assertions.sv verilog-wrappers verilog-props
+	sby -f check.sby
+
 blarney-wrappers: CHERICapWrap.py verilog-wrappers
 	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
 
@@ -30,4 +33,4 @@ clean-blarney-wrappers: clean
 	rm -f *.hs
 
 clean:
-	rm -f *.bo
+	rm -f *.bo
\ No newline at end of file

From 7212f50b4d2476e0ace31a15ef07bd1a811c8ad9 Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jdw57@cam.ac.uk>
Date: Fri, 24 Jan 2025 17:23:49 +0000
Subject: [PATCH 18/32] Take into account tag clearing in setBounds.

---
 CHERICapProps.bsv | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index ad89ec4..05bd946 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -91,6 +91,7 @@ function Bool prop_unique(CapAddr base, CapAddr len,
   return baseCap.exact && expectedBaseCap.exact && implies
     ( boundedCap.exact && newBaseCap.exact &&
       finalCap.exact && expectedCap.exact &&
+      isValidCap(finalCap.value) &&
       newBase >= base && {1'b0, newBase} + {1'b0, newLen} <=
                          {1'b0, base}    + {1'b0, len}
     , toMem(expectedCap.value) == toMem(finalCap.value)

From 19d3983010eaef1c850d22b136e3a132ef75cfab Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Mon, 27 Jan 2025 12:13:19 +0000
Subject: [PATCH 19/32] Added an option to control the capability type used for
 verilog wrappers

---
 CHERICapWrap.bsv | 5 ++++-
 Makefile         | 5 ++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv
index 6714a76..c884fa8 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,10 @@ package CHERICapWrap;
 import CHERICap :: *;
 import CHERICC_Fat :: *;
 
+`ifndef CAPTYPE
 `define CAPTYPE CapPipe
+`endif
+
 `ifndef CAP64
 `define W(name) wrap128_``name
 `else
diff --git a/Makefile b/Makefile
index 25f1985..c0ae5b4 100644
--- a/Makefile
+++ b/Makefile
@@ -5,6 +5,9 @@ else
 BSCFLAGS = -D CAP64
 endif
 
+CAPTYPE ?= CapPipe
+BSCFLAGS += -D CAPTYPE=$(CAPTYPE)
+
 ARCH ?= RISCV
 ifeq ($(ARCH), RISCV)
 BSCFLAGS += -D RISCV
@@ -33,4 +36,4 @@ clean-blarney-wrappers: clean
 	rm -f *.hs
 
 clean:
-	rm -f *.bo
\ No newline at end of file
+	rm -f *.bo

From 0ca39912ba957758a5d04d308441f7f894acbe8d Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Mon, 27 Jan 2025 14:42:41 +0000
Subject: [PATCH 20/32] Let CapWrap build with CapMem and CapReg as well as
 CapPipe

---
 CHERICC_Fat.bsv  |  6 +++---
 CHERICapWrap.bsv | 49 ++++++++++++++++++++++++++----------------------
 2 files changed, 30 insertions(+), 25 deletions(-)

diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index b48bf47..c9beb70 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.
@@ -1112,8 +1112,8 @@ instance CHERICap #(CapMem, OTypeW, FlagsW, CapAddrW, CapW, TSub #(MW, 3));
     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
   //////////////////////////////////////////////////////////////////////////////
diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv
index c884fa8..7d62169 100644
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -34,6 +34,11 @@ import CHERICC_Fat :: *;
 `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
@@ -51,41 +56,41 @@ 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 Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capExactRet(setAddr(capArg(cap), addr));
 (* noinline *)
-function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(cap);
+function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(capArg(cap));
 (* noinline *)
-function Exact#(`CAPTYPE) `W(modifyOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset, Bool doInc) = modifyOffset (cap, offset, doInc);
+function Exact#(`CAPTYPE) `W(modifyOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset, Bool doInc) = capExactRet(modifyOffset (capArg(cap), offset, doInc));
 (* noinline *)
-function Exact#(`CAPTYPE) `W(setOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset) = setOffset (cap, offset);
+function Exact#(`CAPTYPE) `W(setOffset) (`CAPTYPE cap, Bit#(CapAddrW) offset) = capExactRet(setOffset (capArg(cap), offset));
 (* noinline *)
-function Exact#(`CAPTYPE) `W(incOffset) (`CAPTYPE cap, Bit#(CapAddrW) inc) = incOffset (cap, inc);
+function Exact#(`CAPTYPE) `W(incOffset) (`CAPTYPE cap, Bit#(CapAddrW) inc) = capExactRet(incOffset (capArg(cap), inc));
 (* noinline *)
-function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(cap);
+function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(capArg(cap));
 (* noinline *)
-function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(cap);
+function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(capArg(cap));
 (* noinline *)
-function Bit#(TAdd#(CapAddrW, 1)) `W(getLength) (`CAPTYPE cap) = getLength(cap);
+function Bit#(TAdd#(CapAddrW, 1)) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
 (* noinline *)
-function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(cap, isTopIncluded);
+function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(capArg(cap), isTopIncluded);
 (* noinline *)
-function Exact#(`CAPTYPE) `W(setBounds) (`CAPTYPE cap, Bit#(CapAddrW) length) = setBounds(cap, length);
+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 *)
@@ -99,13 +104,13 @@ function `CAPTYPE `W(fromMem) (Tuple2#(Bool, Bit#(CapW)) mem_cap) = fromMem(mem_
 (* noinline *)
 function Tuple2#(Bool, Bit#(CapW)) `W(toMem) (`CAPTYPE cap) = toMem(cap);
 (* noinline *)
-function Bit#(CapAddrW) `W(getRepresentableAlignmentMask) (`CAPTYPE dummy, Bit#(CapAddrW) length) = alignmentMask (dummy, length);
+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 (dummy, length);
+function Bit#(CapAddrW) `W(getRepresentableLength) (`CAPTYPE dummy, Bit#(CapAddrW) length) = roundLength (capArg(dummy), length);
 (* noinline *)
-function Bit#(2) `W(getBaseAlignment) (`CAPTYPE cap) = getBaseAlignment(cap);
-(* noinline *) 
-function Bool `W(isDerivable) (`CAPTYPE cap) = isDerivable(cap);
+function Bit#(2) `W(getBaseAlignment) (`CAPTYPE cap) = getBaseAlignment(capArg(cap));
+(* noinline *)
+function Bool `W(isDerivable) (`CAPTYPE cap) = isDerivable(capArg(cap));
 
 
 

From eb6f9ebade7ec43cbafaf90051a932a9062bc676 Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Mon, 27 Jan 2025 19:45:55 +0000
Subject: [PATCH 21/32] Added setAddrUnsafe to generated verilog wrappers

---
 CHERICapWrap.bsv | 2 ++
 flake.lock       | 0
 2 files changed, 2 insertions(+)
 create mode 100644 flake.lock

diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv
index 7d62169..dba46b5 100644
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -72,6 +72,8 @@ function `CAPTYPE `W(setKind) (`CAPTYPE cap, Kind#(OTypeW) kind) = capRet(setKin
 (* noinline *)
 function Bit#(CapAddrW) `W(getAddr) (`CAPTYPE cap) = getAddr(cap);
 (* noinline *)
+function `CAPTYPE `W(setAddrUnsafe) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capRet(setAddrUnsafe(capArg(cap), addr));
+(* noinline *)
 function Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capExactRet(setAddr(capArg(cap), addr));
 (* noinline *)
 function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(capArg(cap));
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..e69de29

From 033135b5f69ddff5f056e657ed26cfffed5815a2 Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jonwoodruff@gmail.com>
Date: Fri, 31 Jan 2025 11:05:08 +0000
Subject: [PATCH 22/32] Add a new property that encoding and decoding a memory
 capability gives the same result.  This caught the most recent bug.

---
 CHERICapProps.bsv |  7 +++++++
 assertions.sv     | 15 +++++++++++++++
 check.sby         |  4 ++++
 3 files changed, 26 insertions(+)

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

From 9e0636e6fc516d385d6f83c52006139594b1c21e Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Mon, 3 Feb 2025 15:23:58 +0000
Subject: [PATCH 23/32] Added test workflow

---
 .github/workflows/check-prop.yml | 16 +++++++++
 flake.lock                       | 61 ++++++++++++++++++++++++++++++++
 flake.nix                        | 25 +++++++++++++
 3 files changed, 102 insertions(+)
 create mode 100644 .github/workflows/check-prop.yml
 create mode 100644 flake.nix

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/flake.lock b/flake.lock
index e69de29..4b8e412 100644
--- a/flake.lock
+++ 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;
+      }
+    );
+}

From 3926b793bf187ecd20bf6d542d43dd074ae7c051 Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Tue, 4 Feb 2025 12:22:21 +0000
Subject: [PATCH 24/32] Added an env var to control bsc vdir flag

---
 Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index c0ae5b4..a98e422 100644
--- a/Makefile
+++ b/Makefile
@@ -13,6 +13,9 @@ ifeq ($(ARCH), RISCV)
 BSCFLAGS += -D RISCV
 endif
 
+BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)
+BSCFLAGS += -vdir $(BSV_VERILOG_WRAPPERS_DIR)
+
 all: verilog-wrappers blarney-wrappers
 
 verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv

From b3896e4e508a4b898446fa83b9e7b6d9696e0907 Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jonathan.woodruff@capabilitieslimited.co.uk>
Date: Tue, 4 Feb 2025 16:31:01 +0000
Subject: [PATCH 25/32] Move getLength to address length (not address length +
 1), as we're explicitly saturating in order to express as a normal address.

---
 CHERICC_Fat.bsv  | 6 +++---
 CHERICap.bsv     | 4 ++--
 CHERICapWrap.bsv | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHERICC_Fat.bsv b/CHERICC_Fat.bsv
index c9beb70..b6a2bcf 100644
--- a/CHERICC_Fat.bsv
+++ b/CHERICC_Fat.bsv
@@ -346,7 +346,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
@@ -437,12 +437,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;
diff --git a/CHERICap.bsv b/CHERICap.bsv
index 2f6d5a4..ff0d7a2 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;
@@ -258,7 +258,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/CHERICapWrap.bsv b/CHERICapWrap.bsv
index dba46b5..260c4bb 100644
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -88,7 +88,7 @@ function Bit#(CapAddrW) `W(getBase) (`CAPTYPE cap) = getBase(capArg(cap));
 (* noinline *)
 function Bit#(TAdd#(CapAddrW, 1)) `W(getTop) (`CAPTYPE cap) = getTop(capArg(cap));
 (* noinline *)
-function Bit#(TAdd#(CapAddrW, 1)) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
+function Bit#(CapAddrW) `W(getLength) (`CAPTYPE cap) = getLength(capArg(cap));
 (* noinline *)
 function Bool `W(isInBounds) (`CAPTYPE cap, Bool isTopIncluded) = isInBounds(capArg(cap), isTopIncluded);
 (* noinline *)

From 2295c3b8c0e997f95d56167d42eddad7aa706266 Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Wed, 5 Feb 2025 12:28:19 +0000
Subject: [PATCH 26/32] Added addAddrUnsafe verilog wrapper

---
 CHERICapWrap.bsv | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHERICapWrap.bsv b/CHERICapWrap.bsv
index 260c4bb..0ec9262 100644
--- a/CHERICapWrap.bsv
+++ b/CHERICapWrap.bsv
@@ -74,6 +74,8 @@ function Bit#(CapAddrW) `W(getAddr) (`CAPTYPE cap) = getAddr(cap);
 (* noinline *)
 function `CAPTYPE `W(setAddrUnsafe) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capRet(setAddrUnsafe(capArg(cap), addr));
 (* noinline *)
+function `CAPTYPE `W(addAddrUnsafe) (`CAPTYPE cap, Bit#(TSub #(MW, 3)) inc) = capRet(addAddrUnsafe(capArg(cap), inc));
+(* noinline *)
 function Exact#(`CAPTYPE) `W(setAddr) (`CAPTYPE cap, Bit#(CapAddrW) addr) = capExactRet(setAddr(capArg(cap), addr));
 (* noinline *)
 function Bit#(CapAddrW) `W(getOffset) (`CAPTYPE cap) = getOffset(capArg(cap));

From 595447fd62432faa80d4a6533897ea4d229198dd Mon Sep 17 00:00:00 2001
From: Alexandre Joannou <alexandre.joannou@cl.cam.ac.uk>
Date: Mon, 10 Feb 2025 17:44:09 +0000
Subject: [PATCH 27/32] fix property following getLength return type change in
 b3896e4e508a4b898446fa83b9e7b6d9696e0907

---
 CHERICapProps.bsv | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index ea0a314..fd8ffb2 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -52,7 +52,7 @@ function Bool forallBaseAndLen(CapAddr base, CapAddr len,
   Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
   Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
   return baseCap.exact && implies
-    ( boundedCap.exact 
+    ( boundedCap.exact
     , prop(boundedCap.value)
     );
 endfunction
@@ -107,10 +107,10 @@ 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));
+  CapAddr length = getLength(boundedCap.value);
+  Exact#(CapPipe) boundedCap2 = setBounds(baseCap2.value, length);
   return baseCap.exact && baseCap2.exact && implies
-           ( truncateLSB(length) == 1'b0
+           ( ~length != 0
            , boundedCap2.exact
            );
 endfunction

From c5da2ebc5d6fe2fd239736df942e3e6a4ba983f7 Mon Sep 17 00:00:00 2001
From: Peter Rugg <pdr32@cam.ac.uk>
Date: Tue, 4 Mar 2025 14:03:15 +0000
Subject: [PATCH 28/32] Move to building untracked files in subdirectories to
 improve cleaning

---
 .gitignore |  2 ++
 Makefile   | 39 +++++++++++++++++++++++----------------
 check.sby  | 18 +++++++++---------
 3 files changed, 34 insertions(+), 25 deletions(-)
 create mode 100644 .gitignore

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..10a199a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+build/
+counterexamples/
diff --git a/Makefile b/Makefile
index a98e422..ac2af28 100644
--- a/Makefile
+++ b/Makefile
@@ -13,30 +13,37 @@ ifeq ($(ARCH), RISCV)
 BSCFLAGS += -D RISCV
 endif
 
-BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)
-BSCFLAGS += -vdir $(BSV_VERILOG_WRAPPERS_DIR)
+BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)/build/
+BUILD_DIR = $(BSV_VERILOG_WRAPPERS_DIR)
+COUNTEREXAMPLE_DIR = $(CURDIR)/counterexamples/
+BSCFLAGS += -bdir $(BUILD_DIR)
 
 all: verilog-wrappers blarney-wrappers
 
-verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(BUILD_DIR):
+	mkdir -p $@
 
-verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(COUNTEREXAMPLE_DIR):
+	mkdir -p $@
 
-check-prop: assertions.sv verilog-wrappers verilog-props
-	sby -f check.sby
+verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR)
+	bsc $(BSCFLAGS) -vdir $(BSV_VERILOG_WRAPPERS_DIR) -verilog -u $<
 
-blarney-wrappers: CHERICapWrap.py verilog-wrappers
-	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
+verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR) $(COUNTEREXAMPLE_DIR)
+	bsc $(BSCFLAGS) -vdir $(COUNTEREXAMPLE_DIR) -verilog -u $<
 
-.PHONY: clean clean-verilog-wrappers
+check-prop: assertions.sv verilog-props $(COUNTEREXAMPLE_DIR)
+	sby --prefix $(COUNTEREXAMPLE_DIR) -f check.sby
 
-clean-verilog-wrappers: clean
-	rm -f *.v
+blarney-wrappers: CHERICapWrap.py verilog-wrappers $(BUILD_DIR)
+	./CHERICapWrap.py -o $(BUILD_DIR)/CHERIBlarneyWrappers $(BUILD_DIR)/*.v
 
-clean-blarney-wrappers: clean
-	rm -f *.hs
+.PHONY: clean clean-counterexamples full-clean
+
+clean-counterexamples:
+	rm -rf $(COUNTEREXAMPLE_DIR)
 
 clean:
-	rm -f *.bo
+	rm -rf $(BUILD_DIR)
+
+full-clean: clean clean-counterexamples
diff --git a/check.sby b/check.sby
index 9e26204..2f9058e 100644
--- a/check.sby
+++ b/check.sby
@@ -39,12 +39,12 @@ prop_fromToMem: prep -top assert_prop_fromToMem
 
 [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
-module_prop_fromToMem.v
+counterexamples/module_prop_unique.v
+counterexamples/module_prop_exact.v
+counterexamples/module_prop_exactConditions.v
+counterexamples/module_prop_getBase.v
+counterexamples/module_prop_getTop.v
+counterexamples/module_prop_getLength.v
+counterexamples/module_prop_isInBounds.v
+counterexamples/module_prop_setAddr.v
+counterexamples/module_prop_fromToMem.v

From bad0d9cdb620ef8ecb0adf07f161e215a7bf4210 Mon Sep 17 00:00:00 2001
From: Peter Rugg <pdr32@cam.ac.uk>
Date: Tue, 4 Mar 2025 14:04:27 +0000
Subject: [PATCH 29/32] Default to 128-bit caps

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index ac2af28..c97c368 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-CAP ?= 64
+CAP ?= 128
 ifeq ($(CAP), 128)
 BSCFLAGS = -D CAP128
 else

From 7c9559524b68a2cff0b984d026a4dd191b799c58 Mon Sep 17 00:00:00 2001
From: Peter Rugg <pdr32@cam.ac.uk>
Date: Tue, 4 Mar 2025 14:06:41 +0000
Subject: [PATCH 30/32] Increase bit-widths of assertion modules

These were hardwired for RV64, but I'm assuming having too many
bits will not be a problem for RV32?
---
 assertions.sv | 44 ++++++++++++++++++++++----------------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/assertions.sv b/assertions.sv
index 64a06f2..eb51914 100644
--- a/assertions.sv
+++ b/assertions.sv
@@ -1,8 +1,8 @@
 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
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_newBase,
+         input wire [63 : 0] prop_newLen
        );
   wire prop_ok;
 
@@ -20,8 +20,8 @@ module assert_prop_unique(
 endmodule
 
 module assert_prop_exact(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -37,8 +37,8 @@ module assert_prop_exact(
 endmodule
 
 module assert_prop_exactConditions(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -54,8 +54,8 @@ module assert_prop_exactConditions(
 endmodule
 
 module assert_prop_getBase(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -71,9 +71,9 @@ module assert_prop_getBase(
 endmodule
 
 module assert_prop_getTop(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
        );
   wire prop_ok;
 
@@ -90,9 +90,9 @@ module assert_prop_getTop(
 endmodule
 
 module assert_prop_getLength(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_addr,
-         input wire [31 : 0] prop_len
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_len
        );
   wire prop_ok;
 
@@ -109,9 +109,9 @@ module assert_prop_getLength(
 endmodule
 
 module assert_prop_isInBounds(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
        );
   wire prop_ok;
 
@@ -128,9 +128,9 @@ module assert_prop_isInBounds(
 endmodule
 
 module assert_prop_setAddr(
-         input wire [31 : 0] prop_base,
-         input wire [31 : 0] prop_len,
-         input wire [31 : 0] prop_addr
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr
        );
   wire prop_ok;
 

From 199e3c9f7f91b1a6ab7ab771cd1c30131445e27c Mon Sep 17 00:00:00 2001
From: Peter Rugg <pdr32@cam.ac.uk>
Date: Tue, 4 Mar 2025 14:43:05 +0000
Subject: [PATCH 31/32] Extend forallCap to include almightyCap

---
 CHERICapProps.bsv | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index fd8ffb2..8f08a24 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -49,12 +49,18 @@ function Bool implies(Bool x, Bool y) = !x || y;
 
 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)
-    );
+  Bool ret = ?;
+  if (base == 0 && ~len == 0) begin
+    ret = prop(almightyCap);
+  end else begin
+    Exact#(CapPipe) baseCap = setAddr(almightyCap, base);
+    Exact#(CapPipe) boundedCap = setBounds(baseCap.value, len);
+    ret = baseCap.exact && implies
+      ( boundedCap.exact
+      , prop(boundedCap.value)
+      );
+  end
+  return ret;
 endfunction
 
 // Furthermore, every valid capability can be reached by calling setAddr on
@@ -137,7 +143,8 @@ endfunction
 
 (* noinline *)
 function Bool prop_getTop(CapAddr base, CapAddr len, CapAddr addr);
-  function prop(cap) = getTop(cap) == zeroExtend(base) + zeroExtend(len);
+  Bool reqAlmighty = ~len == 0;
+  function prop(cap) = getTop(cap) == zeroExtend(base) + (reqAlmighty ? {1'b1, 0} : zeroExtend(len));
   return forallCap(base, len, addr, prop);
 endfunction
 

From 1d2c0b953ba8e46a6503df7537a8eb02d8df6b5a Mon Sep 17 00:00:00 2001
From: Jonathan Woodruff <jonathan.woodruff@capabilitieslimited.co.uk>
Date: Fri, 7 Mar 2025 15:12:46 +0000
Subject: [PATCH 32/32] Add a property that setBounds will only return a valid
 cap if the bounds are within the original bounds.

---
 CHERICapProps.bsv | 12 ++++++++++++
 assertions.sv     | 21 +++++++++++++++++++++
 check.sby         |  4 ++++
 3 files changed, 37 insertions(+)

diff --git a/CHERICapProps.bsv b/CHERICapProps.bsv
index 8f08a24..fdda65d 100644
--- a/CHERICapProps.bsv
+++ b/CHERICapProps.bsv
@@ -192,4 +192,16 @@ function Bool prop_fromToMem(CapMem in);
   return (cm == in);
 endfunction
 
+(* noinline *)
+function Bool prop_setBounds(CapAddr base, CapAddr len, CapAddr addr, CapAddr new_len);
+  function prop(cap);
+    let new_cap = setBounds(cap,new_len).value;
+    return implies( isValidCap(new_cap),
+                    getBase(cap) <= getBase(new_cap)
+                    && getTop(cap) >= getTop(new_cap)
+                  );
+  endfunction
+  return forallCap(base, len, addr, prop);
+endfunction
+
 endpackage
diff --git a/assertions.sv b/assertions.sv
index eb51914..aa0763f 100644
--- a/assertions.sv
+++ b/assertions.sv
@@ -160,3 +160,24 @@ module assert_prop_fromToMem(
     assert(prop_ok);
   end
 endmodule
+
+module assert_prop_setBounds(
+         input wire [63 : 0] prop_base,
+         input wire [63 : 0] prop_len,
+         input wire [63 : 0] prop_addr,
+         input wire [63 : 0] prop_new_len
+       );
+  wire prop_ok;
+
+  module_prop_setBounds module_prop_setBounds_inst(
+    .prop_setBounds_base(prop_base),
+    .prop_setBounds_len(prop_len),
+    .prop_setBounds_addr(prop_addr),
+    .prop_setBounds_new_len(prop_new_len),
+    .prop_setBounds(prop_ok)
+  );
+
+  always @(*) begin
+    assert(prop_ok);
+  end
+endmodule
diff --git a/check.sby b/check.sby
index 2f9058e..d68cbe5 100644
--- a/check.sby
+++ b/check.sby
@@ -8,6 +8,7 @@ prop_getLength
 prop_isInBounds
 prop_setAddr
 prop_fromToMem
+prop_setBounds
 
 [options]
 depth 1
@@ -27,6 +28,7 @@ read -formal module_prop_getLength.v
 read -formal module_prop_isInBounds.v
 read -formal module_prop_setAddr.v
 read -formal module_prop_fromToMem.v
+read -formal module_prop_setBounds.v
 prop_getBase: prep -top assert_prop_getBase
 prop_getTop: prep -top assert_prop_getTop
 prop_getLength: prep -top assert_prop_getLength
@@ -36,6 +38,7 @@ prop_exact: prep -top assert_prop_exact
 prop_exactConditions: prep -top assert_prop_exactConditions
 prop_setAddr: prep -top assert_prop_setAddr
 prop_fromToMem: prep -top assert_prop_fromToMem
+prop_setBounds: prep -top assert_prop_setBounds
 
 [files]
 assertions.sv
@@ -48,3 +51,4 @@ 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