From 51b1a8833353211aafe72fbcd8dadb0b71ca7d90 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 1 Oct 2016 17:08:19 +0200 Subject: [PATCH] Added smtbmc axicheck2, improved axicheck --- scripts/smtbmc/.gitignore | 2 + scripts/smtbmc/axicheck.sh | 3 +- scripts/smtbmc/axicheck.v | 61 +++++++++----- scripts/smtbmc/axicheck2.sh | 12 +++ scripts/smtbmc/axicheck2.smtc | 2 + scripts/smtbmc/axicheck2.v | 147 ++++++++++++++++++++++++++++++++++ 6 files changed, 207 insertions(+), 20 deletions(-) create mode 100644 scripts/smtbmc/axicheck2.sh create mode 100644 scripts/smtbmc/axicheck2.smtc create mode 100644 scripts/smtbmc/axicheck2.v diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore index 39f1e56..5d927c4 100644 --- a/scripts/smtbmc/.gitignore +++ b/scripts/smtbmc/.gitignore @@ -4,6 +4,8 @@ tracecmp2.smt2 tracecmp2.yslog axicheck.smt2 axicheck.yslog +axicheck2.smt2 +axicheck2.yslog notrap_validop.smt2 notrap_validop.yslog mulcmp.smt2 diff --git a/scripts/smtbmc/axicheck.sh b/scripts/smtbmc/axicheck.sh index 55c2b05..732b3b8 100644 --- a/scripts/smtbmc/axicheck.sh +++ b/scripts/smtbmc/axicheck.sh @@ -8,5 +8,6 @@ yosys -ql axicheck.yslog \ -p 'prep -top testbench -nordff' \ -p 'write_smt2 -wires axicheck.smt2' -yosys-smtbmc -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2 +yosys-smtbmc -t 50 -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2 +# yosys-smtbmc -t 50 -i -s boolector --dump-vcd output.vcd --dump-smtc output.smtc axicheck.smt2 diff --git a/scripts/smtbmc/axicheck.v b/scripts/smtbmc/axicheck.v index 0afe41b..80eda48 100644 --- a/scripts/smtbmc/axicheck.v +++ b/scripts/smtbmc/axicheck.v @@ -34,8 +34,7 @@ module testbench ( .ENABLE_COUNTERS64(1), .ENABLE_REGS_16_31(1), .ENABLE_REGS_DUALPORT(1), - .TWO_STAGE_SHIFT(1), - .BARREL_SHIFTER(0), + .BARREL_SHIFTER(1), .TWO_CYCLE_COMPARE(0), .TWO_CYCLE_ALU(0), .COMPRESSED_ISA(0), @@ -64,26 +63,50 @@ module testbench ( .mem_axi_rdata (mem_axi_rdata ) ); - reg expect_bvalid_0 = 0; - reg expect_bvalid_1 = 0; - reg expect_rvalid = 0; + reg expect_bvalid_aw = 0; + reg expect_bvalid_w = 0; + reg expect_rvalid = 0; + + reg [3:0] timeout_aw = 0; + reg [3:0] timeout_w = 0; + reg [3:0] timeout_b = 0; + reg [3:0] timeout_ar = 0; + reg [3:0] timeout_r = 0; + reg [3:0] timeout_ex = 0; + + always @(posedge clk) begin + timeout_aw <= !mem_axi_awvalid || mem_axi_awready ? 0 : timeout_aw + 1; + timeout_w <= !mem_axi_wvalid || mem_axi_wready ? 0 : timeout_w + 1; + timeout_b <= !mem_axi_bvalid || mem_axi_bready ? 0 : timeout_b + 1; + timeout_ar <= !mem_axi_arvalid || mem_axi_arready ? 0 : timeout_ar + 1; + timeout_r <= !mem_axi_rvalid || mem_axi_rready ? 0 : timeout_r + 1; + timeout_ex <= !{expect_bvalid_aw, expect_bvalid_w, expect_rvalid} ? 0 : timeout_ex + 1; + restrict(timeout_aw != 15); + restrict(timeout_w != 15); + restrict(timeout_b != 15); + restrict(timeout_ar != 15); + restrict(timeout_r != 15); + restrict(timeout_ex != 15); + restrict(!trap); + + end always @(posedge clk) begin if (resetn) begin if (!$past(resetn)) begin assert(!mem_axi_awvalid); - assert(!mem_axi_wvalid); - assume(!mem_axi_bvalid); + assert(!mem_axi_wvalid ); + assume(!mem_axi_bvalid ); assert(!mem_axi_arvalid); - assume(!mem_axi_rvalid); + assume(!mem_axi_rvalid ); end else begin // Only one read/write transaction in flight at each point in time - if (expect_bvalid_0) begin + if (expect_bvalid_aw) begin assert(!mem_axi_awvalid); end - if (expect_bvalid_1) begin + if (expect_bvalid_w) begin assert(!mem_axi_wvalid); end @@ -91,20 +114,20 @@ module testbench ( assert(!mem_axi_arvalid); end - expect_bvalid_0 = expect_bvalid_0 || (mem_axi_awvalid && mem_axi_awready); - expect_bvalid_1 = expect_bvalid_1 || (mem_axi_wvalid && mem_axi_wready); - expect_rvalid = expect_rvalid || (mem_axi_arvalid && mem_axi_arready); + expect_bvalid_aw = expect_bvalid_aw || (mem_axi_awvalid && mem_axi_awready); + expect_bvalid_w = expect_bvalid_w || (mem_axi_wvalid && mem_axi_wready ); + expect_rvalid = expect_rvalid || (mem_axi_arvalid && mem_axi_arready); - if (expect_bvalid_0 || expect_bvalid_1) begin + if (expect_bvalid_aw || expect_bvalid_w) begin assert(!expect_rvalid); end if (expect_rvalid) begin - assert(!expect_bvalid_0); - assert(!expect_bvalid_1); + assert(!expect_bvalid_aw); + assert(!expect_bvalid_w); end - if (!expect_bvalid_0 || !expect_bvalid_1) begin + if (!expect_bvalid_aw || !expect_bvalid_w) begin assume(!mem_axi_bvalid); end @@ -113,8 +136,8 @@ module testbench ( end if (mem_axi_bvalid && mem_axi_bready) begin - expect_bvalid_0 = 0; - expect_bvalid_1 = 0; + expect_bvalid_aw = 0; + expect_bvalid_w = 0; end if (mem_axi_rvalid && mem_axi_rready) begin diff --git a/scripts/smtbmc/axicheck2.sh b/scripts/smtbmc/axicheck2.sh new file mode 100644 index 0000000..df20855 --- /dev/null +++ b/scripts/smtbmc/axicheck2.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +set -ex + +yosys -ql axicheck2.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal axicheck2.v' \ + -p 'prep -top testbench -nordff' \ + -p 'write_smt2 -wires axicheck2.smt2' + +yosys-smtbmc -t 6 -s yices --dump-vcd output.vcd --dump-smtc output.smtc --smtc axicheck2.smtc axicheck2.smt2 + diff --git a/scripts/smtbmc/axicheck2.smtc b/scripts/smtbmc/axicheck2.smtc new file mode 100644 index 0000000..1f8c5ea --- /dev/null +++ b/scripts/smtbmc/axicheck2.smtc @@ -0,0 +1,2 @@ +initial +assume (= [uut_0] [uut_1]) diff --git a/scripts/smtbmc/axicheck2.v b/scripts/smtbmc/axicheck2.v new file mode 100644 index 0000000..3d24a2e --- /dev/null +++ b/scripts/smtbmc/axicheck2.v @@ -0,0 +1,147 @@ +module testbench ( + input clk, + input resetn, + output trap_0, + output trap_1, + + output mem_axi_awvalid_0, + input mem_axi_awready_0, + output [31:0] mem_axi_awaddr_0, + output [ 2:0] mem_axi_awprot_0, + + output mem_axi_awvalid_1, + input mem_axi_awready_1, + output [31:0] mem_axi_awaddr_1, + output [ 2:0] mem_axi_awprot_1, + + output mem_axi_wvalid_0, + input mem_axi_wready_0, + output [31:0] mem_axi_wdata_0, + output [ 3:0] mem_axi_wstrb_0, + + output mem_axi_wvalid_1, + input mem_axi_wready_1, + output [31:0] mem_axi_wdata_1, + output [ 3:0] mem_axi_wstrb_1, + + input mem_axi_bvalid, + output mem_axi_bready_0, + output mem_axi_bready_1, + + output mem_axi_arvalid_0, + input mem_axi_arready_0, + output [31:0] mem_axi_araddr_0, + output [ 2:0] mem_axi_arprot_0, + + output mem_axi_arvalid_1, + input mem_axi_arready_1, + output [31:0] mem_axi_araddr_1, + output [ 2:0] mem_axi_arprot_1, + + input mem_axi_rvalid, + output mem_axi_rready_0, + output mem_axi_rready_1, + input [31:0] mem_axi_rdata +); + picorv32_axi #( + .ENABLE_COUNTERS(1), + .ENABLE_COUNTERS64(1), + .ENABLE_REGS_16_31(1), + .ENABLE_REGS_DUALPORT(1), + .BARREL_SHIFTER(1), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .CATCH_MISALIGN(1), + .CATCH_ILLINSN(1) + ) uut_0 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_0 ), + .mem_axi_awvalid (mem_axi_awvalid_0), + .mem_axi_awready (mem_axi_awready_0), + .mem_axi_awaddr (mem_axi_awaddr_0 ), + .mem_axi_awprot (mem_axi_awprot_0 ), + .mem_axi_wvalid (mem_axi_wvalid_0 ), + .mem_axi_wready (mem_axi_wready_0 ), + .mem_axi_wdata (mem_axi_wdata_0 ), + .mem_axi_wstrb (mem_axi_wstrb_0 ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready_0 ), + .mem_axi_arvalid (mem_axi_arvalid_0), + .mem_axi_arready (mem_axi_arready_0), + .mem_axi_araddr (mem_axi_araddr_0 ), + .mem_axi_arprot (mem_axi_arprot_0 ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready_0 ), + .mem_axi_rdata (mem_axi_rdata ) + ); + + picorv32_axi #( + .ENABLE_COUNTERS(1), + .ENABLE_COUNTERS64(1), + .ENABLE_REGS_16_31(1), + .ENABLE_REGS_DUALPORT(1), + .BARREL_SHIFTER(1), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .CATCH_MISALIGN(1), + .CATCH_ILLINSN(1) + ) uut_1 ( + .clk (clk ), + .resetn (resetn ), + .trap (trap_1 ), + .mem_axi_awvalid (mem_axi_awvalid_1), + .mem_axi_awready (mem_axi_awready_1), + .mem_axi_awaddr (mem_axi_awaddr_1 ), + .mem_axi_awprot (mem_axi_awprot_1 ), + .mem_axi_wvalid (mem_axi_wvalid_1 ), + .mem_axi_wready (mem_axi_wready_1 ), + .mem_axi_wdata (mem_axi_wdata_1 ), + .mem_axi_wstrb (mem_axi_wstrb_1 ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready_1 ), + .mem_axi_arvalid (mem_axi_arvalid_1), + .mem_axi_arready (mem_axi_arready_1), + .mem_axi_araddr (mem_axi_araddr_1 ), + .mem_axi_arprot (mem_axi_arprot_1 ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready_1 ), + .mem_axi_rdata (mem_axi_rdata ) + ); + + always @(posedge clk) begin + if (resetn && $past(resetn)) begin + assert(trap_0 == trap_1 ); + assert(mem_axi_awvalid_0 == mem_axi_awvalid_1); + assert(mem_axi_awaddr_0 == mem_axi_awaddr_1 ); + assert(mem_axi_awprot_0 == mem_axi_awprot_1 ); + assert(mem_axi_wvalid_0 == mem_axi_wvalid_1 ); + assert(mem_axi_wdata_0 == mem_axi_wdata_1 ); + assert(mem_axi_wstrb_0 == mem_axi_wstrb_1 ); + assert(mem_axi_bready_0 == mem_axi_bready_1 ); + assert(mem_axi_arvalid_0 == mem_axi_arvalid_1); + assert(mem_axi_araddr_0 == mem_axi_araddr_1 ); + assert(mem_axi_arprot_0 == mem_axi_arprot_1 ); + assert(mem_axi_rready_0 == mem_axi_rready_1 ); + + if (mem_axi_awvalid_0) assume(mem_axi_awready_0 == mem_axi_awready_1); + if (mem_axi_wvalid_0 ) assume(mem_axi_wready_0 == mem_axi_wready_1 ); + if (mem_axi_arvalid_0) assume(mem_axi_arready_0 == mem_axi_arready_1); + + if ($fell(mem_axi_awready_0)) assume($past(mem_axi_awvalid_0)); + if ($fell(mem_axi_wready_0 )) assume($past(mem_axi_wvalid_0 )); + if ($fell(mem_axi_arready_0)) assume($past(mem_axi_arvalid_0)); + + if ($fell(mem_axi_awready_1)) assume($past(mem_axi_awvalid_1)); + if ($fell(mem_axi_wready_1 )) assume($past(mem_axi_wvalid_1 )); + if ($fell(mem_axi_arready_1)) assume($past(mem_axi_arvalid_1)); + + if ($fell(mem_axi_bvalid)) assume($past(mem_axi_bready_0)); + if ($fell(mem_axi_rvalid)) assume($past(mem_axi_rready_0)); + + if (mem_axi_rvalid && $past(mem_axi_rvalid)) assume($stable(mem_axi_rdata)); + end + end +endmodule