From 2330b84b73000443c9de88104fb6c1e9e4828039 Mon Sep 17 00:00:00 2001
From: Luke Wren <wren6991@gmail.com>
Date: Sun, 30 May 2021 09:44:57 +0100
Subject: [PATCH] Use .f for riscv-formal tb dependencies, small reshuffling of
 directories

---
 .gitmodules                                                | 2 +-
 sourceme                                                   | 2 ++
 test/formal/riscv-formal                                   | 1 -
 test/formal/riscv-formal/riscv-formal                      | 1 +
 test/formal/riscv-formal/tb/hazard3_rvfi.f                 | 4 ++++
 .../formal/riscv-formal/tb}/hazard3_rvfi_monitor.vh        | 0
 .../formal/riscv-formal/tb}/hazard3_rvfi_wrapper.v         | 7 ++++++-
 7 files changed, 14 insertions(+), 3 deletions(-)
 delete mode 160000 test/formal/riscv-formal
 create mode 160000 test/formal/riscv-formal/riscv-formal
 create mode 100644 test/formal/riscv-formal/tb/hazard3_rvfi.f
 rename {hdl => test/formal/riscv-formal/tb}/hazard3_rvfi_monitor.vh (100%)
 rename {hdl => test/formal/riscv-formal/tb}/hazard3_rvfi_wrapper.v (92%)

diff --git a/.gitmodules b/.gitmodules
index a87c55f..58c58a9 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -8,5 +8,5 @@
 	path = scripts
 	url = https://github.com/Wren6991/fpgascripts
 [submodule "test/formal/riscv-formal"]
-	path = test/formal/riscv-formal
+	path = test/formal/riscv-formal/riscv-formal
 	url = https://github.com/Wren6991/riscv-formal.git
diff --git a/sourceme b/sourceme
index dc87120..94e4e76 100644
--- a/sourceme
+++ b/sourceme
@@ -1 +1,3 @@
 export PATH="$PATH:$PWD/scripts"
+export PROJ_ROOT=$PWD
+export HDL=$PROJ_ROOT/hdl
diff --git a/test/formal/riscv-formal b/test/formal/riscv-formal
deleted file mode 160000
index 7dd18d8..0000000
--- a/test/formal/riscv-formal
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 7dd18d861e76e01c6ce27adce1c9cc2f5b36e4c1
diff --git a/test/formal/riscv-formal/riscv-formal b/test/formal/riscv-formal/riscv-formal
new file mode 160000
index 0000000..8bede6c
--- /dev/null
+++ b/test/formal/riscv-formal/riscv-formal
@@ -0,0 +1 @@
+Subproject commit 8bede6ceb93ac66641bbd74a99d65a80140bc31c
diff --git a/test/formal/riscv-formal/tb/hazard3_rvfi.f b/test/formal/riscv-formal/tb/hazard3_rvfi.f
new file mode 100644
index 0000000..77a5b35
--- /dev/null
+++ b/test/formal/riscv-formal/tb/hazard3_rvfi.f
@@ -0,0 +1,4 @@
+file hazard3_rvfi_wrapper.v
+include .
+file $PROJ_ROOT/test/formal/common/ahbl_slave_assumptions.v
+list $HDL/hazard3.f
diff --git a/hdl/hazard3_rvfi_monitor.vh b/test/formal/riscv-formal/tb/hazard3_rvfi_monitor.vh
similarity index 100%
rename from hdl/hazard3_rvfi_monitor.vh
rename to test/formal/riscv-formal/tb/hazard3_rvfi_monitor.vh
diff --git a/hdl/hazard3_rvfi_wrapper.v b/test/formal/riscv-formal/tb/hazard3_rvfi_wrapper.v
similarity index 92%
rename from hdl/hazard3_rvfi_wrapper.v
rename to test/formal/riscv-formal/tb/hazard3_rvfi_wrapper.v
index fd2e6fa..5069fda 100644
--- a/hdl/hazard3_rvfi_wrapper.v
+++ b/test/formal/riscv-formal/tb/hazard3_rvfi_wrapper.v
@@ -87,7 +87,12 @@ ahbl_slave_assumptions #(
 // Device Under Test
 // ----------------------------------------------------------------------------
 
-(* keep *) `rvformal_rand_reg [15:0] irq;
+// FIXME IRQs are tied off because riscv-formal doesn't accept the
+// nonsequential pc_wdata when an instruction is followed by an interrupt
+// (and the rvfi_intr signal doesn't do anything)
+
+wire [15:0] irq = 0;
+// (* keep *) `rvformal_rand_reg [15:0] irq;
 
 hazard3_cpu_2port #(
 	.RESET_VECTOR  (0),