| 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 |