From a6f5bc4f0524f3a0924e0840eeb2ea5f2f26419c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 30 Sep 2016 18:18:32 +0200 Subject: Added smtbmc axicheck --- scripts/smtbmc/.gitignore | 2 + scripts/smtbmc/axicheck.sh | 12 +++ scripts/smtbmc/axicheck.v | 187 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 201 insertions(+) create mode 100644 scripts/smtbmc/axicheck.sh create mode 100644 scripts/smtbmc/axicheck.v (limited to 'scripts') diff --git a/scripts/smtbmc/.gitignore b/scripts/smtbmc/.gitignore index 24ce85b..39f1e56 100644 --- a/scripts/smtbmc/.gitignore +++ b/scripts/smtbmc/.gitignore @@ -2,6 +2,8 @@ tracecmp.smt2 tracecmp.yslog tracecmp2.smt2 tracecmp2.yslog +axicheck.smt2 +axicheck.yslog notrap_validop.smt2 notrap_validop.yslog mulcmp.smt2 diff --git a/scripts/smtbmc/axicheck.sh b/scripts/smtbmc/axicheck.sh new file mode 100644 index 0000000..55c2b05 --- /dev/null +++ b/scripts/smtbmc/axicheck.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +set -ex + +yosys -ql axicheck.yslog \ + -p 'read_verilog -formal -norestrict -assume-asserts ../../picorv32.v' \ + -p 'read_verilog -formal axicheck.v' \ + -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 + diff --git a/scripts/smtbmc/axicheck.v b/scripts/smtbmc/axicheck.v new file mode 100644 index 0000000..0afe41b --- /dev/null +++ b/scripts/smtbmc/axicheck.v @@ -0,0 +1,187 @@ +module testbench ( + input clk, + output trap, + + output mem_axi_awvalid, + input mem_axi_awready, + output [31:0] mem_axi_awaddr, + output [ 2:0] mem_axi_awprot, + + output mem_axi_wvalid, + input mem_axi_wready, + output [31:0] mem_axi_wdata, + output [ 3:0] mem_axi_wstrb, + + input mem_axi_bvalid, + output mem_axi_bready, + + output mem_axi_arvalid, + input mem_axi_arready, + output [31:0] mem_axi_araddr, + output [ 2:0] mem_axi_arprot, + + input mem_axi_rvalid, + output mem_axi_rready, + input [31:0] mem_axi_rdata +); + reg resetn = 0; + + always @(posedge clk) + resetn <= 1; + + picorv32_axi #( + .ENABLE_COUNTERS(1), + .ENABLE_COUNTERS64(1), + .ENABLE_REGS_16_31(1), + .ENABLE_REGS_DUALPORT(1), + .TWO_STAGE_SHIFT(1), + .BARREL_SHIFTER(0), + .TWO_CYCLE_COMPARE(0), + .TWO_CYCLE_ALU(0), + .COMPRESSED_ISA(0), + .CATCH_MISALIGN(1), + .CATCH_ILLINSN(1) + ) uut ( + .clk (clk ), + .resetn (resetn ), + .trap (trap ), + .mem_axi_awvalid (mem_axi_awvalid), + .mem_axi_awready (mem_axi_awready), + .mem_axi_awaddr (mem_axi_awaddr ), + .mem_axi_awprot (mem_axi_awprot ), + .mem_axi_wvalid (mem_axi_wvalid ), + .mem_axi_wready (mem_axi_wready ), + .mem_axi_wdata (mem_axi_wdata ), + .mem_axi_wstrb (mem_axi_wstrb ), + .mem_axi_bvalid (mem_axi_bvalid ), + .mem_axi_bready (mem_axi_bready ), + .mem_axi_arvalid (mem_axi_arvalid), + .mem_axi_arready (mem_axi_arready), + .mem_axi_araddr (mem_axi_araddr ), + .mem_axi_arprot (mem_axi_arprot ), + .mem_axi_rvalid (mem_axi_rvalid ), + .mem_axi_rready (mem_axi_rready ), + .mem_axi_rdata (mem_axi_rdata ) + ); + + reg expect_bvalid_0 = 0; + reg expect_bvalid_1 = 0; + reg expect_rvalid = 0; + + 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_arvalid); + assume(!mem_axi_rvalid); + end else begin + // Only one read/write transaction in flight at each point in time + + if (expect_bvalid_0) begin + assert(!mem_axi_awvalid); + end + + if (expect_bvalid_1) begin + assert(!mem_axi_wvalid); + end + + if (expect_rvalid) begin + 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); + + if (expect_bvalid_0 || expect_bvalid_1) begin + assert(!expect_rvalid); + end + + if (expect_rvalid) begin + assert(!expect_bvalid_0); + assert(!expect_bvalid_1); + end + + if (!expect_bvalid_0 || !expect_bvalid_1) begin + assume(!mem_axi_bvalid); + end + + if (!expect_rvalid) begin + assume(!mem_axi_rvalid); + end + + if (mem_axi_bvalid && mem_axi_bready) begin + expect_bvalid_0 = 0; + expect_bvalid_1 = 0; + end + + if (mem_axi_rvalid && mem_axi_rready) begin + expect_rvalid = 0; + end + + // Check AXI Master Streams + + if ($past(mem_axi_awvalid && !mem_axi_awready)) begin + assert(mem_axi_awvalid); + assert($stable(mem_axi_awaddr)); + assert($stable(mem_axi_awprot)); + end + if ($fell(mem_axi_awvalid)) begin + assert($past(mem_axi_awready)); + end + if ($fell(mem_axi_awready)) begin + assume($past(mem_axi_awvalid)); + end + + if ($past(mem_axi_arvalid && !mem_axi_arready)) begin + assert(mem_axi_arvalid); + assert($stable(mem_axi_araddr)); + assert($stable(mem_axi_arprot)); + end + if ($fell(mem_axi_arvalid)) begin + assert($past(mem_axi_arready)); + end + if ($fell(mem_axi_arready)) begin + assume($past(mem_axi_arvalid)); + end + + if ($past(mem_axi_wvalid && !mem_axi_wready)) begin + assert(mem_axi_wvalid); + assert($stable(mem_axi_wdata)); + assert($stable(mem_axi_wstrb)); + end + if ($fell(mem_axi_wvalid)) begin + assert($past(mem_axi_wready)); + end + if ($fell(mem_axi_wready)) begin + assume($past(mem_axi_wvalid)); + end + + // Check AXI Slave Streams + + if ($past(mem_axi_bvalid && !mem_axi_bready)) begin + assume(mem_axi_bvalid); + end + if ($fell(mem_axi_bvalid)) begin + assume($past(mem_axi_bready)); + end + if ($fell(mem_axi_bready)) begin + assert($past(mem_axi_bvalid)); + end + + if ($past(mem_axi_rvalid && !mem_axi_rready)) begin + assume(mem_axi_rvalid); + assume($stable(mem_axi_rdata)); + end + if ($fell(mem_axi_rvalid)) begin + assume($past(mem_axi_rready)); + end + if ($fell(mem_axi_rready)) begin + assert($past(mem_axi_rvalid)); + end + end + end + end +endmodule -- cgit