| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: easyaxil |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: A formal miter core to compare the easyaxil core to a similar |
| // (but mutated) core. |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // Copyright (C) 2020, Gisselquist Technology, LLC |
| // {{{ |
| // |
| // This file is part of the WB2AXIP project. |
| // |
| // The WB2AXIP project contains free software and gateware, licensed under the |
| // Apache License, Version 2.0 (the "License"). You may not use this project, |
| // or this file, except in compliance with the License. You may obtain a copy |
| // of the License at |
| // |
| // http://www.apache.org/licenses/LICENSE-2.0 |
| // |
| // Unless required by applicable law or agreed to in writing, software |
| // distributed under the License is distributed on an "AS IS" BASIS, WITHOUT |
| // WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the |
| // License for the specific language governing permissions and limitations |
| // under the License. |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // }}} |
| // |
| `default_nettype none |
| // |
| module easyaxil_tb #( |
| // {{{ |
| // |
| // Size of the AXI-lite bus. These are fixed, since 1) AXI-lite |
| // is fixed at a width of 32-bits by Xilinx def'n, and 2) since |
| // we only ever have 4 configuration words. |
| parameter C_AXI_ADDR_WIDTH = 4, |
| localparam C_AXI_DATA_WIDTH = 32, |
| parameter [0:0] OPT_SKIDBUFFER = 1'b0, |
| parameter [0:0] OPT_LOWPOWER = 0 |
| // }}} |
| ) ( |
| // {{{ |
| input wire S_AXI_ACLK, |
| input wire S_AXI_ARESETN, |
| // |
| input wire S_AXI_AWVALID, |
| output wire S_AXI_AWREADY, |
| input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_AWADDR, |
| input wire [2:0] S_AXI_AWPROT, |
| // |
| input wire S_AXI_WVALID, |
| output wire S_AXI_WREADY, |
| input wire [C_AXI_DATA_WIDTH-1:0] S_AXI_WDATA, |
| input wire [C_AXI_DATA_WIDTH/8-1:0] S_AXI_WSTRB, |
| // |
| output wire S_AXI_BVALID, |
| input wire S_AXI_BREADY, |
| output wire [1:0] S_AXI_BRESP, |
| // |
| input wire S_AXI_ARVALID, |
| output wire S_AXI_ARREADY, |
| input wire [C_AXI_ADDR_WIDTH-1:0] S_AXI_ARADDR, |
| input wire [2:0] S_AXI_ARPROT, |
| // |
| output wire S_AXI_RVALID, |
| input wire S_AXI_RREADY, |
| output wire [C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA, |
| output wire [1:0] S_AXI_RRESP, |
| // }}} |
| input wire [7:0] mutation_index |
| ); |
| |
| easyaxil // #(.C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), |
| // .OPT_SKIDBUFFER(OPT_SKIDBUFFER), |
| // .OPT_LOWPOWER(OPT_LOWPOWER) |
| // ) |
| gold ( |
| .S_AXI_ACLK( S_AXI_ACLK), |
| .S_AXI_ARESETN(S_AXI_ARESETN), |
| // |
| .S_AXI_AWVALID(S_AXI_AWVALID), |
| .S_AXI_AWREADY(S_AXI_AWREADY), |
| .S_AXI_AWADDR( S_AXI_AWADDR), |
| .S_AXI_AWPROT( S_AXI_AWPROT), |
| // |
| .S_AXI_WVALID( S_AXI_WVALID), |
| .S_AXI_WREADY( S_AXI_WREADY), |
| .S_AXI_WDATA( S_AXI_WDATA), |
| .S_AXI_WSTRB( S_AXI_WSTRB), |
| // |
| .S_AXI_BVALID( S_AXI_BVALID), |
| .S_AXI_BREADY( S_AXI_BREADY), |
| .S_AXI_BRESP( S_AXI_BRESP), |
| // |
| .S_AXI_ARVALID(S_AXI_ARVALID), |
| .S_AXI_ARREADY(S_AXI_ARREADY), |
| .S_AXI_ARADDR( S_AXI_ARADDR), |
| .S_AXI_ARPROT( S_AXI_ARPROT), |
| // |
| .S_AXI_RVALID(S_AXI_RVALID), |
| .S_AXI_RREADY(S_AXI_RREADY), |
| .S_AXI_RDATA( S_AXI_RDATA), |
| .S_AXI_RRESP( S_AXI_RRESP), |
| .mutsel(0) |
| ); |
| |
| wire uut_AWREADY, uut_WREADY, uut_BVALID, uut_ARREADY, uut_RVALID; |
| wire [1:0] uut_BRESP, uut_RRESP; |
| wire [31:0] uut_RDATA; |
| |
| easyaxil // #( |
| // .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), |
| // .OPT_SKIDBUFFER(OPT_SKIDBUFFER), |
| // .OPT_LOWPOWER(OPT_LOWPOWER) |
| // ) |
| uut ( |
| .S_AXI_ACLK( S_AXI_ACLK), |
| .S_AXI_ARESETN(S_AXI_ARESETN), |
| // |
| .S_AXI_AWVALID(S_AXI_AWVALID), |
| .S_AXI_AWREADY(uut_AWREADY), |
| .S_AXI_AWADDR( S_AXI_AWADDR), |
| .S_AXI_AWPROT( S_AXI_AWPROT), |
| // |
| .S_AXI_WVALID( S_AXI_WVALID), |
| .S_AXI_WREADY( uut_WREADY), |
| .S_AXI_WDATA( S_AXI_WDATA), |
| .S_AXI_WSTRB( S_AXI_WSTRB), |
| // |
| .S_AXI_BVALID( uut_BVALID), |
| .S_AXI_BREADY( S_AXI_BREADY), |
| .S_AXI_BRESP( uut_BRESP), |
| // |
| .S_AXI_ARVALID(S_AXI_ARVALID), |
| .S_AXI_ARREADY(uut_ARREADY), |
| .S_AXI_ARADDR( S_AXI_ARADDR), |
| .S_AXI_ARPROT( S_AXI_ARPROT), |
| // |
| .S_AXI_RVALID(uut_RVALID), |
| .S_AXI_RREADY(S_AXI_RREADY), |
| .S_AXI_RDATA( uut_RDATA), |
| .S_AXI_RRESP( uut_RRESP), |
| .mutsel(mutation_index) |
| ); |
| |
| `ifdef FORMAL |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties used in verfiying this core |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| reg f_past_valid; |
| initial f_past_valid = 0; |
| always @(posedge S_AXI_ACLK) |
| f_past_valid <= 1; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // The AXI-lite control interface |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // {{{ |
| localparam F_AXIL_LGDEPTH = 4; |
| wire [F_AXIL_LGDEPTH-1:0] faxil_rd_outstanding, |
| faxil_wr_outstanding, |
| faxil_awr_outstanding; |
| |
| faxil_slave #( |
| // {{{ |
| .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH), |
| .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), |
| .F_LGDEPTH(F_AXIL_LGDEPTH), |
| .F_AXI_MAXWAIT(2), |
| .F_AXI_MAXDELAY(2), |
| .F_AXI_MAXRSTALL(3), |
| .F_OPT_COVER_BURST(4) |
| // }}} |
| ) faxil( |
| // {{{ |
| .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), |
| // |
| .i_axi_awvalid(S_AXI_AWVALID), |
| .i_axi_awready(S_AXI_AWREADY), |
| .i_axi_awaddr( S_AXI_AWADDR), |
| .i_axi_awcache(4'h0), |
| .i_axi_awprot( S_AXI_AWPROT), |
| // |
| .i_axi_wvalid(S_AXI_WVALID), |
| .i_axi_wready(S_AXI_WREADY), |
| .i_axi_wdata( S_AXI_WDATA), |
| .i_axi_wstrb( S_AXI_WSTRB), |
| // |
| .i_axi_bvalid(S_AXI_BVALID), |
| .i_axi_bready(S_AXI_BREADY), |
| .i_axi_bresp( S_AXI_BRESP), |
| // |
| .i_axi_arvalid(S_AXI_ARVALID), |
| .i_axi_arready(S_AXI_ARREADY), |
| .i_axi_araddr( S_AXI_ARADDR), |
| .i_axi_arcache(4'h0), |
| .i_axi_arprot( S_AXI_ARPROT), |
| // |
| .i_axi_rvalid(S_AXI_RVALID), |
| .i_axi_rready(S_AXI_RREADY), |
| .i_axi_rdata( S_AXI_RDATA), |
| .i_axi_rresp( S_AXI_RRESP), |
| // |
| .f_axi_rd_outstanding(faxil_rd_outstanding), |
| .f_axi_wr_outstanding(faxil_wr_outstanding), |
| .f_axi_awr_outstanding(faxil_awr_outstanding) |
| // }}} |
| ); |
| |
| always @(*) |
| if (S_AXI_ARESETN) |
| begin |
| if (S_AXI_AWVALID) |
| assert(S_AXI_AWREADY == uut_AWREADY); |
| |
| if (S_AXI_WVALID) |
| assert(S_AXI_WREADY == uut_WREADY); |
| |
| if (S_AXI_ARVALID) |
| assert(S_AXI_ARREADY == uut_ARREADY); |
| |
| assert(S_AXI_BVALID == uut_BVALID); |
| assert(S_AXI_RVALID == uut_RVALID); |
| |
| if (S_AXI_BVALID) |
| assert( S_AXI_BRESP == uut_BRESP ); |
| |
| if (S_AXI_RVALID) |
| assert({ S_AXI_RRESP, S_AXI_RDATA } |
| == { uut_RRESP, uut_RDATA }); |
| end |
| |
| // }}} |
| // }}} |
| `endif |
| endmodule |
