From 44d6feba2aab35eb8fbb504e41dfba6b471a74da Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 7 Sep 2016 12:40:19 +0200
Subject: [PATCH] Using assertpmux in "make check"

---
 Makefile   |  3 ++-
 picorv32.v | 28 +++++++++++++++++++++++++++-
 2 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 347fcb8..c03792f 100644
--- a/Makefile
+++ b/Makefile
@@ -23,11 +23,12 @@ check: check-yices
 
 check-%: check.smt2
 	yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd check.smt2
-	yosys-smtbmc -s $(subst check-,,$@) -t 30 --dump-vcd check.vcd -i check.smt2
+	yosys-smtbmc -s $(subst check-,,$@) -t 20 --dump-vcd check.vcd -i check.smt2
 
 check.smt2: picorv32.v
 	yosys -v2 -p 'read_verilog -formal picorv32.v' \
 	          -p 'prep -top picorv32 -nordff' \
+		  -p 'assertpmux -noinit; opt -fast' \
 		  -p 'write_smt2 -wires check.smt2'
 
 test_sp: testbench_sp.vvp firmware/firmware.hex
diff --git a/picorv32.v b/picorv32.v
index a980e38..d457871 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -1016,6 +1016,9 @@ module picorv32 #(
 				mem_rdata_q[14:12] == 3'b101 && mem_rdata_q[31:25] == 7'b0100000
 			};
 
+			is_lui_auipc_jal_jalr_addi_add_sub <= 0;
+			is_compare <= 0;
+
 			(* parallel_case *)
 			case (1'b1)
 				instr_jal:
@@ -1032,6 +1035,29 @@ module picorv32 #(
 					decoded_imm <= 1'bx;
 			endcase
 		end
+
+		if (!resetn) begin
+			is_beq_bne_blt_bge_bltu_bgeu <= 0;
+			is_compare <= 0;
+
+			instr_addi  <= 0;
+			instr_slti  <= 0;
+			instr_sltiu <= 0;
+			instr_xori  <= 0;
+			instr_ori   <= 0;
+			instr_andi  <= 0;
+
+			instr_add   <= 0;
+			instr_sub   <= 0;
+			instr_sll   <= 0;
+			instr_slt   <= 0;
+			instr_sltu  <= 0;
+			instr_xor   <= 0;
+			instr_srl   <= 0;
+			instr_sra   <= 0;
+			instr_or    <= 0;
+			instr_and   <= 0;
+		end
 	end
 
 
@@ -1525,7 +1551,7 @@ module picorv32 #(
 							reg_op2 <= cpuregs_rs2;
 							(* parallel_case *)
 							case (1'b1)
-								is_sb_sh_sw && !instr_trap: begin
+								is_sb_sh_sw: begin
 									cpu_state <= cpu_state_stmem;
 									mem_do_rinst <= 1;
 								end