Add some formal cover properties for ICache

Also (and probably more interestingly) put in the tooling framework to
drive sby in the two different modes.

formal/icache/Makefile

@@ -13,13 +13,23 @@ build-root  := $(abspath ../../build/$(vlnv))
 
 fusesoc-params := --ICacheECC=$(ECC)
 
-fusesoc-run := fusesoc --cores-root=../.. run --build-root=$(build-root)
+# Since we have a hacky hook that runs sv2v in place on fusesoc's
+# copied source files, we have to generate different build roots for
+# the two flavours (otherwise bad things will happen if you run make
+# -j2)
+mk-build-root = $(abspath ../../build/$(vlnv)/$(1))
 
-.PHONY: all prove lint
-all: prove
+mk-fusesoc-cmd = \
+  fusesoc --cores-root=../.. \
+  run --build-root=$(call mk-build-root,$(1)) \
+  --target=$(1) \
+  $(core-name) $(fusesoc-params)
 
-prove:
-	$(fusesoc-run) $(core-name) $(fusesoc-params)
+.PHONY: all prove cover
+all: prove cover
+
+prove cover:
+	$(call mk-fusesoc-cmd,$@)
 
 lint:
 	mypy --strict sv2v_in_place.py

formal/icache/formal_tb.sv

@@ -131,6 +131,8 @@ module formal_tb #(
   `ASSUME(even_address, `IMPLIES(branch_i, ~addr_i[0]))
   // The branch_spec signal must be driven if branch is
   `ASSUME(gate_bs, `IMPLIES(branch_i, branch_spec_i))
+  // Ready will not be asserted when req_i is low
+  `ASSUME(ready_implies_req_i, `IMPLIES(ready_i, req_i))
 
   // Assumptions about the instruction bus
   //
@@ -222,6 +224,32 @@ module formal_tb #(
                    $past(valid_o & ~(ready_i | branch_i)) & (rdata_o[1:0] == 2'b11),
                    $stable(rdata_o[31:16])))
 
+  // Formal coverage points
+  //
+  // See a good result returned by the cache
+  `COVER(fetch_good_result, f_addr_valid & valid_o & ready_i & ~branch_i & ~err_o)
+
+  // See a bad result returned by the cache
+  `COVER(fetch_bad_result, f_addr_valid & valid_o & ready_i & ~branch_i & err_o)
+
+  // See a bad result for the upper word returned by the cache
+  `COVER(fetch_bad_result_2, f_addr_valid & valid_o & ready_i & ~branch_i & err_o & err_plus2_o)
+
+  // See 8 back-to-back fetches ("full throughput")
+  logic [31:0] f_b2b_counter;
+  always_ff @(posedge clk_i or negedge rst_ni) begin
+    if (!rst_ni) begin
+      f_b2b_counter <= 32'd0;
+    end else begin
+      if (valid_o & ready_i & ~branch_i) begin
+        f_b2b_counter <= f_b2b_counter + 32'd1;
+      end else begin
+        f_b2b_counter <= 32'd0;
+      end
+    end
+  end
+  `COVER(back_to_back_fetches, f_b2b_counter == 8);
+
   // Internal (induction) assertions
   //
   // Code below this line can refer to internal signals of the DUT. The assertions shouldn't be

formal/icache/ibex_icache_fpv.core

@@ -50,7 +50,7 @@ parameters:
     description: "Enable ECC protection in instruction cache"
 
 targets:
-  default:
+  prove: &prove
     parameters:
       - ICacheECC
     hooks:
@@ -60,3 +60,14 @@ targets:
       - all
     toplevel: ibex_icache
     default_tool: symbiyosys
+    tools:
+      symbiyosys:
+        tasknames:
+        - prove
+
+  cover:
+    <<: *prove
+    tools:
+      symbiyosys:
+        tasknames:
+        - cover

formal/icache/run.sby

@@ -2,9 +2,16 @@
 # Licensed under the Apache License, Version 2.0, see LICENSE for details.
 # SPDX-License-Identifier: Apache-2.0
 
+[tasks]
+prove pf
+cover cv
+
 [options]
-mode prove
-depth 3
+pf: mode prove
+pf: depth 3
+
+cv: mode cover
+cv: depth 32
 
 [engines]
 smtbmc boolector
@@ -12,8 +19,9 @@ smtbmc boolector
 [script]
 read -sv @INPUT@
 
-# We don't care about the exact behaviour of the memories in the
-# design, so we should blackbox them.
+# Our formal properties are currently just about control logic, which
+# isn't affected by the exact behaviour of the memories in the design.
+# Blackbox them.
 blackbox $abstract\prim_generic_ram_1p
 
 prep -top ibex_icache