| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: axil2apb.v |
| // {{{ |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: High throughput AXI-lite bridge to APB. With both skid |
| // buffers enabled, it can handle 50% throughput--the maximum |
| // that APB can handle. |
| // |
| // 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 axil2apb #( |
| // {{{ |
| parameter C_AXI_ADDR_WIDTH = 32, |
| parameter C_AXI_DATA_WIDTH = 32, |
| // OPT_OUTGOING_SKIDBUFFER: required for 50% throughput |
| parameter [0:0] OPT_OUTGOING_SKIDBUFFER = 1'b0, |
| localparam AW = C_AXI_ADDR_WIDTH, |
| localparam DW = C_AXI_DATA_WIDTH, |
| localparam AXILLSB = $clog2(C_AXI_DATA_WIDTH)-3 |
| // }}} |
| ) ( |
| // {{{ |
| input wire S_AXI_ACLK, |
| input wire S_AXI_ARESETN, |
| // |
| // The AXI-lite interface |
| // {{{ |
| 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 reg S_AXI_BVALID, |
| input wire S_AXI_BREADY, |
| output reg [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 reg S_AXI_RVALID, |
| input wire S_AXI_RREADY, |
| output reg [C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA, |
| output reg [1:0] S_AXI_RRESP, |
| // }}} |
| // |
| // The APB interface |
| // {{{ |
| output reg M_APB_PSEL, |
| output reg M_APB_PENABLE, |
| input wire M_APB_PREADY, |
| output reg [C_AXI_ADDR_WIDTH-1:0] M_APB_PADDR, |
| output reg M_APB_PWRITE, |
| output reg [C_AXI_DATA_WIDTH-1:0] M_APB_PWDATA, |
| output reg [C_AXI_DATA_WIDTH/8-1:0] M_APB_PWSTRB, |
| output reg [2:0] M_APB_PPROT, |
| input wire [C_AXI_DATA_WIDTH-1:0] M_APB_PRDATA, |
| input wire M_APB_PSLVERR |
| // }}} |
| // }}} |
| ); |
| |
| // Register declarations |
| // {{{ |
| wire awskd_valid, wskd_valid, arskd_valid; |
| reg axil_write_ready, axil_read_ready, |
| write_grant, apb_idle; |
| wire [AW-AXILLSB-1:0] awskd_addr, arskd_addr; |
| wire [DW-1:0] wskd_data; |
| wire [DW/8-1:0] wskd_strb; |
| wire [2:0] awskd_prot, arskd_prot; |
| reg apb_bvalid, apb_rvalid, apb_error, out_skid_full; |
| reg [DW-1:0] apb_data; |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Incoming AXI-lite write interface |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // awskd - write address skid buffer |
| // {{{ |
| skidbuffer #(.DW(C_AXI_ADDR_WIDTH-AXILLSB + 3), |
| .OPT_OUTREG(0) |
| ) awskd (.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), |
| .i_valid(S_AXI_AWVALID), .o_ready(S_AXI_AWREADY), |
| .i_data({ S_AXI_AWADDR[AW-1:AXILLSB], S_AXI_AWPROT }), |
| .o_valid(awskd_valid), .i_ready(axil_write_ready), |
| .o_data({ awskd_addr, awskd_prot })); |
| // }}} |
| |
| // wskd - write data skid buffer |
| // {{{ |
| skidbuffer #(.DW(DW+(DW/8)), |
| .OPT_OUTREG(0) |
| ) wskd (.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), |
| .i_valid(S_AXI_WVALID), .o_ready(S_AXI_WREADY), |
| .i_data({ S_AXI_WDATA, S_AXI_WSTRB }), |
| .o_valid(wskd_valid), .i_ready(axil_write_ready), |
| .o_data({ wskd_data, wskd_strb })); |
| // }}} |
| |
| // apb_idle |
| // {{{ |
| always @(*) |
| begin |
| apb_idle = !M_APB_PSEL;// || (M_APB_PENABLE && M_APB_PREADY); |
| if (OPT_OUTGOING_SKIDBUFFER && (M_APB_PENABLE && M_APB_PREADY)) |
| apb_idle = 1'b1; |
| end |
| // }}} |
| |
| // axil_write_ready |
| // {{{ |
| always @(*) |
| begin |
| axil_write_ready = apb_idle; |
| if (S_AXI_BVALID && !S_AXI_BREADY) |
| axil_write_ready = 1'b0; |
| if (!awskd_valid || !wskd_valid) |
| axil_write_ready = 1'b0; |
| if (!write_grant && arskd_valid) |
| axil_write_ready = 1'b0; |
| end |
| // }}} |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Incoming AXI-lite read interface |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // arskd buffer |
| // {{{ |
| skidbuffer #(.DW(C_AXI_ADDR_WIDTH-AXILLSB+3), |
| .OPT_OUTREG(0) |
| ) arskd (.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN), |
| .i_valid(S_AXI_ARVALID), .o_ready(S_AXI_ARREADY), |
| .i_data({ S_AXI_ARADDR[AW-1:AXILLSB], S_AXI_ARPROT }), |
| .o_valid(arskd_valid), .i_ready(axil_read_ready), |
| .o_data({ arskd_addr, arskd_prot })); |
| // }}} |
| |
| // axil_read_ready |
| // {{{ |
| always @(*) |
| begin |
| axil_read_ready = apb_idle; |
| if (S_AXI_RVALID && !S_AXI_RREADY) |
| axil_read_ready = 1'b0; |
| if (write_grant && awskd_valid && wskd_valid) |
| axil_read_ready = 1'b0; |
| if (!arskd_valid) |
| axil_read_ready = 1'b0; |
| end |
| // }}} |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Arbitrate among reads and writes --- alternating arbitration |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // write_grant -- alternates |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if (apb_idle) |
| begin |
| if (axil_write_ready) |
| write_grant <= 1'b0; |
| else if (axil_read_ready) |
| write_grant <= 1'b1; |
| end |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Drive the APB bus |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // APB bus |
| // {{{ |
| initial M_APB_PSEL = 1'b0; |
| initial M_APB_PENABLE = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (apb_idle) |
| begin |
| M_APB_PSEL <= 1'b0; |
| if (axil_read_ready) |
| begin |
| M_APB_PSEL <= 1'b1; |
| M_APB_PADDR <= { arskd_addr, {(AXILLSB){1'b0}} }; |
| M_APB_PWRITE <= 1'b0; |
| M_APB_PPROT <= arskd_prot; |
| end else if (axil_write_ready) |
| begin |
| M_APB_PSEL <= 1'b1; |
| M_APB_PADDR <= { awskd_addr, {(AXILLSB){1'b0}} }; |
| M_APB_PWRITE <= 1'b1; |
| M_APB_PPROT <= awskd_prot; |
| end |
| |
| if (wskd_valid) |
| begin |
| M_APB_PWDATA <= wskd_data; |
| M_APB_PWSTRB <= wskd_strb; |
| end |
| |
| M_APB_PENABLE <= 1'b0; |
| end else if (!M_APB_PENABLE) |
| M_APB_PENABLE <= 1'b1; |
| else if (M_APB_PREADY) |
| begin // if (M_APB_PSEL && M_APB_ENABLE) |
| M_APB_PENABLE <= 1'b0; |
| M_APB_PSEL <= 1'b0; |
| end |
| |
| if (!S_AXI_ARESETN) |
| begin |
| M_APB_PSEL <= 1'b0; |
| M_APB_PENABLE <= 1'b0; |
| end |
| end |
| // }}} |
| |
| reg r_apb_bvalid, r_apb_rvalid, r_apb_error; |
| reg [DW-1:0] r_apb_data; |
| |
| generate if (OPT_OUTGOING_SKIDBUFFER) |
| begin |
| // {{{ |
| // r_apb_bvalid, r_apb_rvalid, r_apb_error, r_apb_data |
| // {{{ |
| initial r_apb_bvalid = 1'b0; |
| initial r_apb_rvalid = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| begin |
| if (M_APB_PSEL && M_APB_PENABLE && M_APB_PREADY) |
| begin |
| r_apb_bvalid <= (S_AXI_BVALID && !S_AXI_BREADY) && M_APB_PWRITE; |
| r_apb_rvalid <= (S_AXI_RVALID && !S_AXI_RREADY) && !M_APB_PWRITE; |
| if (!M_APB_PWRITE) |
| r_apb_data <= M_APB_PRDATA; |
| r_apb_error <= M_APB_PSLVERR; |
| end else begin |
| if (S_AXI_BREADY) |
| r_apb_bvalid <= 1'b0; |
| if (S_AXI_RREADY) |
| r_apb_rvalid <= 1'b0; |
| end |
| |
| if (!S_AXI_ARESETN) |
| begin |
| r_apb_bvalid <= 1'b0; |
| r_apb_rvalid <= 1'b0; |
| end |
| end |
| // }}} |
| |
| // apb_bvalid |
| // {{{ |
| always @(*) |
| apb_bvalid = (M_APB_PSEL && M_APB_PENABLE |
| && M_APB_PREADY && M_APB_PWRITE)|| r_apb_bvalid; |
| // }}} |
| |
| // apb_bvalid |
| // {{{ |
| always @(*) |
| apb_rvalid = (M_APB_PSEL && M_APB_PENABLE |
| && M_APB_PREADY && !M_APB_PWRITE)||r_apb_rvalid; |
| // }}} |
| |
| // apb_data |
| // {{{ |
| always @(*) |
| if (out_skid_full) |
| apb_data = r_apb_data; |
| else |
| apb_data = M_APB_PRDATA; |
| // }}} |
| |
| // apb_error |
| // {{{ |
| always @(*) |
| if (out_skid_full) |
| apb_error = r_apb_error; |
| else |
| apb_error = M_APB_PSLVERR; |
| // }}} |
| |
| always @(*) |
| out_skid_full = r_apb_bvalid || r_apb_rvalid; |
| // }}} |
| end else begin |
| // {{{ |
| always @(*) |
| r_apb_bvalid = 1'b0; |
| |
| always @(*) |
| r_apb_rvalid = 1'b0; |
| |
| always @(*) |
| r_apb_error = 1'b0; |
| |
| always @(*) |
| r_apb_data = 0; |
| |
| always @(*) |
| apb_bvalid = M_APB_PSEL && M_APB_PENABLE |
| && M_APB_PREADY && M_APB_PWRITE; |
| always @(*) |
| apb_rvalid = M_APB_PSEL && M_APB_PENABLE |
| && M_APB_PREADY && !M_APB_PWRITE; |
| always @(*) |
| apb_data = M_APB_PRDATA; |
| always @(*) |
| apb_error = M_APB_PSLVERR; |
| |
| always @(*) |
| out_skid_full = 1'b0; |
| |
| // Verilator lint_off UNUSED |
| wire skd_unused; |
| assign skd_unused = &{ 1'b0, r_apb_bvalid, r_apb_rvalid, |
| r_apb_data, r_apb_error, out_skid_full }; |
| // Verilator lint_on UNUSED |
| // }}} |
| end endgenerate |
| |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI-lite write return signaling |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // BVALID |
| // {{{ |
| initial S_AXI_BVALID = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_BVALID <= 1'b0; |
| else if (!S_AXI_BVALID || S_AXI_BREADY) |
| S_AXI_BVALID <= apb_bvalid; |
| // }}} |
| |
| // BRESP |
| // {{{ |
| initial S_AXI_BRESP = 2'b00; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_BRESP <= 2'b00; |
| else if (!S_AXI_BVALID || S_AXI_BREADY) |
| S_AXI_BRESP <= { apb_error, 1'b0 }; |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI-lite read return signaling |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| |
| // RVALID |
| // {{{ |
| initial S_AXI_RVALID = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_RVALID <= 1'b0; |
| else if (!S_AXI_RVALID || S_AXI_RREADY) |
| S_AXI_RVALID <= apb_rvalid; |
| // }}} |
| |
| // RRESP |
| // {{{ |
| initial S_AXI_RRESP = 2'b00; |
| always @(posedge S_AXI_ACLK) |
| if (!S_AXI_ARESETN) |
| S_AXI_RRESP <= 2'b00; |
| else if (!S_AXI_RVALID || S_AXI_RREADY) |
| S_AXI_RRESP <= { apb_error, 1'b0 }; |
| // }}} |
| |
| // RDATA |
| // {{{ |
| always @(posedge S_AXI_ACLK) |
| if ((!S_AXI_RVALID || S_AXI_RREADY) && apb_rvalid) |
| S_AXI_RDATA <= apb_data; |
| // }}} |
| |
| // }}} |
| |
| // Make Verilator happy |
| // {{{ |
| // Verilator lint_off UNUSED |
| wire unused; |
| assign unused = &{ 1'b0, S_AXI_AWPROT, S_AXI_ARPROT, |
| S_AXI_AWADDR[AXILLSB-1:0], S_AXI_ARADDR[AXILLSB-1:0] |
| }; |
| // Verilator lint_on UNUSED |
| // }}} |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Formal properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| `ifdef FORMAL |
| localparam F_LGDEPTH = 3; |
| |
| wire [F_LGDEPTH-1:0] faxi_rd_outstanding, |
| faxi_wr_outstanding, |
| faxi_awr_outstanding; |
| reg f_past_valid; |
| |
| initial f_past_valid = 1'b0; |
| always @(posedge S_AXI_ACLK) |
| f_past_valid <= 1'b1; |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // AXI-lite interface properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| faxil_slave #( |
| // {{{ |
| .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH), |
| .C_AXI_DATA_WIDTH (C_AXI_DATA_WIDTH), |
| .F_OPT_COVER_BURST(4), |
| .F_AXI_MAXWAIT(17), |
| .F_AXI_MAXDELAY(17), |
| .F_AXI_MAXRSTALL(3), |
| .F_LGDEPTH(F_LGDEPTH) |
| // }}} |
| ) faxil ( |
| // {{{ |
| .i_clk(S_AXI_ACLK), // System clock |
| .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_awprot(S_AXI_AWPROT), |
| .i_axi_awcache(4'h0), |
| // |
| .i_axi_wready(S_AXI_WREADY), |
| .i_axi_wdata(S_AXI_WDATA), |
| .i_axi_wstrb(S_AXI_WSTRB), |
| .i_axi_wvalid(S_AXI_WVALID), |
| // |
| .i_axi_bresp(S_AXI_BRESP), |
| .i_axi_bvalid(S_AXI_BVALID), |
| .i_axi_bready(S_AXI_BREADY), |
| // |
| .i_axi_arvalid(S_AXI_ARVALID), |
| .i_axi_arready(S_AXI_ARREADY), |
| .i_axi_araddr(S_AXI_ARADDR), |
| .i_axi_arprot(S_AXI_ARPROT), |
| .i_axi_arcache(4'h0), |
| // |
| .i_axi_rvalid(S_AXI_RVALID), |
| .i_axi_rready(S_AXI_RREADY), |
| .i_axi_rresp(S_AXI_RRESP), |
| .i_axi_rdata(S_AXI_RDATA), |
| // |
| .f_axi_rd_outstanding(faxi_rd_outstanding), |
| .f_axi_wr_outstanding(faxi_wr_outstanding), |
| .f_axi_awr_outstanding(faxi_awr_outstanding) |
| // }}} |
| ); |
| |
| // Correlate outstanding counters against our state |
| // {{{ |
| always @(*) |
| if (S_AXI_ARESETN) |
| begin |
| assert(faxi_awr_outstanding == (S_AXI_AWREADY ? 0:1) |
| + (r_apb_bvalid ? 1:0) |
| + (S_AXI_BVALID ? 1:0) |
| + ((M_APB_PSEL && M_APB_PWRITE) ? 1:0)); |
| |
| assert(faxi_wr_outstanding == (S_AXI_WREADY ? 0:1) |
| + (r_apb_bvalid ? 1:0) |
| + (S_AXI_BVALID ? 1:0) |
| + ((M_APB_PSEL && M_APB_PWRITE) ? 1:0)); |
| |
| assert(faxi_rd_outstanding == (S_AXI_ARREADY ? 0:1) |
| + (r_apb_rvalid ? 1:0) |
| + (S_AXI_RVALID ? 1:0) |
| + ((M_APB_PSEL && !M_APB_PWRITE) ? 1:0)); |
| |
| if (r_apb_bvalid) |
| assert(S_AXI_BVALID); |
| if (r_apb_rvalid) |
| assert(S_AXI_RVALID); |
| end |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // APB interface properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| fapb_master #( |
| // {{{ |
| .AW(C_AXI_ADDR_WIDTH), |
| .DW(C_AXI_DATA_WIDTH), |
| .F_OPT_MAXSTALL(3) |
| // }}} |
| ) fapb ( |
| // {{{ |
| .PCLK(S_AXI_ACLK), .PRESETn(S_AXI_ARESETN), |
| .PSEL( M_APB_PSEL), |
| .PENABLE(M_APB_PENABLE), |
| .PREADY( M_APB_PREADY), |
| .PADDR( M_APB_PADDR), |
| .PWRITE( M_APB_PWRITE), |
| .PWDATA( M_APB_PWDATA), |
| .PWSTRB( M_APB_PWSTRB), |
| .PPROT( M_APB_PPROT), |
| .PRDATA( M_APB_PRDATA), |
| .PSLVERR(M_APB_PSLVERR) |
| // }}} |
| ); |
| |
| always @(*) |
| if (!M_APB_PSEL) |
| assert(!M_APB_PENABLE); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Induction invariants |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| always @(*) |
| assert(!axil_write_ready || !axil_read_ready); |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Contract properties |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| (* anyconst *) reg f_never_test; |
| (* anyconst *) reg [AW-1:0] f_never_addr; |
| (* anyconst *) reg [DW-1:0] f_never_data; |
| (* anyconst *) reg [DW/8-1:0] f_never_strb; |
| (* anyconst *) reg [2:0] f_never_prot; |
| |
| // Assume the never values are never received |
| // {{{ |
| always @(*) |
| if (f_never_test) |
| begin |
| assume(f_never_addr[AXILLSB-1:0] == 0); |
| |
| if (S_AXI_AWVALID) |
| begin |
| assume(S_AXI_AWADDR[AW-1:AXILLSB] != f_never_addr[AW-1:AXILLSB]); |
| assume(S_AXI_AWPROT != f_never_prot); |
| end |
| |
| if (S_AXI_WVALID) |
| begin |
| assume(S_AXI_WDATA != f_never_data); |
| assume(S_AXI_WSTRB != f_never_strb); |
| end |
| |
| if (S_AXI_ARVALID) |
| begin |
| assume(S_AXI_ARADDR[AW-1:AXILLSB] != f_never_addr[AW-1:AXILLSB]); |
| assume(S_AXI_ARPROT != f_never_prot); |
| end |
| |
| if (M_APB_PSEL && M_APB_PENABLE && M_APB_PREADY&& !M_APB_PWRITE) |
| assume(M_APB_PRDATA != f_never_data); |
| end |
| // }}} |
| |
| // Assert the never values are never in the incoming skid buffers |
| // {{{ |
| always @(*) |
| if (f_never_test) |
| begin |
| if (awskd_valid) |
| begin |
| assert(awskd_addr != f_never_addr[AW-1:AXILLSB]); |
| assert(awskd_prot != f_never_prot); |
| end |
| |
| if (wskd_valid) |
| begin |
| assert(wskd_data != f_never_data); |
| assert(wskd_strb != f_never_strb); |
| end |
| |
| if (arskd_valid) |
| begin |
| assert(arskd_addr != f_never_addr[AW-1:AXILLSB]); |
| assert(arskd_prot != f_never_prot); |
| end |
| |
| if (r_apb_rvalid) |
| assert(r_apb_data != f_never_data); |
| end |
| // }}} |
| |
| // Assert the never values are never output |
| // {{{ |
| always @(*) |
| if (f_never_test) |
| begin |
| if (M_APB_PSEL) |
| begin |
| assert(M_APB_PADDR != f_never_addr); |
| assert(M_APB_PPROT != f_never_prot); |
| if (M_APB_PWRITE) |
| begin |
| assert(M_APB_PWDATA != f_never_data); |
| assert(M_APB_PWSTRB != f_never_strb); |
| end |
| end |
| |
| if (S_AXI_RVALID) |
| assert(S_AXI_RDATA != f_never_data); |
| end |
| // }}} |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Cover checks |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // None (yet) |
| |
| // }}} |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Careless assumptions |
| // {{{ |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // |
| |
| // }}} |
| `endif |
| // }}} |
| endmodule |