Add a fusesoc flow to dv/formal 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.

This also allows us to automatically patch the fusesoc-provided src files to work
around some current restrictions in the formal flow, without modifying the main
repository tree.

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,25 @@ 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
+	patch -p0 < patches/ibex_id_stage.diff
+
 .PHONY: sv
 sv:
 	mkdir -p build

dv/formal/README.md

@@ -5,6 +5,15 @@ Prerequisities (in your PATH):
 - [psgen](https://github.com/mndstrmr/psgen)
 
 Build instructions:
+- Clone this repository
+- `cd dv/formal`
+- `nix develop .#formal`
+- `make` invokes JasperGold in batch-mode, and attempts to prove everything. (for regressions)
+- `make jg` invokes JasperGold interactively, halting after sourcing the contents of `verify.tcl`.
+
+Building as above invokes the following steps, which can also be done manually during development:
+- `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).
 - `git submodule init`
 - `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.

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_id_stage.diff

@@ -0,0 +1,11 @@
+--- build/fusesoc/src/lowrisc_ibex_ibex_core_0.1/rtl/ibex_id_stage.sv	2024-08-25 12:37:56.787684672 +0100
++++ build/fusesoc/src/lowrisc_ibex_ibex_core_0.1/rtl/ibex_id_stage.sv	2024-08-25 12:39:23.606231887 +0100
+@@ -522,7 +522,7 @@
+     // - When modifying any PMP CSR, PMP check of the next instruction might get invalidated.
+     //   Hence, a pipeline flush is needed to instantiate another PMP check with the updated CSRs.
+     // - When modifying debug CSRs.
+-    if (csr_op_en_o == 1'b1 && (csr_op_o == CSR_OP_WRITE || csr_op_o == CSR_OP_SET)) begin
++    if (csr_op_en_o == 1'b1 && (csr_op_o == CSR_OP_WRITE || csr_op_o == CSR_OP_SET || csr_op_o == CSR_OP_CLEAR)) begin
+       if (csr_num_e'(instr_rdata_i[31:20]) == CSR_MSTATUS ||
+           csr_num_e'(instr_rdata_i[31:20]) == CSR_MIE     ||
+           csr_num_e'(instr_rdata_i[31:20]) == CSR_MSECCFG ||

dv/formal/patches/ibex_top.diff

@@ -0,0 +1,31 @@
+--- 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;
+-  localparam bit          ResetAll              = Lockstep;
++  localparam bit          ResetAll              = 1;
+   localparam bit          DummyInstructions     = SecureIbex;
+   localparam bit          RegFileECC            = SecureIbex;
+   localparam bit          RegFileWrenCheck      = SecureIbex;
+@@ -236,12 +236,13 @@
+ 
+   assign core_sleep_o = ~clock_en;
+ 
+-  prim_clock_gating core_clock_gate_i (
+-    .clk_i    (clk_i),
+-    .en_i     (clock_en),
+-    .test_en_i(test_en_i),
+-    .clk_o    (clk)
+-  );
++  assign clk = clk_i;
++  // prim_clock_gating core_clock_gate_i (
++  //   .clk_i    (clk_i),
++  //   .en_i     (clock_en),
++  //   .test_en_i(test_en_i),
++  //   .clk_o    (clk)
++  // );
+ 
+   ////////////////////////
+   // Core instantiation //

dv/formal/verify.tcl

@@ -13,44 +13,13 @@ 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
 
+analyze -sv12 spec/stub.sv
 analyze -sv12 spec/spec_api.sv
 
 # analyze -sv12 bound/binder.sv