diff options
Diffstat (limited to 'picorv32/scripts/smtbmc/axicheck.v')
| -rw-r--r-- | picorv32/scripts/smtbmc/axicheck.v | 210 |
1 files changed, 0 insertions, 210 deletions
diff --git a/picorv32/scripts/smtbmc/axicheck.v b/picorv32/scripts/smtbmc/axicheck.v deleted file mode 100644 index 80eda48..0000000 --- a/picorv32/scripts/smtbmc/axicheck.v +++ /dev/null @@ -1,210 +0,0 @@ -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), - .BARREL_SHIFTER(1), - .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_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_arvalid); - assume(!mem_axi_rvalid ); - end else begin - // Only one read/write transaction in flight at each point in time - - if (expect_bvalid_aw) begin - assert(!mem_axi_awvalid); - end - - if (expect_bvalid_w) begin - assert(!mem_axi_wvalid); - end - - if (expect_rvalid) begin - assert(!mem_axi_arvalid); - end - - 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_aw || expect_bvalid_w) begin - assert(!expect_rvalid); - end - - if (expect_rvalid) begin - assert(!expect_bvalid_aw); - assert(!expect_bvalid_w); - end - - if (!expect_bvalid_aw || !expect_bvalid_w) 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_aw = 0; - expect_bvalid_w = 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 |