[dv,formal] Add a fusesoc flow for generating the fileset

This lets fusesoc do the heavy lifting in identify the correct files for us.
Fusesoc is already extensively used for this purpose for synthesis and simulation.

As part of this step, apply RTL patches that work around some current
restrictions in the formal flow to the /build fileset copied by fusesoc.

Co-authored-by: Gary Guo <gary.guo@lowrisc.org>
Signed-off-by: Harry Callahan <hcallahan@lowrisc.org>

dv/formal/Makefile

@@ -1,3 +1,5 @@
+IBEX_ROOT=../..
+
 SAIL=sail
 
 SAIL_RISCV_MODEL_DIR=../sail-riscv/model
@@ -16,6 +18,24 @@ SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv
 	-sv-fun2wires wX \
 	-sv-fun2wires 2:rX \
 
+# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
+# and then generate a filelist for jasper to ingest.
+# Finally, apply a number of small RTL patches necessary to make the formal flow work. (see files in patches/)
+# (Only patch the duplicated source files that fusesoc has copied into build/fusesoc/src, not the version-controlled originals)
+# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
+#   JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
+.PHONY: fusesoc
+fusesoc:
+	mkdir -p build/fusesoc
+	fusesoc \
+	  --cores-root $(IBEX_ROOT) \
+	  run \
+	  --build-root build/fusesoc \
+	  --tool vcs \
+	  --setup \
+	  lowrisc:ibex:ibex_formal:0.1
+	patch -p0 < patches/ibex_top.diff
+
 .PHONY: sv
 sv:
 	mkdir -p build

dv/formal/README.md

@@ -5,6 +5,8 @@ Prerequisities (in your PATH):
 - [psgen](https://github.com/mndstrmr/psgen)
 
 Build instructions:
+- `make fusesoc` fetches the necessary RTL using the Fusesoc tool, and makes a local copy inside `build/`. This also creates a filelist (`.scr`) that Jasper knows how to ingest.
+  - This step also patches the Ibex RTL with the changes described [in the section below](#rtl-changes).
 - `make psgen` to build the SV for the proofs given in `thm/`
 - `make sv` to build the SV translation of the Sail compiler. Will invoke `buildspec.py`, which can be configured to adjust which instructions are defined. By default all of them are, this is correct but slow.
 - Make the changes to Ibex described in the RTL changes.

dv/formal/ibex_formal.core

@@ -0,0 +1,31 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:ibex:ibex_formal:0.1"
+description: "Ibex formal module used to prove equivalence with Sail"
+
+filesets:
+  files_rtl:
+    depend:
+      - lowrisc:ibex:ibex_pkg
+      - lowrisc:ibex:ibex_core
+      - lowrisc:prim:buf
+      - lowrisc:prim:clock_gating
+      - lowrisc:prim:secded
+      - lowrisc:prim:assert
+      - lowrisc:prim:ram_1p_pkg
+      - lowrisc:prim_generic:buf
+      - lowrisc:prim_generic:clock_gating
+    files:
+      - ../../rtl/ibex_register_file_ff.sv # generic FF-based
+      - ../../rtl/ibex_register_file_fpga.sv # FPGA
+      - ../../rtl/ibex_register_file_latch.sv # ASIC
+      - ../../rtl/ibex_top.sv
+    file_type: systemVerilogSource
+
+targets:
+  default:
+    filesets:
+      - files_rtl
+    toplevel: ibex_top

dv/formal/patches/ibex_top.diff

@@ -1,8 +1,6 @@
-diff --git a/rtl/ibex_top.sv b/rtl/ibex_top.sv
-index 81e49633..17b36c17 100644
---- a/rtl/ibex_top.sv
-+++ b/rtl/ibex_top.sv
-@@ -142,7 +142,7 @@ module ibex_top import ibex_pkg::*; #(
+--- build/fusesoc/rtl/ibex_top.sv	2024-08-25 12:49:31.975238123 +0100
++++ build/fusesoc/rtl/ibex_top.sv	2024-08-25 12:51:45.786743599 +0100
+@@ -142,7 +142,7 @@
  );
  
    localparam bit          Lockstep              = SecureIbex;
@@ -11,7 +9,7 @@ index 81e49633..17b36c17 100644
    localparam bit          DummyInstructions     = SecureIbex;
    localparam bit          RegFileECC            = SecureIbex;
    localparam bit          RegFileWrenCheck      = SecureIbex;
-@@ -236,12 +236,13 @@ module ibex_top import ibex_pkg::*; #(
+@@ -236,12 +236,13 @@
  
    assign core_sleep_o = ~clock_en;
  

dv/formal/verify.tcl

@@ -13,41 +13,10 @@ set_prove_cache_mode coi
 
 set_prove_per_property_time_limit 10s
 
-set ibex_root ../../
-set sail_lib_dir $env(SAIL_DIR)/lib/sv
-set prim $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/
-set dv $ibex_root/vendor/lowrisc_ip/dv/sv/dv_utils/
-
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_alu.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_compressed_decoder.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_controller.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_cs_registers.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_decoder.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_ex_block.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_id_stage.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_if_stage.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_wb_stage.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_load_store_unit.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_multdiv_slow.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_counter.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_multdiv_fast.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_prefetch_buffer.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_fetch_fifo.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_pmp.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_core.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_csr.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_register_file_ff.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_assert.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_ram_1p_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_generic_buf.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_generic_clock_gating.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_buf.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_clock_gating.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_top.sv
+# Load all Ibex RTL, using the filelist generated by fusesoc
+analyze -sv12 +define+SYNTHESIS -f_relative_to_file_location build/fusesoc/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr
 
+set sail_lib_dir $env(LOWRISC_SAIL_SRC)/lib/sv
 analyze -sv12 -incdir $sail_lib_dir build/ibexspec.sv
 analyze -sv12 spec/stub.sv