picorv32/scripts/smtbmc/axicheck.v

211 lines
5.4 KiB
Verilog

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