diff --git a/vai_reg/Makefile b/vai_reg/Makefile
index 3b6e7ca..d90b1a6 100644
--- a/vai_reg/Makefile
+++ b/vai_reg/Makefile
@@ -1,6 +1,15 @@
-vai_reg: vai_reg.vhd symbiyosys.sby
-	sby --yosys "yosys -m ghdl" -f -d work symbiyosys.sby
+.PHONY: cover prove all clean
 
+all: cover bmc prove
+
+cover: vai_reg.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/vai_reg-$@ symbiyosys.sby $@
+
+bmc: vai_reg.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/vai_reg-$@ symbiyosys.sby $@
+
+prove: vai_reg.vhd symbiyosys.sby
+	sby --yosys "yosys -m ghdl" -f -d work/vai_reg-$@ symbiyosys.sby $@
 
 clean:
 	rm -rf work
diff --git a/vai_reg/symbiyosys.sby b/vai_reg/symbiyosys.sby
index fa2c454..b111acc 100644
--- a/vai_reg/symbiyosys.sby
+++ b/vai_reg/symbiyosys.sby
@@ -1,9 +1,18 @@
+[tasks]
+cover
+bmc
+prove
+
 [options]
-depth 30
-mode bmc
+depth 20
+cover: mode cover
+bmc: mode bmc
+prove: mode prove
 
 [engines]
-smtbmc z3
+cover: smtbmc z3
+bmc: abc bmc3
+prove: abc pdr
 
 [script]
 ghdl --std=08 -fpsl vai_reg.vhd -e vai_reg