diff --git a/.gitignore b/.gitignore
index bca5e64..66f233f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,6 +20,8 @@
 /testbench_synth.exe
 /testbench.gtkw
 /testbench.vcd
+/check.smt2
+/check.vcd
 /synth.log
 /synth.v
 .*.swp
diff --git a/Makefile b/Makefile
index b5244ce..829e2d5 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,15 @@ testbench.vcd: testbench.exe firmware/firmware.hex
 view: testbench.vcd
 	gtkwave $< testbench.gtkw
 
+check: check.smt2
+	# yosys-smtbmc -m picorv32 check.smt2
+	yosys-smtbmc -m picorv32 -t 10 -c check.vcd -i check.smt2
+
+check.smt2: picorv32.v
+	yosys -v2 -p 'read_verilog -formal picorv32.v' \
+	          -p 'prep -top picorv32 -nordff' \
+		  -p 'write_smt2 -bv -mem -wires check.smt2'
+
 test_sp: testbench_sp.exe firmware/firmware.hex
 	vvp -N testbench_sp.exe
 
@@ -69,9 +78,9 @@ toc:
 	gawk '/^-+$$/ { y=tolower(x); gsub("[^a-z0-9]+", "-", y); gsub("-$$", "", y); printf("- [%s](#%s)\n", x, y); } { x=$$0; }' README.md
 
 clean:
-	rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) \
+	rm -vrf $(FIRMWARE_OBJS) $(TEST_OBJS) check.smt2 check.vcd synth.v synth.log \
 		firmware/firmware.elf firmware/firmware.bin firmware/firmware.hex firmware/firmware.map \
-		synth.v testbench.exe testbench_sp.exe testbench_axi.exe testbench_synth.exe testbench.vcd
+		testbench.exe testbench_sp.exe testbench_axi.exe testbench_synth.exe testbench.vcd
 
 .PHONY: test view test_sp test_axi test_synth toc clean
 
diff --git a/picorv32.v b/picorv32.v
index ebe65bb..7f38a2e 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -1092,6 +1092,26 @@ module picorv32 #(
 		reg_next_pc[1:0] <= 0;
 		current_pc = 'bx;
 	end
+
+
+	// Formal Verification
+`ifdef FORMAL
+	reg [3:0] cycle = 0;
+
+	always @(posedge clk) begin
+		if (~&cycle)
+			cycle <= cycle + 1;
+	end
+
+	always @* begin
+		assume (resetn == |cycle);
+		if (cycle) begin
+			// instruction fetches are read-only
+			if (mem_valid && mem_instr)
+				assert (mem_wstrb == 0);
+		end
+	end
+`endif
 endmodule