Minor fixes/cleanups in mul reset logic

4 files changed, 107 insertions, 1 deletions

diff --git a/picorv32.v b/picorv32.v
index d4fb656..0f7ce79 100644
--- a/picorv32.v
+++ b/picorv32.v
@@ -1862,7 +1862,7 @@ module picorv32_pcpi_mul #(
 	always @(posedge clk) begin
 		pcpi_wr <= 0;
 		pcpi_ready <= 0;
-		if (mul_finish) begin
+		if (mul_finish && resetn) begin
 			pcpi_wr <= 1;
 			pcpi_ready <= 1;
 			pcpi_rd <= instr_any_mulh ? rd >> 32 : rd;
@@ -1928,6 +1928,11 @@ module picorv32_pcpi_fast_mul (
 		end
 		active2 <= active1;
 		shift_out <= instr_any_mulh;
+
+		if (!resetn) begin
+			active1 <= 0;
+			active2 <= 0;
+		end
 	end
 
 	assign pcpi_wr = active2;
diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore
index 54541e1..66e0f4c 100644
--- a/scripts/smtbmc/.gitignore
+++ b/scripts/smtbmc/.gitignore
@@ -2,5 +2,7 @@ tracecmp.smt2
 tracecmp.yslog
 notrap_validop.smt2
 notrap_validop.yslog
+mulcmp.smt2
+mulcmp.yslog
 output.vcd
 output.smtc
diff --git a/scripts/smtbmc/mulcmp.sh b/scripts/smtbmc/mulcmp.sh
new file mode 100644
index 0000000..b232ac9
--- /dev/null
+++ b/scripts/smtbmc/mulcmp.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -ex
+
+yosys -ql mulcmp.yslog \
+        -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \
+        -p 'read_verilog -formal mulcmp.v' \
+	-p 'prep -top testbench -nordff' \
+	-p 'write_smt2 -mem -bv -wires mulcmp.smt2'
+
+yosys-smtbmc -s yices -t 100 --dump-vcd output.vcd --dump-smtc output.smtc mulcmp.smt2
+
diff --git a/scripts/smtbmc/mulcmp.v b/scripts/smtbmc/mulcmp.v
new file mode 100644
index 0000000..20c47f3
--- /dev/null
+++ b/scripts/smtbmc/mulcmp.v
@@ -0,0 +1,87 @@
+module testbench(input clk, mem_ready_0, mem_ready_1);
+
+	reg resetn = 0;
+
+	always @(posedge clk)
+		resetn <= 1;
+
+	reg          pcpi_valid_0 = 1;
+	reg          pcpi_valid_1 = 1;
+
+	wire [31:0] pcpi_insn = $anyconst;
+	wire [31:0] pcpi_rs1 = $anyconst;
+	wire [31:0] pcpi_rs2 = $anyconst;
+
+	wire        pcpi_wr_0;
+	wire [31:0] pcpi_rd_0;
+	wire        pcpi_wait_0;
+	wire        pcpi_ready_0;
+
+	wire        pcpi_wr_1;
+	wire [31:0] pcpi_rd_1;
+	wire        pcpi_wait_1;
+	wire        pcpi_ready_1;
+
+	reg         pcpi_wr_ref;
+	reg  [31:0] pcpi_rd_ref;
+	reg         pcpi_ready_ref = 0;
+
+	picorv32_pcpi_mul mul_0 (
+		.clk       (clk         ),
+		.resetn    (resetn      ),
+		.pcpi_valid(pcpi_valid_0),
+		.pcpi_insn (pcpi_insn   ),
+		.pcpi_rs1  (pcpi_rs1    ),
+		.pcpi_rs2  (pcpi_rs2    ),
+		.pcpi_wr   (pcpi_wr_0   ),
+		.pcpi_rd   (pcpi_rd_0   ),
+		.pcpi_wait (pcpi_wait_0 ),
+		.pcpi_ready(pcpi_ready_0),
+
+	);
+
+	picorv32_pcpi_fast_mul mul_1 (
+		.clk       (clk         ),
+		.resetn    (resetn      ),
+		.pcpi_valid(pcpi_valid_1),
+		.pcpi_insn (pcpi_insn   ),
+		.pcpi_rs1  (pcpi_rs1    ),
+		.pcpi_rs2  (pcpi_rs2    ),
+		.pcpi_wr   (pcpi_wr_1   ),
+		.pcpi_rd   (pcpi_rd_1   ),
+		.pcpi_wait (pcpi_wait_1 ),
+		.pcpi_ready(pcpi_ready_1),
+
+	);
+
+	always @(posedge clk) begin
+		if (resetn) begin
+			if (pcpi_ready_0 && pcpi_ready_1) begin
+				assert(pcpi_wr_0 == pcpi_wr_1);
+				assert(pcpi_rd_0 == pcpi_rd_1);
+			end
+
+			if (pcpi_ready_0) begin
+				pcpi_valid_0 <= 0;
+				pcpi_wr_ref <= pcpi_wr_0;
+				pcpi_rd_ref <= pcpi_rd_0;
+				pcpi_ready_ref <= 1;
+				if (pcpi_ready_ref) begin
+					assert(pcpi_wr_0 == pcpi_wr_ref);
+					assert(pcpi_rd_0 == pcpi_rd_ref);
+				end
+			end
+
+			if (pcpi_ready_1) begin
+				pcpi_valid_1 <= 0;
+				pcpi_wr_ref <= pcpi_wr_1;
+				pcpi_rd_ref <= pcpi_rd_1;
+				pcpi_ready_ref <= 1;
+				if (pcpi_ready_ref) begin
+					assert(pcpi_wr_1 == pcpi_wr_ref);
+					assert(pcpi_rd_1 == pcpi_rd_ref);
+				end
+			end
+		end
+	end
+endmodule