diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/smtbmc/.gitignore | 2 | ||||
| -rw-r--r-- | scripts/smtbmc/mulcmp.sh | 12 | ||||
| -rw-r--r-- | scripts/smtbmc/mulcmp.v | 87 | ||||
| -rw-r--r-- | scripts/smtbmc/notrap_validop.sh | 6 | ||||
| -rw-r--r-- | scripts/smtbmc/tracecmp.sh | 2 |
5 files changed, 105 insertions, 4 deletions
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..586d72a --- /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 -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 diff --git a/scripts/smtbmc/notrap_validop.sh b/scripts/smtbmc/notrap_validop.sh index 10a7ca5..95e0f92 100644 --- a/scripts/smtbmc/notrap_validop.sh +++ b/scripts/smtbmc/notrap_validop.sh @@ -6,8 +6,8 @@ yosys -ql notrap_validop.yslog \ -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ -p 'read_verilog -formal notrap_validop.v' \ -p 'prep -top testbench -nordff' \ - -p 'write_smt2 -mem -bv -wires notrap_validop.smt2' + -p 'write_smt2 -wires notrap_validop.smt2' -#yosys-smtbmc -s yices -t 50 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2 -yosys-smtbmc -s yices -i -t 27 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2 +yosys-smtbmc -s yices -t 30 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2 +yosys-smtbmc -s yices -i -t 30 --dump-vcd output.vcd --dump-smtc output.smtc notrap_validop.smt2 diff --git a/scripts/smtbmc/tracecmp.sh b/scripts/smtbmc/tracecmp.sh index 6f471bd..449af52 100644 --- a/scripts/smtbmc/tracecmp.sh +++ b/scripts/smtbmc/tracecmp.sh @@ -6,7 +6,7 @@ yosys -ql tracecmp.yslog \ -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ -p 'read_verilog -formal tracecmp.v' \ -p 'prep -top testbench -nordff' \ - -p 'write_smt2 -mem -bv -wires tracecmp.smt2' + -p 'write_smt2 -wires tracecmp.smt2' yosys-smtbmc -s yices --smtc tracecmp.smtc --dump-vcd output.vcd --dump-smtc output.smtc tracecmp.smt2 |