Merge branch 'CHERI' of https://github.com/CTSRD-CHERI/Toooba into CHERI

2020-07-08 12:45:43 +01:00
parent 0b8a031184 68d3bd484e
commit 40b44d51e2
418 changed files with 179163 additions and 170736 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -17,3 +17,4 @@ symbol_table.txt
 vpi_wrapper_*
 builds/RV*/build_dir
 builds/RV*/Verilog_RTL
+.depends.mk
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_bluesim/Makefile
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_bluesim/Makefile
@@ -0,0 +1,69 @@
+###  -*-Makefile-*-
+
+# ================================================================
+# Path to RISCY-OOO sources
+
+RISCY_HOME ?= ../../src_Core/RISCY_OOO
+# RISCY_HOME ?= $(HOME)/Projects/RISCV/MIT-riscy/riscy-OOO
+
+RISCY_DIRS = $(RISCY_HOME)/procs/RV64G_OOO:$(RISCY_HOME)/procs/lib:$(RISCY_HOME)/coherence/src:$(RISCY_HOME)/fpgautils/lib
+
+CONNECTAL_DIRS = $(RISCY_HOME)/connectal/bsv:$(RISCY_HOME)/connectal/tests/spi:$(RISCY_HOME)/connectal/lib/bsv
+
+RVFI_DII_DIRS = $(RISCY_HOME)/../../src_Verifier:$(RISCY_HOME)/../../src_Verifier/BSV-RVFI-DII
+
+CHERI_DIRS = $(RISCY_HOME)/../../libs/cheri-cap-lib
+
+# ALL_RISCY_DIRS = $(RISCY_DIRS)
+ALL_RISCY_DIRS = $(RISCY_DIRS):$(CONNECTAL_DIRS):$(RVFI_DII_DIRS):$(CHERI_DIRS)
+
+# ================================================================
+
+REPO ?= ../..
+ARCH ?= RV64ACDFIMSUxCHERI
+
+# ================================================================
+# RISC-V config macros passed into Bluespec 'bsc' compiler
+
+BSC_COMPILATION_FLAGS += \
+	-D RV64 \
+	-D ISA_PRIV_M  -D ISA_PRIV_U  -D ISA_PRIV_S  \
+	-D SV39  \
+	-D ISA_I  -D ISA_M  -D ISA_A  -D ISA_F  -D ISA_D  -D ISA_FD_DIV  -D ISA_C  \
+	-D SHIFT_BARREL    \
+	-D MULT_SYNTH    \
+	-D Near_Mem_Caches    \
+	-D FABRIC64    \
+	-D CheriBusBytes=8 \
+	-D CheriMasterIDWidth=1 \
+	-D CheriTransactionIDWidth=5 \
+	-D CAP128 -D BLUESIM \
+	-D MEM64 \
+	-D RISCV \
+	-D RVFI_DII \
+	-D RVFI \
+
+
+# Default ISA test
+
+TEST ?= rv64ui-p-add
+
+#================================================================
+# Parameter settings for MIT RISCY
+
+BSC_COMPILATION_FLAGS += -D BSIM \
+
+
+CACHE_SIZE ?= TEST
+
+include $(REPO)/builds/Resources/Include_RISCY_Config.mk
+
+#================================================================
+# Common boilerplate rules
+
+include $(REPO)/builds/Resources/Include_Common.mk
+
+#================================================================
+# Makefile rules for building for specific simulator: bluesim
+
+include $(REPO)/builds/Resources/Include_bluesim.mk
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_bluesim/TagTableStructure.bsv
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_bluesim/TagTableStructure.bsv
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_verilator/Makefile
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_verilator/Makefile
@@ -20,29 +20,29 @@ ALL_RISCY_DIRS = $(RISCY_DIRS):$(CONNECTAL_DIRS):$(RVFI_DII_DIRS):$(CHERI_DIRS)
 # ================================================================

 REPO ?= ../..
-ARCH ?= RV64ACDFIMSU
+ARCH ?= RV64ACDFIMSUxCHERI

 # ================================================================
 # RISC-V config macros passed into Bluespec 'bsc' compiler

-MORE_DEFINES = RV64 \
-               ISA_PRIV_M ISA_PRIV_U ISA_PRIV_S \
-               SV39 \
-               ISA_I ISA_M ISA_A ISA_F ISA_D ISA_FD_DIV ISA_C \
-               SHIFT_BARREL \
-               MULT_SYNTH \
-               Near_Mem_Caches \
-               FABRIC64 \
-               CheriBusBytes=8 \
-               CheriMasterIDWidth=1 \
-               CheriTransactionIDWidth=5 \
-               CAP128 \
-               MEM64 \
-               RVFI_DII \
-               RVFI BLUESIM\
-               RISCV
-BSC_DEFINES += $(MORE_DEFINES)
-BSC_COMPILATION_FLAGS += $(addprefix -D , $(MORE_DEFINES))
+BSC_COMPILATION_FLAGS += \
+	-D RV64 \
+	-D ISA_PRIV_M  -D ISA_PRIV_U  -D ISA_PRIV_S  \
+	-D SV39  \
+	-D ISA_I  -D ISA_M  -D ISA_A  -D ISA_F  -D ISA_D  -D ISA_FD_DIV  -D ISA_C  \
+	-D SHIFT_BARREL    \
+	-D MULT_SYNTH    \
+	-D Near_Mem_Caches    \
+	-D FABRIC64    \
+	-D CheriBusBytes=8 \
+	-D CheriMasterIDWidth=1 \
+	-D CheriTransactionIDWidth=5 \
+	-D CAP128 -D BLUESIM \
+	-D MEM64 \
+	-D RISCV \
+	-D RVFI_DII \
+	-D RVFI \
+

 # Default ISA test

@@ -53,6 +53,7 @@ TEST ?= rv64ui-p-add

 BSC_COMPILATION_FLAGS += -D BSIM \

+
 CACHE_SIZE ?= TEST

 include $(REPO)/builds/Resources/Include_RISCY_Config.mk
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_verilator/Mem.hex
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_verilator/Mem.hex
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_verilator/TagTableStructure.bsv
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_RVFI_DII_verilator/TagTableStructure.bsv
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_bluesim/Makefile
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_bluesim/Makefile
@@ -10,13 +10,15 @@ RISCY_DIRS = $(RISCY_HOME)/procs/RV64G_OOO:$(RISCY_HOME)/procs/lib:$(RISCY_HOME)

 CONNECTAL_DIRS = $(RISCY_HOME)/connectal/bsv:$(RISCY_HOME)/connectal/tests/spi:$(RISCY_HOME)/connectal/lib/bsv

+CHERI_DIRS = $(RISCY_HOME)/../../libs/cheri-cap-lib
+
 # ALL_RISCY_DIRS = $(RISCY_DIRS)
-ALL_RISCY_DIRS = $(RISCY_DIRS):$(CONNECTAL_DIRS)
+ALL_RISCY_DIRS = $(RISCY_DIRS):$(CONNECTAL_DIRS):$(CHERI_DIRS)

 # ================================================================

 REPO ?= ../..
-ARCH ?= RV64ACDFIMSU
+ARCH ?= RV64ACDFIMSUxCHERI

 # ================================================================
 # RISC-V config macros passed into Bluespec 'bsc' compiler
@@ -26,13 +28,16 @@ BSC_COMPILATION_FLAGS += \
 	-D ISA_PRIV_M  -D ISA_PRIV_U  -D ISA_PRIV_S  \
 	-D SV39  \
 	-D ISA_I  -D ISA_M  -D ISA_A  -D ISA_F  -D ISA_D  -D ISA_FD_DIV  -D ISA_C  \
-	-D CheriBusBytes=8 \
-	-D CheriMasterIDWidth=1 \
-	-D CheriTransactionIDWidth=5 \
 	-D SHIFT_BARREL    \
 	-D MULT_SYNTH    \
 	-D Near_Mem_Caches    \
 	-D FABRIC64    \
+	-D CheriBusBytes=8 \
+	-D CheriMasterIDWidth=1 \
+	-D CheriTransactionIDWidth=5 \
+	-D CAP128 -D BLUESIM \
+	-D MEM64 \
+	-D RISCV \


 # Default ISA test
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_bluesim/TagTableStructure.bsv
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_bluesim/TagTableStructure.bsv
@@ -0,0 +1,34 @@
+/*-
+ *
+ * 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@
+ */
+
+// This file was generated by the tagsparams.py script
+// 2020-03-24 15:49:40.494187
+
+import Vector::*;
+Vector#(2, Integer) tableStructure = cons(0, cons(64, nil));
+Integer table_end_addr = 'hbffff000;
+Integer table_start_addr = 'hbf7df080;
+Integer covered_start_addr = 'h80000000;
+Integer covered_mem_size  = 'h3fffc000;
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_verilator/Makefile
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_verilator/Makefile
@@ -18,27 +18,26 @@ ALL_RISCY_DIRS = $(RISCY_DIRS):$(CONNECTAL_DIRS):$(CHERI_DIRS)
 # ================================================================

 REPO ?= ../..
-ARCH ?= RV64ACDFIMSU
+ARCH ?= RV64ACDFIMSUxCHERI

 # ================================================================
 # RISC-V config macros passed into Bluespec 'bsc' compiler

-MORE_DEFINES = RV64 \
-               ISA_PRIV_M ISA_PRIV_U ISA_PRIV_S \
-               SV39 \
-               ISA_I ISA_M ISA_A ISA_F ISA_D ISA_FD_DIV ISA_C \
-               SHIFT_BARREL \
-               MULT_SYNTH \
-               Near_Mem_Caches \
-               FABRIC64 \
-               CheriBusBytes=8 \
-               CheriMasterIDWidth=1 \
-               CheriTransactionIDWidth=5 \
-               CAP128 BLUESIM\
-               MEM64 \
-               RISCV
-BSC_DEFINES += $(MORE_DEFINES)
-BSC_COMPILATION_FLAGS += $(addprefix -D , $(MORE_DEFINES))
+BSC_COMPILATION_FLAGS += \
+	-D RV64 \
+	-D ISA_PRIV_M  -D ISA_PRIV_U  -D ISA_PRIV_S  \
+	-D SV39  \
+	-D ISA_I  -D ISA_M  -D ISA_A  -D ISA_F  -D ISA_D  -D ISA_FD_DIV  -D ISA_C  \
+	-D SHIFT_BARREL    \
+	-D MULT_SYNTH    \
+	-D Near_Mem_Caches    \
+	-D FABRIC64    \
+	-D CheriBusBytes=8 \
+	-D CheriMasterIDWidth=1 \
+	-D CheriTransactionIDWidth=5 \
+	-D CAP128 -D BLUESIM \
+	-D MEM64 \
+	-D RISCV \


 # Default ISA test
--- a/builds/RV64ACDFIMSUxCHERI_Toooba_verilator/TagTableStructure.bsv
+++ b/builds/RV64ACDFIMSUxCHERI_Toooba_verilator/TagTableStructure.bsv
@@ -0,0 +1,34 @@
+/*-
+ *
+ * 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@
+ */
+
+// This file was generated by the tagsparams.py script
+// 2020-03-24 15:49:40.494187
+
+import Vector::*;
+Vector#(2, Integer) tableStructure = cons(0, cons(64, nil));
+Integer table_end_addr = 'hbffff000;
+Integer table_start_addr = 'hbf7df080;
+Integer covered_start_addr = 'h80000000;
+Integer covered_mem_size  = 'h3fffc000;
--- a/builds/Resources/Include_Common.mk
+++ b/builds/Resources/Include_Common.mk
@@ -63,7 +63,6 @@ BSC_COMPILATION_FLAGS += \

 EXAMPLE ?= PLEASE_DEFINE_EXAMPLE_PATH_TO_ELF

-
 .PHONY: run_example
 run_example:
 	make -C  $(TESTS_DIR)/elf_to_hex
--- a/builds/Resources/Include_RISCY_Config.mk
+++ b/builds/Resources/Include_RISCY_Config.mk
@@ -10,7 +10,7 @@ PROC := RV64G_OOO
 # core size
 CORE_SIZE ?= SMALL
 # cache size
-CACHE_SIZE ?= SMALL
+CACHE_SIZE ?= LARGE
 # always include perf counter
 PERF_COUNT := true
 # dram type in simulation: VC707 or AWSF1
@@ -69,15 +69,13 @@ XILINX_FP_FMA_LATENCY = 3
 XILINX_INT_MUL_LATENCY = 2


-NEW_DEFINES = \
-	CORE_$(CORE_SIZE) \
-	NUM_CORES=$(CORE_NUM) \
-	CACHE_$(CACHE_SIZE) \
-        XILINX_FP_FMA_LATENCY=$(XILINX_FP_FMA_LATENCY) \
-        XILINX_INT_MUL_LATENCY=$(XILINX_INT_MUL_LATENCY) \
-	USE_BSV_BRAM_SYNC_FIFO
-BSC_DEFINES += $(NEW_DEFINES)
-BSC_COMPILATION_FLAGS += $(addprefix -D , $(NEW_DEFINES))
+BSC_COMPILATION_FLAGS += \
+	-D CORE_$(CORE_SIZE) \
+	-D NUM_CORES=$(CORE_NUM) \
+	-D CACHE_$(CACHE_SIZE) \
+        -D XILINX_FP_FMA_LATENCY=$(XILINX_FP_FMA_LATENCY) \
+        -D XILINX_INT_MUL_LATENCY=$(XILINX_INT_MUL_LATENCY) \
+	-D USE_BSV_BRAM_SYNC_FIFO \


 # TODO:
--- a/builds/Resources/Include_bluesim.mk
+++ b/builds/Resources/Include_bluesim.mk
@@ -12,11 +12,22 @@ TMP_DIRS  = -bdir build_dir  -simdir build_dir  -info-dir build_dir
 build_dir:
 	mkdir -p $@

+ifeq (,$(filter clean full_clean,$(MAKECMDGOALS)))
+include .depends.mk
+
+.depends.mk: build_dir
+	bluetcl -exec makedepend -elab -sim  $(TMP_DIRS)  $(RTL_GEN_DIRS)  $(BSC_COMPILATION_FLAGS)  -p $(BSC_PATH) -o $@ $(TOPFILE)
+endif
+
+%.bo:
+	$(info building $@)
+	bsc -elab -sim  $(TMP_DIRS)  $(RTL_GEN_DIRS)  $(BSC_COMPILATION_FLAGS)  -p $(BSC_PATH) $<
+
 .PHONY: compile
-compile: build_dir
-	@echo "INFO: Re-compiling Core (CPU, Caches)"
-	bsc -u -elab -sim  $(TMP_DIRS)  $(BSC_COMPILATION_FLAGS)  -p $(BSC_PATH)  $(TOPFILE)
-	@echo "INFO: Re-compiled  Core (CPU, Caches)"
+compile: build_dir build_dir/Top_HW_Side.bo
+#	@echo "INFO: Re-compiling Core (CPU, Caches)"
+#	bsc -u -elab -sim  $(TMP_DIRS)  $(BSC_COMPILATION_FLAGS)  -p $(BSC_PATH)  $(TOPFILE)
+#	@echo "INFO: Re-compiled  Core (CPU, Caches)"

 # ================================================================
 # Compile and link Bluesim intermediate files into a Bluesim executable
@@ -33,7 +44,7 @@ BSC_C_FLAGS += \
 # you may have to remove the line: -Xc++ -D_GLIBCXX_USE_CXX11_ABI=0

 .PHONY: simulator
-simulator:
+simulator: build_dir/Top_HW_Side.bo
 	@echo "INFO: linking bsc-compiled objects into Bluesim executable"
 	bsc -sim -parallel-sim-link 8 +RTS -K128M -RTS \
 		$(TMP_DIRS) \
--- a/builds/Resources/Include_verilator.mk
+++ b/builds/Resources/Include_verilator.mk
@@ -9,29 +9,25 @@

 RTL_GEN_DIRS = -vdir Verilog_RTL  -bdir build_dir  -info-dir build_dir

-.depends.mk: $(REPO)/builds/Resources/genDependencies.tcl build_dir
-	$(info generating bsv dependency graph)
-	BSC_PATH=$(BSC_PATH) \
-	BSC_DEFINES="$(BSC_DEFINES)" \
-	BSC_BUILDDIR=build_dir \
-	BSC_TOPFILE=$(REPO)/src_Testbench/Top/Top_HW_Side.bsv \
-	OUTPUTFILE=$@ \
-	$<
-
 build_dir:
 	mkdir -p $@

 Verilog_RTL:
 	mkdir -p $@

+ifeq (,$(filter clean full_clean,$(MAKECMDGOALS)))
 include .depends.mk

+.depends.mk: build_dir Verilog_RTL
+	bluetcl -exec makedepend -verilog -elab  $(RTL_GEN_DIRS)  $(BSC_COMPILATION_FLAGS) -p $(BSC_PATH) -o $@ $(TOPFILE)
+endif
+
 %.bo:
 	$(info building $@)
-	bsc -verilog -elab -bdir build_dir -vdir Verilog_RTL $(BSC_COMPILATION_FLAGS) -p $(BSC_PATH) $<
+	bsc -verilog -elab  $(RTL_GEN_DIRS)  $(BSC_COMPILATION_FLAGS) -p $(BSC_PATH) $<

 .PHONY: compile
-compile: .depends.mk build_dir Verilog_RTL build_dir/Top_HW_Side.bo
+compile: build_dir Verilog_RTL build_dir/Top_HW_Side.bo
 #Verilog_RTL/mkTop_HW_Side.v:  build_dir Verilog_RTL /tmp/src_dir $(VERILOG_SUB_MODULES)
 #Verilog_RTL/mkTop_HW_Side.v: $(TOPFILE) build_dir/Top_HW_Side.bo build_dir Verilog_RTL
 #	@echo  "INFO: Verilog RTL generation ..."
--- a/builds/Resources/genDependencies.tcl
+++ b/builds/Resources/genDependencies.tcl
@@ -1,118 +0,0 @@
-#! /usr/bin/env bluetcl
-#
-# Copyright (c) 2020 Alexandre Joannou
-# All rights reserved.
-#
-# This software was developed by SRI International and the University of
-# Cambridge Computer Laboratory (Department of Computer Science and
-# Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
-# DARPA SSITH 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@
-#
-
-namespace import ::Bluetcl::*
-
-# there does not seam to be a nice "getopt" in tcl, so for now, falling back on:
-#
-# - env variables:
-# BSC_PATH
-# BSC_DEFINES
-# BSC_BUILDDIR
-# BSC_TOPFILE
-# OUTPUTFILE
-#
-# - if argv is non empty, each arg is passed individually to a flags set command
-#   (that is, can't pass flags that expect arguments themselves like -D XXX)
-################################################################################
-
-if { [info exists env(BSC_PATH)] } {
-  set path $env(BSC_PATH)
-} else {
-  #set path ".:+"
-  set path "../../libs/BlueStuff:../../libs/BlueStuff/AXI:../../libs/BlueStuff/BlueUtils:../../libs/BlueStuff/BlueBasics:../../src_Core/RISCY_OOO/procs/RV64G_OOO:../../src_Core/RISCY_OOO/procs/lib:../../src_Core/RISCY_OOO/coherence/src:../../src_Core/RISCY_OOO/fpgautils/lib:../../src_Core/RISCY_OOO/connectal/bsv:../../src_Core/RISCY_OOO/connectal/tests/spi:../../src_Core/RISCY_OOO/connectal/lib/bsv:../../src_Core/RISCY_OOO/../../src_Verifier:../../src_Core/RISCY_OOO/../../src_Verifier/BSV-RVFI-DII:../../src_Core/RISCY_OOO/../CHERI:../../src_Core/RISCY_OOO/../../libs/cheri-cap-lib:../../src_Core/CPU:../../src_Core/ISA:../../src_Core/Core:../../src_Core/PLIC:../../src_Core/Debug_Module:../../src_Core/BSV_Additional_Libs:../../src_Testbench/Top:../../src_Testbench/SoC:../../libs/TagController/TagController:../../libs/TagController/TagController/CacheCore:+"
-}
-
-if { [info exists env(BSC_DEFINES)] } {
-  set defines [split $env(BSC_DEFINES)]
-} else {
-  #set defines {}
-  set defines [split "RISCV RV64 ISA_PRIV_M ISA_PRIV_U ISA_PRIV_S SV39 ISA_I ISA_M ISA_A ISA_F ISA_D ISA_FD_DIV ISA_C SHIFT_BARREL MULT_SYNTH Near_Mem_Caches FABRIC64 CAP128 MEM64 BSIM CORE_SMALL NUM_CORES=1 CACHE_SMALL XILINX_FP_FMA_LATENCY=3 XILINX_INT_MUL_LATENCY=2 USE_BSV_BRAM_SYNC_FIFO"]
-}
-
-if { [info exists env(BSC_BUILDDIR)] } {
-  set builddir $env(BSC_BUILDDIR)
-} else {
-  set builddir "build"
-}
-
-if { [info exists env(BSC_TOPFILE)] } {
-  set topfile $env(BSC_TOPFILE)
-} else {
-  set topfile "Top.bsv"
-}
-
-if { [info exists env(OUTPUTFILE)] } {
-  set outputfile $env(OUTPUTFILE)
-} else {
-  set outputfile ".depends.mk"
-}
-
-# debug prints
-#puts "path: $path"
-#puts "defines: $defines"
-#puts "builddir: $builddir"
-#puts "topfile: $topfile"
-#puts "outputfile: $outputfile"
-#puts "argv: $argv"
-
-# setting compiler flags
-################################################################################
-
-flags set -p $path
-flags set -bdir $builddir
-flags set -verilog
-foreach i $defines {
-  flags set -D $i
-}
-if { $argc > 0 } { foreach i $argv { flags set $i } }
-
-# output of "depend make" seams to be of the form
-# { {tgtA {depA0 depA1 ...}}
-#   {tgtB {depB0 depB1 ...}}
-#   ...
-# }
-# reformating it for make
-################################################################################
-try {
-  set res [depend make $topfile]
-} finally {
-  if { [info exists res] } {
-    set fd [open $outputfile w]
-    foreach i $res {
-      set tgt [lindex $i 0]
-      set deps [join [lindex $i 1]]
-      puts $fd [append tgt ": " $deps]
-    }
-    close $fd
-    puts "generated make dependency rules for \"$topfile\" in: $outputfile"
-  } else {
-    puts "could not generate make dependency rules for \"$topfile\""
-  }
-}
--- a/src_Core/BSV_Additional_Libs/CreditCounter.bsv
+++ b/src_Core/BSV_Additional_Libs/CreditCounter.bsv
@@ -37,7 +37,7 @@ module mkCreditCounter (CreditCounter_IFC #(w));

   method UInt #(w) value = crg [1];

-   method Action incr;
+   method Action incr if (crg [0] != maxBound);
      if (crg [0] == maxBound) begin
         $display ("%0d: ERROR: CreditCounter: overflow", cur_cycle);
         $finish (1);    // Assertion failure
--- a/src_Core/CPU/CPU_Decode_C.bsv
+++ b/src_Core/CPU/CPU_Decode_C.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2016-2019 Bluespec, Inc. All Rights Reserved
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package CPU_Decode_C;

--- a/src_Core/CPU/Core.bsv
+++ b/src_Core/CPU/Core.bsv
@@ -2,6 +2,21 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
@@ -186,6 +201,13 @@ interface Core;
   interface Vector #(SupSize, Get #(Trace_Data2)) v_to_TV;
 `endif

+`ifdef DEBUG_WEDGE
+    (* always_enabled *)
+    method Tuple2#(CapMem, Bit#(32)) debugLastInst;
+    (* always_enabled *)
+    method Tuple2#(CapMem, Bit#(32)) debugNextInst;
+`endif
+
 endinterface

 // fixpoint to instantiate modules
@@ -1431,4 +1453,9 @@ module mkCore#(CoreId coreId)(Core);
   interface v_to_TV = map (toGet, v_f_to_TV);
 `endif

+`ifdef DEBUG_WEDGE
+    method Tuple2#(CapMem, Bit#(32)) debugLastInst = commitStage.debugLastInst;
+    method Tuple2#(CapMem, Bit#(32)) debugNextInst = rob.debugNextInst;
+`endif
+
 endmodule
--- a/src_Core/CPU/CsrFile.bsv
+++ b/src_Core/CPU/CsrFile.bsv
@@ -2,9 +2,11 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
 //
-// CHERI modifications:
-//     Copyright (c) 2020 Jonathan Woodruff
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
 //     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
 //     All rights reserved.
 //
 //     This software was developed by SRI International and the University of
@@ -12,6 +14,9 @@
 //     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
 //     DARPA SSITH research programme.
 //
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
@@ -290,6 +295,14 @@ module mkStatsCsr(StatsCsr);
    endmethod
 endmodule

+function Reg#(Data) scrToCsr(Reg#(CapReg) scr) = interface Reg
+        method _write (x) = action CapPipe scr_pipe = cast(scr); scr <= cast(setOffset(scr_pipe, x).value); endaction;
+        method Data _read;
+          CapPipe scr_pipe = cast(scr);
+          return getOffset(scr_pipe);
+        endmethod
+    endinterface;
+
 // same as EHR except that read port 0 is not ordered with other methods. Read
 // port 1 will still get bypassing from write port 0.
 module mkConfigEhr#(t init)(Ehr#(n, t)) provisos(Bits#(t, w));
@@ -395,11 +408,13 @@ module mkCsrFile #(Data hartid)(CsrFile);
    // misa
    Reg#(Data) misa_csr = readOnlyReg({getXLBits, 36'b0, getExtensionBits(isa)});
    // medeleg: some exceptions don't exist, fix corresponding bits to 0
+    Reg#(Bit#(3)) medeleg_28_26_reg <- mkCsrReg(0); // CHERI causes 0x1a-0x1c
    Reg#(Bit#(1)) medeleg_15_reg <- mkCsrReg(0); // cause 15
    Reg#(Bit#(3)) medeleg_13_11_reg <- mkCsrReg(0); // case 13-11
    Reg#(Bit#(10)) medeleg_9_0_reg <- mkCsrReg(0); // cause 9-0
-    Reg#(Data) medeleg_csr = concatReg6(
-        readOnlyReg(48'b0), medeleg_15_reg,
+    Reg#(Data) medeleg_csr = concatReg8(
+        readOnlyReg(35'b0), medeleg_28_26_reg,
+        readOnlyReg(10'b0), medeleg_15_reg,
        readOnlyReg(1'b0), medeleg_13_11_reg,
        readOnlyReg(1'b0), medeleg_9_0_reg
    );
@@ -754,8 +769,10 @@ module mkCsrFile #(Data hartid)(CsrFile);
            // Supervisor CSRs
            CSRsstatus:    sstatus_csr;
            CSRsie:        sie_csr;
+            CSRstvec:      scrToCsr(stcc_reg); // Only accessed by debugger. CPU accesses decoded into cspecialrw
            CSRscounteren: scounteren_csr;
            CSRsscratch:   sscratch_csr;
+            CSRsepc:       scrToCsr(sepcc_reg[1]); // Only accessed by debugger. CPU accesses decoded into cspecialrw
            CSRscause:     scause_csr;
            CSRstval:      stval_csr;
            CSRsip:        sip_csr;
@@ -766,8 +783,10 @@ module mkCsrFile #(Data hartid)(CsrFile);
            CSRmedeleg:    medeleg_csr;
            CSRmideleg:    mideleg_csr;
            CSRmie:        mie_csr;
+            CSRmtvec:      scrToCsr(mtcc_reg); // Only accessed by debugger. CPU accesses decoded into cspecialrw
            CSRmcounteren: mcounteren_csr;
            CSRmscratch:   mscratch_csr;
+            CSRmepc:       scrToCsr(mepcc_reg[1]); // Only accessed by debugger. CPU accesses decoded into cspecialrw
            CSRmcause:     mcause_csr;
            CSRmtval:      mtval_csr;
            CSRmip:        mip_csr;
@@ -799,10 +818,7 @@ module mkCsrFile #(Data hartid)(CsrFile);

 `ifdef INCLUDE_GDB_CONTROL
           CSRdcsr:       rg_dcsr;    // TODO: take NMI into account (cf. Piccolo/Flute)
-           CSRdpc:        interface Reg;
-                              method _write (x) = action rg_dpc <= setAddrUnsafe(rg_dpc, x); endaction;
-                              method _read = getAddr(rg_dpc);
-                          endinterface
+           CSRdpc:        scrToCsr(rg_dpc);
           CSRdscratch0:  rg_dscratch0;
           CSRdscratch1:  rg_dscratch1;
 `endif
@@ -871,7 +887,7 @@ module mkCsrFile #(Data hartid)(CsrFile);
                                          x [3],        // ie_vec[prvM]
                                          x [1],        // ie_vec[prvS]
                                          x [0]);       // ie_vec[prvU]
-            CSRmedeleg:    { 48'b0, x[15], 1'b0, x[13:12], x[11], 1'b0, x[9:0]};
+            CSRmedeleg:    { 35'b0, x[28:26], 10'b0, x[15], 1'b0, x[13:12], x[11], 1'b0, x[9:0]};
            CSRmideleg:    { 52'b0, x[11], 1'b0, x[9:8], x[7], 1'b0, x[5:4], x[3], 1'b0, x[1:0]};
            CSRmip:        ((mip_csr & (~ mip_mie_warl_mask)) | (x & mip_mie_warl_mask));
            CSRmie:        (x & mip_mie_warl_mask);
@@ -1055,8 +1071,8 @@ module mkCsrFile #(Data hartid)(CsrFile);
        // check if trap is delegated
        Bool deleg = prv_reg <= prvS && (case(t) matches
            tagged Exception .e: return medeleg_csr[pack(e)] == 1;
+            tagged CapException .ce: return medeleg_csr[pack(CHERIFault)] == 1;
            tagged Interrupt .i: return mideleg_csr[pack(i)] == 1;
-            default: return False;
        endcase);
        // handle the trap
        if(deleg) begin // handle in S mode
@@ -1145,7 +1161,7 @@ module mkCsrFile #(Data hartid)(CsrFile);
                                          /* ie_vec [prvM] */ prev_ie_vec[prvM],
                                          ie_vec [prvS],
                                          ie_vec [prvU]);
-        return RET_Updates {new_pcc: cast(mepcc_reg[0])
+        return RET_Updates {new_pcc: cast(setKind(mepcc_reg[0], getKind(mepcc_reg[0]) == SENTRY ? UNSEALED : getKind(mepcc_reg[0])))
 `ifdef INCLUDE_TANDEM_VERIF
                            , prv:    prev_prv_vec[prvM],
                            status: mstatus_val
@@ -1174,7 +1190,7 @@ module mkCsrFile #(Data hartid)(CsrFile);
                                          ie_vec [prvM],
                                          /* ie_vec [prvS] */ prev_ie_vec[prvS],
                                          ie_vec [prvU]);
-        return RET_Updates {new_pcc: cast(sepcc_reg[0])
+        return RET_Updates {new_pcc: cast(setKind(sepcc_reg[0], getKind(sepcc_reg[0]) == SENTRY ? UNSEALED : getKind(sepcc_reg[0])))
 `ifdef INCLUDE_TANDEM_VERIF
                            , prv:    prev_prv_vec[prvS],
                            status: mstatus_val
--- a/src_Core/CPU/LLC_AXI4_Adapter.bsv
+++ b/src_Core/CPU/LLC_AXI4_Adapter.bsv
@@ -1,3 +1,17 @@
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+
 package LLC_AXI4_Adapter;

 // ================================================================
@@ -140,7 +154,7 @@ module mkLLC_AXi4_Adapter #(MemFifoClient #(idT, childT) llc)
      let new_cline = CLine { tag: rg_rd_rsp_beat[0] == 0 ? unpack(new_cline_tag) : rg_cline.tag
                            , data: unpack(new_cline_data) };

-      if (rg_rd_rsp_beat == 7) begin
+      if (mem_rsp.rlast) begin
         let ldreq <- pop (f_pending_reads);
         MemRsMsg #(idT, childT) resp = MemRsMsg {data:  new_cline,
                                                  child: ldreq.child,
@@ -150,10 +164,13 @@ module mkLLC_AXi4_Adapter #(MemFifoClient #(idT, childT) llc)

         if (cfg_verbosity > 1)
            $display ("    Response to LLC: ", fshow (resp));
-      end

-      rg_cline <= new_cline;
-      rg_rd_rsp_beat <= rg_rd_rsp_beat + 1;
+         rg_rd_rsp_beat <= 0;
+         rg_cline <= unpack(0);
+      end else begin
+         rg_rd_rsp_beat <= rg_rd_rsp_beat + 1;
+         rg_cline <= new_cline;
+      end
   endrule

   // ================================================================
@@ -190,8 +207,11 @@ module mkLLC_AXi4_Adapter #(MemFifoClient #(idT, childT) llc)

      // on last flit...
      // ===============
-      if (rg_wr_req_beat == 7)
+      if (rg_wr_req_beat == 7) begin
         llc.toM.deq;
+         rg_wr_req_beat <= 0;
+      end else // increment flit counter
+         rg_wr_req_beat <= rg_wr_req_beat + 1;

      // on each flit ...
      // ================
@@ -203,9 +223,6 @@ module mkLLC_AXi4_Adapter #(MemFifoClient #(idT, childT) llc)
        wstrb:  line_strb[rg_wr_req_beat],
        wlast:  rg_wr_req_beat == 7,
        wuser:  pack(line_data[rg_wr_req_beat[2:1]].tag)});
-      // increment flit counter
-      rg_wr_req_beat <= rg_wr_req_beat + 1;
-
   endrule

   // ----------------
--- a/src_Core/CPU/MMIOPlatform.bsv
+++ b/src_Core/CPU/MMIOPlatform.bsv
@@ -1,7 +1,22 @@
-
 // Copyright (c) 2018 Massachusetts Institute of Technology
 // Portions (c) 2019-2020 Bluespec, Inc.
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/CPU/MMIO_AXI4_Adapter.bsv
+++ b/src_Core/CPU/MMIO_AXI4_Adapter.bsv
@@ -1,4 +1,18 @@
 // Copyright (c) 2019-2020 Bluespec, Inc.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package MMIO_AXI4_Adapter;

--- a/src_Core/CPU/Proc.bsv
+++ b/src_Core/CPU/Proc.bsv
@@ -5,6 +5,22 @@ package Proc;
 // Copyright (c) 2018 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
@@ -87,6 +103,11 @@ import ProcTypes   :: *;
 import Trace_Data2 :: *;
 `endif

+`ifdef DEBUG_WEDGE
+import CHERICap    :: *;
+import CHERICC_Fat :: *;
+`endif
+
 // ================================================================

 (* synthesize *)
@@ -312,6 +333,11 @@ module mkProc (Proc_IFC);
   interface v_to_TV = core [0].v_to_TV;
 `endif

+`ifdef DEBUG_WEDGE
+    method Tuple2#(CapMem, Bit#(32)) hart0_last_inst = core[0].debugLastInst;
+    method Tuple2#(CapMem, Bit#(32)) hart0_next_inst = core[0].debugNextInst;
+`endif
+
 endmodule: mkProc

 // ================================================================
--- a/src_Core/CPU/Proc_IFC.bsv
+++ b/src_Core/CPU/Proc_IFC.bsv
@@ -1,4 +1,19 @@
 // Copyright (c) 2016-2020 Bluespec, Inc. All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package Proc_IFC;

@@ -31,6 +46,11 @@ import Trace_Data2 :: *;
 import Types :: *;
 `endif

+`ifdef DEBUG_WEDGE
+import CHERICap    :: *;
+import CHERICC_Fat :: *;
+`endif
+
 // ================================================================
 // CPU interface

@@ -113,6 +133,13 @@ interface Proc_IFC;
   interface Vector #(SupSize, Get #(Trace_Data2)) v_to_TV;
 `endif

+`ifdef DEBUG_WEDGE
+    (* always_enabled *)
+    method Tuple2#(CapMem, Bit#(32)) hart0_last_inst;
+    (* always_enabled *)
+    method Tuple2#(CapMem, Bit#(32)) hart0_next_inst;
+`endif
+
 endinterface

 // ================================================================
--- a/src_Core/Core/CoreW.bsv
+++ b/src_Core/Core/CoreW.bsv
@@ -1,4 +1,19 @@
 // Copyright (c) 2018-2020 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package CoreW;

@@ -216,6 +231,11 @@ module mkCoreW #(Reset dm_power_on_reset)

   mkConnection (debug_module.hart0_client_run_halt, proc.hart0_run_halt_server);
   mkConnection (debug_module.hart0_get_other_req,   proc.hart0_put_other_req);
+
+`ifdef DEBUG_WEDGE
+   mkConnection (proc.hart0_last_inst, debug_module.hart0_last_inst);
+   mkConnection (proc.hart0_next_inst, debug_module.hart0_next_inst);
+`endif
 `endif

 `ifdef INCLUDE_TANDEM_VERIF
--- a/src_Core/Core/CoreW_IFC.bsv
+++ b/src_Core/Core/CoreW_IFC.bsv
@@ -1,4 +1,19 @@
 // Copyright (c) 2018-2020 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package CoreW_IFC;

--- a/src_Core/Core/Fabric_Defs.bsv
+++ b/src_Core/Core/Fabric_Defs.bsv
@@ -1,4 +1,16 @@
 // Copyright (c) 2018-2019 Bluespec, Inc. All Rights Reserved
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package Fabric_Defs;

--- a/src_Core/Core/TV_Encode.bsv
+++ b/src_Core/Core/TV_Encode.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2013-2020 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package TV_Encode;

--- a/src_Core/Core/TV_Taps.bsv
+++ b/src_Core/Core/TV_Taps.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2018-2020 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package TV_Taps;

--- a/src_Core/Core/Trace_Data2_to_Trace_Data.bsv
+++ b/src_Core/Core/Trace_Data2_to_Trace_Data.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2020 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package Trace_Data2_to_Trace_Data;

--- a/src_Core/Debug_Module/DM_Abstract_Commands.bsv
+++ b/src_Core/Debug_Module/DM_Abstract_Commands.bsv
@@ -1,4 +1,19 @@
 // Copyright (c) 2017-2019 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package DM_Abstract_Commands;

--- a/src_Core/Debug_Module/DM_Common.bsv
+++ b/src_Core/Debug_Module/DM_Common.bsv
@@ -22,7 +22,7 @@ package DM_Common;

 typedef Bit #(7)  DM_Addr;

-DM_Addr max_DM_Addr = 'h5F;
+DM_Addr max_DM_Addr = 'h7F;

 typedef Bit #(32) DM_Word;

@@ -79,6 +79,26 @@ DM_Addr dm_addr_sbdata1      = 'h3d;
 DM_Addr dm_addr_sbdata2      = 'h3e;
 DM_Addr dm_addr_sbdata3      = 'h3f;

+// ----------------
+// Custom registers
+
+DM_Addr dm_addr_custom0      = 'h70;
+DM_Addr dm_addr_custom1      = 'h71;
+DM_Addr dm_addr_custom2      = 'h72;
+DM_Addr dm_addr_custom3      = 'h73;
+DM_Addr dm_addr_custom4      = 'h74;
+DM_Addr dm_addr_custom5      = 'h75;
+DM_Addr dm_addr_custom6      = 'h76;
+DM_Addr dm_addr_custom7      = 'h77;
+DM_Addr dm_addr_custom8      = 'h78;
+DM_Addr dm_addr_custom9      = 'h79;
+DM_Addr dm_addr_custom10     = 'h7a;
+DM_Addr dm_addr_custom11     = 'h7b;
+DM_Addr dm_addr_custom12     = 'h7c;
+DM_Addr dm_addr_custom13     = 'h7d;
+DM_Addr dm_addr_custom14     = 'h7e;
+DM_Addr dm_addr_custom15     = 'h7f;
+
 // ================================================================

 function Fmt fshow_dm_addr (DM_Addr dm_addr);
--- a/src_Core/Debug_Module/DM_Run_Control.bsv
+++ b/src_Core/Debug_Module/DM_Run_Control.bsv
@@ -1,4 +1,19 @@
 // Copyright (c) 2017-2019 Bluespec, Inc. All Rights Reserved.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package DM_Run_Control;

--- a/src_Core/Debug_Module/DM_System_Bus.bsv
+++ b/src_Core/Debug_Module/DM_System_Bus.bsv
@@ -1,16 +1,18 @@
 // Copyright (c) 2017-2019 Bluespec, Inc. All Rights Reserved.
-
+//
 //-
-// AXI (user fields) modifications:
-//     Copyright (c) 2019 Alexandre Joannou
-//     Copyright (c) 2019 Peter Rugg
-//     Copyright (c) 2019 Jonathan Woodruff
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
 //     All rights reserved.
 //
 //     This software was developed by SRI International and the University of
 //     Cambridge Computer Laboratory (Department of Computer Science and
 //     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
 //     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
 //-

 package DM_System_Bus;
--- a/src_Core/Debug_Module/Debug_Module.bsv
+++ b/src_Core/Debug_Module/Debug_Module.bsv
@@ -1,16 +1,18 @@
 // Copyright (c) 2017-2019 Bluespec, Inc. All Rights Reserved.
-
+//
 //-
-// AXI (user fields) modifications:
-//     Copyright (c) 2019 Alexandre Joannou
-//     Copyright (c) 2019 Peter Rugg
-//     Copyright (c) 2019 Jonathan Woodruff
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
 //     All rights reserved.
 //
 //     This software was developed by SRI International and the University of
 //     Cambridge Computer Laboratory (Department of Computer Science and
 //     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
 //     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
 //-

 package Debug_Module;
@@ -89,6 +91,12 @@ import DM_Run_Control       :: *;
 import DM_Abstract_Commands :: *;
 import DM_System_Bus        :: *;

+`ifdef DEBUG_WEDGE
+import ConfigReg   :: *;
+import CHERICap    :: *;
+import CHERICC_Fat :: *;
+`endif
+
 // ================================================================

 export DM_Common :: *;
@@ -124,6 +132,15 @@ interface Debug_Module_IFC;
   // CSR access
   interface Client #(DM_CPU_Req #(12, XLEN), DM_CPU_Rsp #(XLEN)) hart0_csr_mem_client;

+   // Optional debug from commit stage and ROB
+`ifdef DEBUG_WEDGE
+   (* always_enabled *)
+   method Action hart0_last_inst (Tuple2 #(CapMem, Bit #(32)) pcc_inst);
+
+   (* always_enabled *)
+   method Action hart0_next_inst (Tuple2 #(CapMem, Bit #(32)) pcc_inst);
+`endif
+
   // ----------------
   // Facing Platform

@@ -152,6 +169,13 @@ module mkDebug_Module (Debug_Module_IFC);

   FIFO#(DM_Addr) f_read_addr <- mkFIFO1;

+`ifdef DEBUG_WEDGE
+   Reg #(CapMem)             rg_last_pcc          <- mkConfigReg (unpack (0));
+   Reg #(Bit #(32))          rg_last_inst         <- mkConfigReg (0);
+   Reg #(CapMem)             rg_next_pcc          <- mkConfigReg (unpack (0));
+   Reg #(Bit #(32))          rg_next_inst         <- mkConfigReg (0);
+`endif
+
   // ================================================================
   // Reset all three parts when dm_run_control.dmactive is low

@@ -226,6 +250,32 @@ module mkDebug_Module (Debug_Module_IFC);

 	    dm_word <- dm_system_bus.av_read (dm_addr);

+`ifdef DEBUG_WEDGE
+	 else if (dm_addr == dm_addr_custom0)
+
+	    dm_word = getAddr (rg_last_pcc) [31:0];
+
+	 else if (dm_addr == dm_addr_custom1)
+
+	    dm_word = getAddr (rg_last_pcc) [63:32];
+
+	 else if (dm_addr == dm_addr_custom2)
+
+	    dm_word = rg_last_inst;
+
+	 else if (dm_addr == dm_addr_custom3)
+
+	    dm_word = getAddr (rg_next_pcc) [31:0];
+
+	 else if (dm_addr == dm_addr_custom4)
+
+	    dm_word = getAddr (rg_next_pcc) [63:32];
+
+	 else if (dm_addr == dm_addr_custom5)
+
+	    dm_word = rg_next_inst;
+`endif
+
 	 else begin
 	    // TODO: set error status?
 	    dm_word = 0;
@@ -313,6 +363,19 @@ module mkDebug_Module (Debug_Module_IFC);
   // CSR access
   interface Client hart0_csr_mem_client = dm_abstract_commands.hart0_csr_mem_client;

+   // Optional debug from commit stage
+`ifdef DEBUG_WEDGE
+   method Action hart0_last_inst (Tuple2 #(CapMem, Bit #(32)) pcc_inst);
+      rg_last_pcc  <= tpl_1 (pcc_inst);
+      rg_last_inst <= tpl_2 (pcc_inst);
+   endmethod
+
+   method Action hart0_next_inst (Tuple2 #(CapMem, Bit #(32)) pcc_inst);
+      rg_next_pcc  <= tpl_1 (pcc_inst);
+      rg_next_inst <= tpl_2 (pcc_inst);
+   endmethod
+`endif
+
   // ----------------
   // Facing Platform

--- a/src_Core/ISA/ISA_Decls.bsv
+++ b/src_Core/ISA/ISA_Decls.bsv
@@ -1,4 +1,16 @@
 // Copyright (c) 2013-2020 Bluespec, Inc. All Rights Reserved
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // ================================================================
 // ISA defs for UC Berkeley RISC V
--- a/src_Core/ISA/ISA_Decls_CHERI.bsv
+++ b/src_Core/ISA/ISA_Decls_CHERI.bsv
@@ -1,11 +1,14 @@
 /*
- * Copyright (c) 2019 Peter Rugg
+ * Copyright (c) 2020 Peter Rugg
+ * Copyright (c) 2020 Jonathan Woodruff
 * All rights reserved.
- *
+
 * This software was developed by SRI International and the University of
 * Cambridge Computer Laboratory (Department of Computer Science and
 * Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
 * DARPA SSITH research programme.
+
+ * This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
 *
 * @BERI_LICENSE_HEADER_START@
 *
@@ -101,10 +104,10 @@ function SCR unpackSCR(Bit#(5) x);
    endcase);
 endfunction

-function CapPipe update_scr_via_csr (CapPipe old_scr, WordXL new_csr);
+function CapPipe update_scr_via_csr (CapPipe old_scr, WordXL new_csr, Bool allow_sealed);
    let new_scr = setOffset(old_scr, new_csr);
    let ret = new_scr.value;
-    if (!new_scr.exact || (getKind(old_scr) != UNSEALED)) begin
+    if (!new_scr.exact || (getKind(old_scr) != UNSEALED && !allow_sealed)) begin
        ret = setValidCap(ret, False);
    end
    return ret;
@@ -191,7 +194,8 @@ Bit #(5) f5rs2_cap_CClearReg   = 5'h0d;
 // 5'h0e unused
 Bit #(5) f5rs2_cap_CGetAddr    = 5'h0f;
 Bit #(5) f5rs2_cap_CClearFPReg = 5'h10;
-// 5'h11-5'h1f unused (5'h1f reserved for 1-reg instructions
+Bit #(5) f5rs2_cap_CSealEntry  = 5'h11;
+// 5'h12-5'h1f unused (5'h1f reserved for 1-reg instructions

 // ================================================================
 // f7_cap_{Load, Store} opcode subdivision
--- a/src_Core/ISA/ISA_Decls_Priv_M.bsv
+++ b/src_Core/ISA/ISA_Decls_Priv_M.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2013-2019 Bluespec, Inc. All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // ================================================================
 // This is an 'include' file, not a separate BSV package
--- a/src_Core/ISA/ISA_Decls_Priv_S.bsv
+++ b/src_Core/ISA/ISA_Decls_Priv_S.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2013-2019 Bluespec, Inc. All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // ================================================================
 // WARNING: this is an 'include' file, not a separate BSV package!
--- a/src_Core/ISA/TV_Info.bsv
+++ b/src_Core/ISA/TV_Info.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2013-2019 Bluespec, Inc. All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // ================================================================
 // Definition of Tandem Verifier Packets.
--- a/src_Core/PLIC/PLIC.bsv
+++ b/src_Core/PLIC/PLIC.bsv
@@ -1,4 +1,18 @@
 // Copyright (c) 2019-2020 Bluespec, Inc.  All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package PLIC;

--- a/src_Core/PLIC/PLIC_16_2_7.bsv
+++ b/src_Core/PLIC/PLIC_16_2_7.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2019 Bluespec, Inc.  All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package PLIC_16_2_7;

--- a/src_Core/PLIC/Test_PLIC.bsv
+++ b/src_Core/PLIC/Test_PLIC.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2019 Bluespec, Inc.  All Rights Reserved
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 package Test_PLIC;

--- a/src_Core/RISCY_OOO/coherence/src/CCPipe.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/CCPipe.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/CCTypes.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/CCTypes.bsv
@@ -1,6 +1,20 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/CrossBar.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/CrossBar.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/IBank.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/IBank.bsv
@@ -1,5 +1,18 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/ICRqMshr.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/ICRqMshr.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/IPRqMshr.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/IPRqMshr.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/L1Bank.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/L1Bank.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/L1CRqMshr.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/L1CRqMshr.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/L1PRqMshr.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/L1PRqMshr.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/L1Pipe.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/L1Pipe.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/LLBank.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/LLBank.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/LLCRqMshr.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/LLCRqMshr.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/LLPipe.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/LLPipe.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/RWBramCore.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/RWBramCore.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/RandomReplace.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/RandomReplace.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/SelfInvIBank.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/SelfInvIBank.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/SelfInvIPipe.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/SelfInvIPipe.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2019 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/SelfInvL1Bank.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/SelfInvL1Bank.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/SelfInvL1Pipe.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/SelfInvL1Pipe.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2019 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/coherence/src/SelfInvLLBank.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/SelfInvLLBank.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/coherence/src/SelfInvLLPipe.bsv
+++ b/src_Core/RISCY_OOO/coherence/src/SelfInvLLPipe.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/connectal/bsv/ConnectalBramFifo.bsv
+++ b/src_Core/RISCY_OOO/connectal/bsv/ConnectalBramFifo.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2015 Quanta Research Cambridge, Inc.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/AluExePipeline.bsv
@@ -1,6 +1,21 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/CommitStage.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/CommitStage.bsv
@@ -2,6 +2,22 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
@@ -145,6 +161,10 @@ interface CommitStage;
   method Bool is_debug_halted;
   method Action debug_resume;
 `endif
+`ifdef DEBUG_WEDGE
+    (* always_enabled *)
+    method Tuple2#(CapMem, Bit#(32)) debugLastInst;
+`endif
 endinterface

 // we apply actions the end of commit rule
@@ -604,6 +624,11 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
   endfunction
 `endif

+`ifdef DEBUG_WEDGE
+    Reg#(CapMem)   rg_last_pcc  <- mkReg(unpack(0));
+    Reg#(Bit#(32)) rg_last_inst <- mkReg(0);
+`endif
+
    // TODO Currently we don't check spec bits == 0 when we commit an
    // instruction. This is because killings of wrong path instructions are
    // done in a single cycle. However, when we make killings distributed or
@@ -763,6 +788,13 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
                    x, no_fflags, no_mstatus, tagged Valid trap_updates, no_ret_updates);
 `endif
          rg_serial_num <= rg_serial_num + 1;
+`ifdef DEBUG_WEDGE
+          Bool is_exception = trap.trap matches tagged Interrupt .i ? False : True;
+          if (is_exception) begin
+              rg_last_pcc  <= trap.pc;
+              rg_last_inst <= trap.orig_inst;
+          end
+`endif

          // system consistency
          // TODO spike flushes TLB here, but perhaps it is because spike's TLB
@@ -929,6 +961,10 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
                  x, no_fflags, new_mstatus, no_trap_updates, m_ret_updates);
 `endif
        rg_serial_num <= rg_serial_num + 1;
+`ifdef DEBUG_WEDGE
+        rg_last_pcc  <= x.pc;
+        rg_last_inst <= x.orig_inst;
+`endif

        // rename stage only sends out system inst when ROB is empty, so no
        // need to flush ROB again
@@ -1052,6 +1088,10 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
       // (whereas the 'fflags' variable does just one update after superscalar retirement).
       Bit #(5) po_fflags  = ?;
       Data     po_mstatus = ?;
+`endif
+`ifdef DEBUG_WEDGE
+        CapMem   last_pcc  = rg_last_pcc;
+        Bit#(32) last_inst = rg_last_inst;
 `endif
        // compute what actions to take
        for(Integer i = 0; i < valueof(SupSize); i = i+1) begin
@@ -1094,6 +1134,10 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
                             no_trap_updates, no_ret_updates);
 `endif
                    instret = instret + 1;
+`ifdef DEBUG_WEDGE
+                    last_pcc  = x.pc;
+                    last_inst = x.orig_inst;
+`endif

                    // inst can be committed, deq it
                    rob.deqPort[i].deq;
@@ -1147,6 +1191,10 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
            end
        end
        rg_serial_num <= rg_serial_num + instret;
+`ifdef DEBUG_WEDGE
+        rg_last_pcc  <= last_pcc;
+        rg_last_inst <= last_inst;
+`endif

        // write FPU csr
        if(csrf.fpuInstNeedWr(fflags, will_dirty_fpu_state)) begin
@@ -1265,4 +1313,10 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
   endmethod
 `endif

+`ifdef DEBUG_WEDGE
+    method Tuple2#(CapMem, Bit#(32)) debugLastInst;
+        return tuple2(rg_last_pcc, rg_last_inst);
+    endmethod
+`endif
+
 endmodule
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/FetchStage.bsv
@@ -2,6 +2,22 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/FpuMulDivExePipeline.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/FpuMulDivExePipeline.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/MemExePipeline.bsv
@@ -1,6 +1,21 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/ProcConfig.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/ProcConfig.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/RFileSynth.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/RFileSynth.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
@@ -2,6 +2,21 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/RV64G_OOO/ReservationStationMem.bsv
+++ b/src_Core/RISCY_OOO/procs/RV64G_OOO/ReservationStationMem.bsv
@@ -1,6 +1,20 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/Amo.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Amo.bsv
@@ -1,5 +1,18 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/Bht.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Bht.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/BrPred.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/BrPred.bsv
@@ -1,6 +1,20 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/Btb.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Btb.bsv
@@ -1,6 +1,20 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/Bypass.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Bypass.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/CacheUtils.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/CacheUtils.bsv
@@ -1,6 +1,20 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi
+++ b/src_Core/RISCY_OOO/procs/lib/CapChecks.bsvi
@@ -5,6 +5,7 @@
 `CAP_CHECK_FIELD(src2_sealed_with_type,"src2_sealed_with_type")
 `CAP_CHECK_FIELD(ddc_unsealed,"ddc_unsealed")
 `CAP_CHECK_FIELD(src1_unsealed,"src1_unsealed")
+`CAP_CHECK_FIELD(src1_unsealed_or_sentry,"src1_unsealed_or_sentry")
 `CAP_CHECK_FIELD(src2_unsealed,"src2_unsealed")
 `CAP_CHECK_FIELD(src1_src2_types_match,"src1_src2_types_match")
 `CAP_CHECK_FIELD(src1_permit_ccall,"src1_permit_ccall")
--- a/src_Core/RISCY_OOO/procs/lib/DTlb.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/DTlb.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/Decode.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Decode.bsv
@@ -1,6 +1,21 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
@@ -1295,6 +1310,16 @@ function DecodeResult decode(Instruction inst, Bool cap_mode);
                                    regs.src1 = Valid(tagged Gpr rs1);
                                    dInst.capFunc = CapInspect (GetAddr);
                                end
+                                f5rs2_cap_CSealEntry: begin
+                                    dInst.capChecks.src1_tag = True;
+                                    dInst.capChecks.src1_unsealed = True;
+                                    dInst.capChecks.src1_permit_x = True;
+
+                                    dInst.iType = Cap;
+                                    regs.dst = Valid(tagged Gpr rd);
+                                    regs.src1 = Valid(tagged Gpr rs1);
+                                    dInst.capFunc = CapModify (SealEntry);
+                                end
                                f5rs2_cap_CGetOffset: begin
                                    dInst.iType = Cap;
                                    regs.dst = Valid(tagged Gpr rd);
@@ -1316,7 +1341,7 @@ function DecodeResult decode(Instruction inst, Bool cap_mode);
                                f5rs2_cap_CJALR: begin
                                    dInst.capChecks.src1_tag = True;
                                    dInst.capChecks.src1_permit_x = True;
-                                    dInst.capChecks.src1_unsealed = True;
+                                    dInst.capChecks.src1_unsealed_or_sentry = True;

                                    dInst.capChecks.check_enable = True;
                                    dInst.capChecks.check_authority_src = Src1;
--- a/src_Core/RISCY_OOO/procs/lib/DirPredictor.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/DirPredictor.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/Ehr.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Ehr.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/Exec.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Exec.bsv
@@ -1,5 +1,20 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Peter Rugg
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
@@ -45,6 +60,8 @@ function Maybe#(CSR_XCapCause) capChecks(CapPipe a, CapPipe b, CapPipe ddc, CapC
        result = eDDC(SealViolation);
    else if (toCheck.src1_unsealed            && isValidCap(a) && (getKind(a) != UNSEALED))
        result = e1(SealViolation);
+    else if (toCheck.src1_unsealed_or_sentry  && isValidCap(a) && (getKind(a) != UNSEALED) && (getKind(a) != SENTRY))
+        result = e1(SealViolation);
    else if (toCheck.src2_unsealed            && isValidCap(b) && (getKind(b) != UNSEALED))
        result = e2(SealViolation);
    else if (toCheck.src1_sealed_with_type    && (getKind (a) matches tagged SEALED_WITH_TYPE .t ? False : True))
@@ -179,10 +196,10 @@ function CapPipe specialRWALU(CapPipe cap, CapPipe oldCap, SpecialRWFunc scrType
    let offset = getOffset(cap);
    let oldOffset = getOffset(oldCap);
    CapPipe res = (case (scrType) matches
-        tagged TVEC .csrf: update_scr_via_csr(oldCap, csrOp(oldOffset, getAddr(cap), csrf) & ~64'h2);
-        tagged EPC .csrf: update_scr_via_csr(oldCap, csrOp(oldOffset, getAddr(cap), csrf) & ~64'h1);
-        tagged TCC: update_scr_via_csr(cap, offset & ~64'h2); // Mask out bit 1
-        tagged EPCC: update_scr_via_csr(cap, offset & ~64'h1); // Mask out bit 0 TODO factor out update_scr_via_csr
+        tagged TVEC .csrf: update_scr_via_csr(oldCap, csrOp(oldOffset, getAddr(cap), csrf) & ~64'h2, False);
+        tagged EPC .csrf: update_scr_via_csr(oldCap, csrOp(oldOffset, getAddr(cap), csrf) & ~64'h1, False);
+        tagged TCC: update_scr_via_csr(cap, offset & ~64'h2, False); // Mask out bit 1
+        tagged EPCC: update_scr_via_csr(cap, offset & ~64'h1, offset[0] == 1'b0); // Mask out bit 0
        tagged Normal: cap;
    endcase);
    return res;
@@ -205,8 +222,13 @@ function Tuple2#(CapPipe,Bool) capModify(CapPipe a, CapPipe b, CapModifyFunc fun
                      tagged EPC ._: nullWithAddr(getOffset(b));
                   endcase);
            tagged SetAddr .addrSource    :
-                if (addrSource == Src1Type && (getKind(a) == UNSEALED)) return t(nullWithAddr(-1)); // TODO correct behaviour around reserved types
+                if      (addrSource == Src1Type && (getKind(a) == UNSEALED)) return t(nullWithAddr(otype_unsealed_ext));
+                else if (addrSource == Src1Type && (getKind(a) == SENTRY  )) return t(nullWithAddr(otype_sentry_ext));
+                else if (addrSource == Src1Type && (getKind(a) == RES0    )) return t(nullWithAddr(otype_res0_ext));
+                else if (addrSource == Src1Type && (getKind(a) == RES1    )) return t(nullWithAddr(otype_res1_ext));
                else return t(setAddr(b, (addrSource == Src1Type) ? zeroExtend(getKind(a).SEALED_WITH_TYPE) : getAddr(a) ).value);
+            tagged SealEntry              :
+                t(setKind(a, SENTRY));
            tagged Seal                   :
                t((validAsType(b, getAddr(b)) && isValidCap(b)) ?
                     setKind(a, SEALED_WITH_TYPE (truncate(getAddr(b))))
@@ -220,7 +242,7 @@ function Tuple2#(CapPipe,Bool) capModify(CapPipe a, CapPipe b, CapModifyFunc fun
            tagged FromPtr                :
                t(getAddr(a) == 0 ? nullCap : setOffset(b, getAddr(a)).value);
            tagged BuildCap               :
-                t(setKind(setValidCap(a, True),UNSEALED)); // TODO preserve sentries
+                t(setKind(setValidCap(a, True), getKind(a)==SENTRY ? SENTRY : UNSEALED));
            tagged Move                   :
                t(a);
            tagged ClearTag               :
@@ -303,6 +325,7 @@ function CapPipe brAddrCalc(CapPipe pc, CapPipe val, IType iType, Data imm, Bool
    CapPipe branchTarget = incOffset(pc, imm).value;
    CapPipe jumpTarget = incOffset(val, imm).value;
    jumpTarget = setAddrUnsafe(jumpTarget, {truncateLSB(getAddr(jumpTarget)), 1'b0});
+    jumpTarget = setKind(jumpTarget, UNSEALED); // It is checked elsewhere that we have an unsealed cap already, or sentry if permitted
    CapPipe targetAddr = (case (iType)
            J       : branchTarget;
            Jr,CCall,CJALR      : jumpTarget;
@@ -365,7 +388,7 @@ function ExecResult basicExec(DecodedInst dInst, CapPipe rVal1, CapPipe rVal2, C
    if (dInst.capChecks.cfromptr_bypass && getAddr(rVal1) == 0) begin
        capException = Invalid;
    end
-    if (dInst.capChecks.ccseal_bypass && (!isValidCap(rVal2) || getAddr(rVal2) == -1) && isValidCap(rVal1)) begin
+    if (dInst.capChecks.ccseal_bypass && (!isValidCap(rVal2) || getAddr(rVal2) == -1 || getKind(rVal1) != UNSEALED) && isValidCap(rVal1)) begin
        capException = Invalid;
        boundsCheck = Invalid;
    end
@@ -379,7 +402,7 @@ function ExecResult basicExec(DecodedInst dInst, CapPipe rVal1, CapPipe rVal2, C
            Amo         : rVal2;
            J           : nullWithAddr(getOffset(link_pcc));
            CCall       : cap_alu_result;
-            CJALR       : link_pcc;
+            CJALR       : setKind(link_pcc, SENTRY);
            Jr          : nullWithAddr(getOffset(link_pcc));
            Auipc       : nullWithAddr(getOffset(pcc) + getDInstImm(dInst).Valid);
            Auipcc      : incOffset(pcc, getDInstImm(dInst).Valid).value; // could be computed with alu
--- a/src_Core/RISCY_OOO/procs/lib/FP_Utils.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/FP_Utils.bsv
@@ -1,4 +1,17 @@
 // Copyright (c) 2019 Bluepec, Inc
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // This package implements utility functions used by the floating point
 // related logic
 package FP_Utils;
--- a/src_Core/RISCY_OOO/procs/lib/Fifos.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Fifos.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/Fpu.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/Fpu.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2016, 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/GSelectPred.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/GSelectPred.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/GSharePred.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/GSharePred.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2018 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/ITlb.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/ITlb.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/L1CoCache.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/L1CoCache.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/L2Tlb.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/LLCDmaConnect.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/LLCDmaConnect.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2017 Massachusetts Institute of Technology
 // Portions Copyright (c) 2019-2020 Bluespec, Inc.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-

 // This file is a modified version of:    RISCY_OOO/procs/lib/LLCDmaConnect.bsv
 // Bluespec: this file is has many modifications.
--- a/src_Core/RISCY_OOO/procs/lib/LLCRqMshrSecureModel.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/LLCRqMshrSecureModel.bsv
@@ -1,5 +1,19 @@

 // Copyright (c) 2019 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/LLCache.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/LLCache.bsv
@@ -1,5 +1,18 @@

 // Copyright (c) 2017 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/MMIOAddrs.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/MMIOAddrs.bsv
@@ -1,6 +1,19 @@

 // Copyright (c) 2018 Massachusetts Institute of Technology
 // Portions copyright (c) 2019-2020 Bluespec, Inc.
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/src_Core/RISCY_OOO/procs/lib/MMIOCore.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/MMIOCore.bsv
@@ -1,5 +1,19 @@
 // Copyright (c) 2018 Massachusetts Institute of Technology
 //
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Alexandre Joannou
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
+//
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
 // files (the "Software"), to deal in the Software without
--- a/src_Core/RISCY_OOO/procs/lib/MMIOInst.bsv
+++ b/src_Core/RISCY_OOO/procs/lib/MMIOInst.bsv
@@ -1,5 +1,19 @@

 // Copyright (c) 2018 Massachusetts Institute of Technology
+//
+//-
+// RVFI_DII + CHERI modifications:
+//     Copyright (c) 2020 Jessica Clarke
+//     Copyright (c) 2020 Jonathan Woodruff
+//     All rights reserved.
+//
+//     This software was developed by SRI International and the University of
+//     Cambridge Computer Laboratory (Department of Computer Science and
+//     Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
+//     DARPA SSITH research programme.
+//
+//     This work was supported by NCSC programme grant 4212611/RFA 15971 ("SafeBet").
+//-
 // 
 // Permission is hereby granted, free of charge, to any person
 // obtaining a copy of this software and associated documentation
--- a/Show More
+++ b/Show More