From cefe09b8d41285d3ece4ab0efcfe6aea1a259cd8 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 30 Aug 2016 11:12:16 +0200 Subject: [PATCH] Minor fixes/cleanups in mul reset logic --- picorv32.v | 7 +++- scripts/smtbmc/.gitignore | 2 + scripts/smtbmc/mulcmp.sh | 12 ++++++ scripts/smtbmc/mulcmp.v | 87 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 scripts/smtbmc/mulcmp.sh create mode 100644 scripts/smtbmc/mulcmp.v 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