diff --git a/formal/icache/Makefile b/formal/icache/Makefile
index 423c401b..92068fa2 100644
--- a/formal/icache/Makefile
+++ b/formal/icache/Makefile
@@ -4,17 +4,22 @@
 
 # A simple wrapper around fusesoc to make it a bit easier to run the formal flow
 
+# Whether to use ECC (0 for disabled; 1 for enabled)
+ECC := 0
+
 core-name   := lowrisc:fpv:ibex_icache_fpv
 vlnv        := $(subst :,_,$(core-name))
 build-root  := $(abspath ../../build/$(vlnv))
 
-fusesoc-run := cd ../..; fusesoc --cores-root=. run
+fusesoc-params := --ICacheECC=$(ECC)
+
+fusesoc-run := fusesoc --cores-root=../.. run --build-root=$(build-root)
 
 .PHONY: all prove lint
 all: prove
 
 prove:
-	fusesoc --cores-root=../.. run --build-root=$(build-root) $(core-name)
+	$(fusesoc-run) $(core-name) $(fusesoc-params)
 
 lint:
 	mypy --strict sv2v_in_place.py
diff --git a/formal/icache/ibex_icache_fpv.core b/formal/icache/ibex_icache_fpv.core
index b61cacd2..276e0642 100644
--- a/formal/icache/ibex_icache_fpv.core
+++ b/formal/icache/ibex_icache_fpv.core
@@ -51,10 +51,12 @@ parameters:
 
 targets:
   default:
+    parameters:
+      - ICacheECC
     hooks:
       pre_build:
         - sv2v_in_place
     filesets:
       - all
-    toplevel: tb
+    toplevel: ibex_icache
     default_tool: symbiyosys