From bc47b9126031ed572c4c78ae42ce739451a9aa80 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 16 Nov 2016 16:42:00 +0100 Subject: [PATCH] Added tracecmp3 smtbmc script --- scripts/smtbmc/.gitignore | 4 ++ scripts/smtbmc/tracecmp3.sh | 17 +++++ scripts/smtbmc/tracecmp3.v | 131 ++++++++++++++++++++++++++++++++++++ 3 files changed, 152 insertions(+) create mode 100644 scripts/smtbmc/tracecmp3.sh create mode 100644 scripts/smtbmc/tracecmp3.v diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore index 5d927c4..1ce906e 100644 --- a/scripts/smtbmc/.gitignore +++ b/scripts/smtbmc/.gitignore @@ -2,6 +2,10 @@ tracecmp.smt2 tracecmp.yslog tracecmp2.smt2 tracecmp2.yslog +tracecmp3.blif +tracecmp3.cex +tracecmp3.smt2 +tracecmp3.yslog axicheck.smt2 axicheck.yslog axicheck2.smt2 diff --git a/scripts/smtbmc/tracecmp3.sh b/scripts/smtbmc/tracecmp3.sh new file mode 100644 index 0000000..bfa0b3c --- /dev/null +++ b/scripts/smtbmc/tracecmp3.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +set -ex + +yosys -l tracecmp3.yslog \ + -p 'read_verilog ../../picorv32.v' \ + -p 'read_verilog -formal tracecmp3.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires tracecmp3.smt2' \ + -p 'miter -assert -flatten testbench miter' \ + -p 'hierarchy -top miter; memory_map; opt -full' \ + -p 'techmap; opt; abc; opt -fast' \ + -p 'write_blif tracecmp3.blif' + +yosys-abc -c 'read_blif tracecmp3.blif; undc; strash; zero; sim3 -v; undc -c; write_cex -n tracecmp3.cex' +yosys-smtbmc -s yices --cex tracecmp3.cex --dump-vcd output.vcd --dump-smtc output.smtc tracecmp3.smt2 + diff --git a/scripts/smtbmc/tracecmp3.v b/scripts/smtbmc/tracecmp3.v new file mode 100644 index 0000000..ac9968c --- /dev/null +++ b/scripts/smtbmc/tracecmp3.v @@ -0,0 +1,131 @@ +// Based on the benchmark from 2016 Yosys-SMTBMC presentation, which in turn is +// based on the tracecmp2 test from this directory. + +module testbench ( + input clk, + input [31:0] mem_rdata_in, + + input pcpi_wr, + input [31:0] pcpi_rd, + input pcpi_wait, + input pcpi_ready +); + reg resetn = 0; + + always @(posedge clk) + resetn <= 1; + + wire cpu0_mem_valid; + wire cpu0_mem_instr; + wire cpu0_mem_ready; + wire [31:0] cpu0_mem_addr; + wire [31:0] cpu0_mem_wdata; + wire [3:0] cpu0_mem_wstrb; + wire [31:0] cpu0_mem_rdata; + wire cpu0_trace_valid; + wire [35:0] cpu0_trace_data; + + wire cpu1_mem_valid; + wire cpu1_mem_instr; + wire cpu1_mem_ready; + wire [31:0] cpu1_mem_addr; + wire [31:0] cpu1_mem_wdata; + wire [3:0] cpu1_mem_wstrb; + wire [31:0] cpu1_mem_rdata; + wire cpu1_trace_valid; + wire [35:0] cpu1_trace_data; + + wire mem_ready; + wire [31:0] mem_rdata; + + assign mem_ready = cpu0_mem_valid && cpu1_mem_valid; + assign mem_rdata = mem_rdata_in; + + assign cpu0_mem_ready = mem_ready; + assign cpu0_mem_rdata = mem_rdata; + + assign cpu1_mem_ready = mem_ready; + assign cpu1_mem_rdata = mem_rdata; + + reg [ 2:0] trace_balance = 3'b010; + reg [35:0] trace_buffer_cpu0 = 0, trace_buffer_cpu1 = 0; + + always @(posedge clk) begin + if (resetn) begin + if (cpu0_trace_valid) + trace_buffer_cpu0 <= cpu0_trace_data; + + if (cpu1_trace_valid) + trace_buffer_cpu1 <= cpu1_trace_data; + + if (cpu0_trace_valid && !cpu1_trace_valid) + trace_balance <= trace_balance << 1; + + if (!cpu0_trace_valid && cpu1_trace_valid) + trace_balance <= trace_balance >> 1; + end + end + + always @* begin + if (resetn && cpu0_mem_ready) begin + assert(cpu0_mem_addr == cpu1_mem_addr); + assert(cpu0_mem_wstrb == cpu1_mem_wstrb); + if (cpu0_mem_wstrb[3]) assert(cpu0_mem_wdata[31:24] == cpu1_mem_wdata[31:24]); + if (cpu0_mem_wstrb[2]) assert(cpu0_mem_wdata[23:16] == cpu1_mem_wdata[23:16]); + if (cpu0_mem_wstrb[1]) assert(cpu0_mem_wdata[15: 8] == cpu1_mem_wdata[15: 8]); + if (cpu0_mem_wstrb[0]) assert(cpu0_mem_wdata[ 7: 0] == cpu1_mem_wdata[ 7: 0]); + end + if (trace_balance == 3'b010) begin + assert(trace_buffer_cpu0 == trace_buffer_cpu1); + end + end + + picorv32 #( + .ENABLE_COUNTERS(0), + .REGS_INIT_ZERO(1), + .COMPRESSED_ISA(1), + .ENABLE_TRACE(1), + + .TWO_STAGE_SHIFT(0), + .ENABLE_PCPI(1) + ) cpu0 ( + .clk (clk ), + .resetn (resetn ), + .mem_valid (cpu0_mem_valid ), + .mem_instr (cpu0_mem_instr ), + .mem_ready (cpu0_mem_ready ), + .mem_addr (cpu0_mem_addr ), + .mem_wdata (cpu0_mem_wdata ), + .mem_wstrb (cpu0_mem_wstrb ), + .mem_rdata (cpu0_mem_rdata ), + .pcpi_wr (pcpi_wr ), + .pcpi_rd (pcpi_rd ), + .pcpi_wait (pcpi_wait ), + .pcpi_ready (pcpi_ready ), + .trace_valid (cpu0_trace_valid), + .trace_data (cpu0_trace_data ) + ); + + picorv32 #( + .ENABLE_COUNTERS(0), + .REGS_INIT_ZERO(1), + .COMPRESSED_ISA(1), + .ENABLE_TRACE(1), + + .TWO_STAGE_SHIFT(1), + .TWO_CYCLE_COMPARE(1), + .TWO_CYCLE_ALU(1) + ) cpu1 ( + .clk (clk ), + .resetn (resetn ), + .mem_valid (cpu1_mem_valid ), + .mem_instr (cpu1_mem_instr ), + .mem_ready (cpu1_mem_ready ), + .mem_addr (cpu1_mem_addr ), + .mem_wdata (cpu1_mem_wdata ), + .mem_wstrb (cpu1_mem_wstrb ), + .mem_rdata (cpu1_mem_rdata ), + .trace_valid (cpu1_trace_valid), + .trace_data (cpu1_trace_data ) + ); +endmodule