diff --git a/dv/formal/Makefile b/dv/formal/Makefile index 4dec6a95..cabb5afd 100644 --- a/dv/formal/Makefile +++ b/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 diff --git a/dv/formal/README.md b/dv/formal/README.md index 16d33b71..da43e7c3 100644 --- a/dv/formal/README.md +++ b/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. diff --git a/dv/formal/ibex_formal.core b/dv/formal/ibex_formal.core new file mode 100644 index 00000000..b1958ed3 --- /dev/null +++ b/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 diff --git a/dv/formal/rtl-changes.patch b/dv/formal/patches/ibex_top.diff similarity index 76% rename from dv/formal/rtl-changes.patch rename to dv/formal/patches/ibex_top.diff index 45a5c94f..626c9028 100644 --- a/dv/formal/rtl-changes.patch +++ b/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; diff --git a/dv/formal/verify.tcl b/dv/formal/verify.tcl index d2206dbe..84f9abb4 100644 --- a/dv/formal/verify.tcl +++ b/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