Google Git
Sign in
foss-eda-tools / third_party / shuttle / sky130 / mpw-001 / slot-003 / 2ca0eb0565b960278b3c1e7a112f4a570aa036e1 / . / verilog / rtl / softshell / third_party / wb2axip / rtl / axilxbar.v
blob: 0e158b808d5c9d8fe6c9f2de8e4e7d800ef974c1 [file] [log] [blame]
////////////////////////////////////////////////////////////////////////////////
//
// Filename: axilxbar.v
//
// Project: WB2AXIPSP: bus bridges and other odds and ends
//
// Purpose: Create a full crossbar between NM AXI-lite sources (masters),
// and NS AXI-lite slaves. Every master can talk to any slave,
// provided it isn't already busy.
//
// Performance: This core has been designed with the goal of being able to push
// one transaction through the interconnect, from any master to
// any slave, per clock cycle. This may perhaps be its most unique
// feature. While throughput is good, latency is something else.
//
// The arbiter requires a clock to switch, then another clock to send data
// downstream. This creates a minimum two clock latency up front. The
// return path suffers another clock of latency as well, placing the
// minimum latency at four clocks. The minimum write latency is at
// least one clock longer, since the write data must wait for the write
// address before proceeeding.
//
// Usage: To use, you must first set NM and NS to the number of masters
// and the number of slaves you wish to connect to. You then need to
// adjust the addresses of the slaves, found SLAVE_ADDR array. Those
// bits that are relevant in SLAVE_ADDR to then also be set in SLAVE_MASK.
// Adjusting the data and address widths go without saying.
//
// Lower numbered masters are given priority in any "fight".
//
// Channel grants are given on the condition that 1) they are requested,
// 2) no other channel has a grant, 3) all of the responses have been
// received from the current channel, and 4) the internal counters are
// not overflowing.
//
// The core limits the number of outstanding transactions on any channel to
// 1<<LGMAXBURST-1.
//
// Channel grants are lost 1) after OPT_LINGER clocks of being idle, or
// 2) when another master requests an idle (but still lingering) channel
// assignment, or 3) once all the responses have been returned to the
// current channel, and the current master is requesting another channel.
//
// A special slave is allocated for the case of no valid address.
//
// Since the write channel has no address information, the write data
// channel always be delayed by at least one clock from the write address
// channel.
//
// If OPT_LOWPOWER is set, then unused values will be set to zero.
// This can also be used to help identify relevant values within any
// trace.
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2019-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 axilxbar #(
parameter integer C_AXI_DATA_WIDTH = 32,
parameter integer C_AXI_ADDR_WIDTH = 32,
//
// NM is the number of master interfaces this core supports
parameter NM = 4,
//
// NS is the number of slave interfaces
parameter NS = 8,
//
// AW, and DW, are short-hand abbreviations used locally.
localparam AW = C_AXI_ADDR_WIDTH,
localparam DW = C_AXI_DATA_WIDTH,
// SLAVE_ADDR is a bit vector containing AW bits for each of the
// slaves indicating the base address of the slave. This
// goes with SLAVE_MASK below.
parameter [NS*AW-1:0] SLAVE_ADDR = {
3'b111, {(AW-3){1'b0}},
3'b110, {(AW-3){1'b0}},
3'b101, {(AW-3){1'b0}},
3'b100, {(AW-3){1'b0}},
3'b011, {(AW-3){1'b0}},
3'b010, {(AW-3){1'b0}},
4'b0001, {(AW-4){1'b0}},
4'b0000, {(AW-4){1'b0}} },
//
// SLAVE_MASK indicates which bits in the SLAVE_ADDR bit vector
// need to be checked to determine if a given address request
// maps to the given slave or not
// Verilator lint_off WIDTH
parameter [NS*AW-1:0] SLAVE_MASK =
(NS <= 1) ? { 4'b1111, {(AW-4){1'b0}}}
: { {(NS-2){ 3'b111, {(AW-3){1'b0}} }},
{(2){ 4'b1111, {(AW-4){1'b0}}}} },
// Verilator lint_on WIDTH
//
// If set, OPT_LOWPOWER will set all unused registers, both
// internal and external, to zero anytime their corresponding
// *VALID bit is clear
parameter [0:0] OPT_LOWPOWER = 1,
//
// OPT_LINGER is the number of cycles to wait, following a
// transaction, before tearing down the bus grant.
parameter OPT_LINGER = 4,
//
// LGMAXBURST is the log (base two) of the maximum number of
// requests that can be outstanding on any given channel at any
// given time. It is used within this core to control the
// counters that are used to determine if a particular channel
// grant must stay open, or if it may be closed.
parameter LGMAXBURST = 5
) (
input wire S_AXI_ACLK,
input wire S_AXI_ARESETN,
//
input wire [NM*C_AXI_ADDR_WIDTH-1:0] S_AXI_AWADDR,
input wire [NM*3-1:0] S_AXI_AWPROT,
input wire [NM-1:0] S_AXI_AWVALID,
output wire [NM-1:0] S_AXI_AWREADY,
//
input wire [NM*C_AXI_DATA_WIDTH-1:0] S_AXI_WDATA,
input wire [NM*C_AXI_DATA_WIDTH/8-1:0] S_AXI_WSTRB,
input wire [NM-1:0] S_AXI_WVALID,
output wire [NM-1:0] S_AXI_WREADY,
//
output wire [NM*2-1:0] S_AXI_BRESP,
output wire [NM-1:0] S_AXI_BVALID,
input wire [NM-1:0] S_AXI_BREADY,
//
input wire [NM*C_AXI_ADDR_WIDTH-1:0] S_AXI_ARADDR,
input wire [NM*3-1:0] S_AXI_ARPROT,
input wire [NM-1:0] S_AXI_ARVALID,
output wire [NM-1:0] S_AXI_ARREADY,
//
output wire [NM*C_AXI_DATA_WIDTH-1:0] S_AXI_RDATA,
output wire [NM*2-1:0] S_AXI_RRESP,
output wire [NM-1:0] S_AXI_RVALID,
input wire [NM-1:0] S_AXI_RREADY,
//
//
//
output wire [NS*C_AXI_ADDR_WIDTH-1:0] M_AXI_AWADDR,
output wire [NS*3-1:0] M_AXI_AWPROT,
output wire [NS-1:0] M_AXI_AWVALID,
input wire [NS-1:0] M_AXI_AWREADY,
//
output wire [NS*C_AXI_DATA_WIDTH-1:0] M_AXI_WDATA,
output wire [NS*C_AXI_DATA_WIDTH/8-1:0] M_AXI_WSTRB,
output wire [NS-1:0] M_AXI_WVALID,
input wire [NS-1:0] M_AXI_WREADY,
//
input wire [NS*2-1:0] M_AXI_BRESP,
input wire [NS-1:0] M_AXI_BVALID,
output wire [NS-1:0] M_AXI_BREADY,
//
output wire [NS*C_AXI_ADDR_WIDTH-1:0] M_AXI_ARADDR,
output wire [NS*3-1:0] M_AXI_ARPROT,
output wire [NS-1:0] M_AXI_ARVALID,
input wire [NS-1:0] M_AXI_ARREADY,
//
input wire [NS*C_AXI_DATA_WIDTH-1:0] M_AXI_RDATA,
input wire [NS*2-1:0] M_AXI_RRESP,
input wire [NS-1:0] M_AXI_RVALID,
output wire [NS-1:0] M_AXI_RREADY
);
//
// Local parameters, derived from those above
localparam LGLINGER = (OPT_LINGER>1) ? $clog2(OPT_LINGER+1) : 1;
//
localparam LGNM = (NM>1) ? $clog2(NM) : 1;
localparam LGNS = (NS>1) ? $clog2(NS+1) : 1;
//
// In order to use indexes, and hence fully balanced mux trees, it helps
// to make certain that we have a power of two based lookup. NMFULL
// is the number of masters in this lookup, with potentially some
// unused extra ones. NSFULL is defined similarly.
localparam NMFULL = (NM>1) ? (1<<LGNM) : 1;
localparam NSFULL = (NS>1) ? (1<<LGNS) : 2;
//
localparam [1:0] INTERCONNECT_ERROR = 2'b11;
localparam [0:0] OPT_SKID_INPUT = 0;
localparam [0:0] OPT_BUFFER_DECODER = 1;
genvar N,M;
integer iN, iM;
reg [NSFULL-1:0] wrequest [0:NM-1];
reg [NSFULL-1:0] rrequest [0:NM-1];
reg [NSFULL-1:0] wrequested [0:NM];
reg [NSFULL-1:0] rrequested [0:NM];
reg [NS:0] wgrant [0:NM-1];
reg [NS:0] rgrant [0:NM-1];
reg [NM-1:0] swgrant;
reg [NM-1:0] srgrant;
reg [NS-1:0] mwgrant;
reg [NS-1:0] mrgrant;
// verilator lint_off UNUSED
wire [LGMAXBURST-1:0] w_sawpending [0:NM-1];
wire [LGMAXBURST-1:0] w_swpending [0:NM-1];
wire [LGMAXBURST-1:0] w_srpending [0:NM-1];
// verilator lint_on UNUSED
reg [NM-1:0] swfull;
reg [NM-1:0] srfull;
reg [NM-1:0] swempty;
reg [NM-1:0] srempty;
//
reg [LGNS-1:0] swindex [0:NMFULL-1];
reg [LGNS-1:0] srindex [0:NMFULL-1];
reg [LGNM-1:0] mwindex [0:NSFULL-1];
reg [LGNM-1:0] mrindex [0:NSFULL-1];
(* keep *) reg [NM-1:0] wdata_expected;
// The shadow buffers
reg [NMFULL-1:0] m_awvalid, m_wvalid, m_arvalid;
wire [NM-1:0] dcd_awvalid, dcd_arvalid;
wire [C_AXI_ADDR_WIDTH-1:0] m_awaddr [0:NMFULL-1];
wire [2:0] m_awprot [0:NMFULL-1];
wire [C_AXI_DATA_WIDTH-1:0] m_wdata [0:NMFULL-1];
wire [C_AXI_DATA_WIDTH/8-1:0] m_wstrb [0:NMFULL-1];
wire [C_AXI_ADDR_WIDTH-1:0] m_araddr [0:NMFULL-1];
wire [2:0] m_arprot [0:NMFULL-1];
//
wire [NM-1:0] skd_awvalid, skd_awstall, skd_wvalid;
wire [NM-1:0] skd_arvalid, skd_arstall;
wire [AW-1:0] skd_awaddr [0:NM-1];
wire [3-1:0] skd_awprot [0:NM-1];
wire [AW-1:0] skd_araddr [0:NM-1];
wire [3-1:0] skd_arprot [0:NM-1];
reg [NSFULL-1:0] m_axi_awvalid;
reg [NSFULL-1:0] m_axi_awready;
reg [NSFULL-1:0] m_axi_wvalid;
reg [NSFULL-1:0] m_axi_wready;
reg [NSFULL-1:0] m_axi_bvalid;
`ifdef FORMAL
reg [NSFULL-1:0] m_axi_bready;
`endif
reg [1:0] m_axi_bresp [0:NSFULL-1];
reg [NSFULL-1:0] m_axi_arvalid;
// Verilator lint_off UNUSED
reg [NSFULL-1:0] m_axi_arready;
// Verilator lint_on UNUSED
reg [NSFULL-1:0] m_axi_rvalid;
// Verilator lint_off UNUSED
reg [NSFULL-1:0] m_axi_rready;
// Verilator lint_on UNUSED
reg [DW-1:0] m_axi_rdata [0:NSFULL-1];
reg [1:0] m_axi_rresp [0:NSFULL-1];
reg [NM-1:0] slave_awaccepts;
reg [NM-1:0] slave_waccepts;
reg [NM-1:0] slave_raccepts;
always @(*)
begin
m_axi_awvalid = -1;
m_axi_awready = -1;
m_axi_wvalid = -1;
m_axi_wready = -1;
m_axi_bvalid = 0;
m_axi_awvalid[NS-1:0] = M_AXI_AWVALID;
m_axi_awready[NS-1:0] = M_AXI_AWREADY;
m_axi_wvalid[NS-1:0] = M_AXI_WVALID;
m_axi_wready[NS-1:0] = M_AXI_WREADY;
m_axi_bvalid[NS-1:0] = M_AXI_BVALID;
for(iM=0; iM<NS; iM=iM+1)
begin
m_axi_bresp[iM] = M_AXI_BRESP[iM* 2 +: 2];
m_axi_rdata[iM] = M_AXI_RDATA[iM*DW +: DW];
m_axi_rresp[iM] = M_AXI_RRESP[iM* 2 +: 2];
end
for(iM=NS; iM<NSFULL; iM=iM+1)
begin
m_axi_bresp[iM] = INTERCONNECT_ERROR;
m_axi_rdata[iM] = 0;
m_axi_rresp[iM] = INTERCONNECT_ERROR;
end
`ifdef FORMAL
m_axi_bready = -1;
m_axi_bready[NS-1:0] = M_AXI_BREADY;
`endif
end
generate for(N=0; N<NM; N=N+1)
begin : DECODE_WRITE_REQUEST
wire [NS:0] wdecode;
skidbuffer #(.DW(AW+3), .OPT_OUTREG(OPT_SKID_INPUT))
awskid(S_AXI_ACLK, !S_AXI_ARESETN,
S_AXI_AWVALID[N], S_AXI_AWREADY[N],
{ S_AXI_AWADDR[N*AW +: AW], S_AXI_AWPROT[N*3 +: 3] },
skd_awvalid[N], !skd_awstall[N],
{ skd_awaddr[N], skd_awprot[N] });
addrdecode #(.AW(AW), .DW(3), .NS(NS),
.SLAVE_ADDR(SLAVE_ADDR),
.SLAVE_MASK(SLAVE_MASK),
.OPT_REGISTERED(OPT_BUFFER_DECODER))
wraddr(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
.i_valid(skd_awvalid[N]), .o_stall(skd_awstall[N]),
.i_addr(skd_awaddr[N]), .i_data(skd_awprot[N]),
.o_valid(dcd_awvalid[N]),
.i_stall(!dcd_awvalid[N]||!slave_awaccepts[N]),
.o_decode(wdecode), .o_addr(m_awaddr[N]),
.o_data(m_awprot[N]));
skidbuffer #(.DW(DW+DW/8), .OPT_OUTREG(OPT_SKID_INPUT))
wskid(S_AXI_ACLK, !S_AXI_ARESETN,
S_AXI_WVALID[N], S_AXI_WREADY[N],
{ S_AXI_WDATA[N*DW +: DW], S_AXI_WSTRB[N*DW/8 +: DW/8]},
skd_wvalid[N], (m_wvalid[N] && slave_waccepts[N]),
{ m_wdata[N], m_wstrb[N] });
always @(*)
begin
slave_awaccepts[N] = 1'b1;
if (!swgrant[N])
slave_awaccepts[N] = 1'b0;
if (swfull[N])
slave_awaccepts[N] = 1'b0;
if (!wrequest[N][swindex[N]])
slave_awaccepts[N] = 1'b0;
if (!wgrant[N][NS]&&(m_axi_awvalid[swindex[N]] && !m_axi_awready[swindex[N]]))
slave_awaccepts[N] = 1'b0;
// ERRORs are always accepted
// back pressure is handled in the write side
end
always @(*)
begin
slave_waccepts[N] = 1'b1;
if (!swgrant[N])
slave_waccepts[N] = 1'b0;
if (!wdata_expected[N])
slave_waccepts[N] = 1'b0;
if (!wgrant[N][NS] &&(m_axi_wvalid[swindex[N]]
&& !m_axi_wready[swindex[N]]))
slave_waccepts[N] = 1'b0;
if (wgrant[N][NS]&&(S_AXI_BVALID[N]&& !S_AXI_BREADY[N]))
slave_waccepts[N] = 1'b0;
end
always @(*)
begin
m_awvalid[N]= dcd_awvalid[N] && !swfull[N];
m_wvalid[N] = skd_wvalid[N];
wrequest[N]= 0;
if (!swfull[N])
wrequest[N][NS:0] = wdecode;
end
`ifdef FORMAL
always @(*)
if (skd_awvalid[N])
assert(skd_awprot[N] == 0);
`endif
end for (N=NM; N<NMFULL; N=N+1)
begin : UNUSED_WSKID_BUFFERS
always @(*)
m_awvalid[N] = 0;
assign m_awaddr[N] = 0;
assign m_awprot[N] = 0;
assign m_wdata[N] = 0;
assign m_wstrb[N] = 0;
end endgenerate
generate for(N=0; N<NM; N=N+1)
begin : DECODE_READ_REQUEST
wire [NS:0] rdecode;
skidbuffer #(.DW(AW+3), .OPT_OUTREG(OPT_SKID_INPUT))
arskid(S_AXI_ACLK, !S_AXI_ARESETN,
S_AXI_ARVALID[N], S_AXI_ARREADY[N],
{ S_AXI_ARADDR[N*AW +: AW], S_AXI_ARPROT[N*3 +: 3] },
skd_arvalid[N], !skd_arstall[N],
{ skd_araddr[N], skd_arprot[N] });
addrdecode #(.AW(AW), .DW(3), .NS(NS),
.SLAVE_ADDR(SLAVE_ADDR), .SLAVE_MASK(SLAVE_MASK),
.OPT_REGISTERED(OPT_BUFFER_DECODER))
rdaddr(.i_clk(S_AXI_ACLK), .i_reset(!S_AXI_ARESETN),
.i_valid(skd_arvalid[N]), .o_stall(skd_arstall[N]),
.i_addr(skd_araddr[N]), .i_data(skd_arprot[N]),
.o_valid(dcd_arvalid[N]),
.i_stall(!m_arvalid[N] || !slave_raccepts[N]),
.o_decode(rdecode), .o_addr(m_araddr[N]),
.o_data(m_arprot[N]));
always @(*)
begin
m_arvalid[N] = dcd_arvalid[N] && !srfull[N];
rrequest[N] = 0;
if (!srfull[N])
rrequest[N][NS:0] = rdecode;
end
always @(*)
begin
slave_raccepts[N] = 1'b1;
if (!srgrant[N])
slave_raccepts[N] = 1'b0;
if (srfull[N])
slave_raccepts[N] = 1'b0;
// verilator lint_off WIDTH
if (!rrequest[N][srindex[N]])
slave_raccepts[N] = 1'b0;
// verilator lint_on WIDTH
if (!rgrant[N][NS])
begin
if (m_axi_arvalid[srindex[N]] && !m_axi_arready[srindex[N]])
slave_raccepts[N] = 1'b0;
end else if (S_AXI_RVALID[N] && !S_AXI_RREADY[N])
slave_raccepts[N] = 1'b0;
end
`ifdef FORMAL
always @(*)
if (skd_arvalid[N])
assert(skd_arprot[N] == 0);
`endif
end for (N=NM; N<NMFULL; N=N+1)
begin : UNUSED_RSKID_BUFFERS
always @(*)
m_arvalid[N] = 0;
assign m_araddr[N] = 0;
assign m_arprot[N] = 0;
end endgenerate
always @(*)
begin : DECONFLICT_WRITE_REQUESTS
for(iN=1; iN<NM ; iN=iN+1)
wrequested[iN] = 0;
// Vivado may complain about too many bits for wrequested.
// This is (currrently) expected. swindex is used to index
// into wrequested, and swindex has LGNS bits, where LGNS
// is $clog2(NS+1) rather than $clog2(NS). The extra bits
// are defined to be zeros, but the point is there are defined.
// Therefore, no matter what swindex is, it will always
// reference something valid.
wrequested[NM] = 0;
for(iM=0; iM<NS; iM=iM+1)
begin
wrequested[0][iM] = 1'b0;
for(iN=1; iN<NM ; iN=iN+1)
begin
// Continue to request any channel with
// a grant and pending operations
if (wrequest[iN-1][iM] && wgrant[iN-1][iM])
wrequested[iN][iM] = 1;
if (wrequest[iN-1][iM] && (!swgrant[iN-1]||swempty[iN-1]))
wrequested[iN][iM] = 1;
// Otherwise, if it's already claimed, then
// it can't be claimed again
if (wrequested[iN-1][iM])
wrequested[iN][iM] = 1;
end
wrequested[NM][iM] = wrequest[NM-1][iM] || wrequested[NM-1][iM];
end
end
always @(*)
begin : DECONFLICT_READ_REQUESTS
for(iN=0; iN<NM ; iN=iN+1)
rrequested[iN] = 0;
// See the note above for wrequested. This applies to
// rrequested as well.
rrequested[NM] = 0;
for(iM=0; iM<NS; iM=iM+1)
begin
rrequested[0][iM] = 0;
for(iN=1; iN<NM ; iN=iN+1)
begin
// Continue to request any channel with
// a grant and pending operations
if (rrequest[iN-1][iM] && rgrant[iN-1][iM])
rrequested[iN][iM] = 1;
if (rrequest[iN-1][iM] && (!srgrant[iN-1] || srempty[iN-1]))
rrequested[iN][iM] = 1;
// Otherwise, if it's already claimed, then
// it can't be claimed again
if (rrequested[iN-1][iM])
rrequested[iN][iM] = 1;
end
rrequested[NM][iM] = rrequest[NM-1][iM] || rrequested[NM-1][iM];
end
end
generate for(M=0; M<NS; M=M+1)
begin
always @(*)
begin
mwgrant[M] = 0;
for(iN=0; iN<NM; iN=iN+1)
if (wgrant[iN][M])
mwgrant[M] = 1;
end
always @(*)
begin
mrgrant[M] = 0;
for(iN=0; iN<NM; iN=iN+1)
if (rgrant[iN][M])
mrgrant[M] = 1;
end
end endgenerate
generate for(N=0; N<NM; N=N+1)
begin : ARBITRATE_WRITE_REQUESTS
reg stay_on_channel;
reg requested_channel_is_available;
reg leave_channel;
reg [LGNS-1:0] requested_index;
always @(*)
begin
stay_on_channel = |(wrequest[N][NS:0] & wgrant[N]);
if (swgrant[N] && !swempty[N])
stay_on_channel = 1;
end
always @(*)
begin
requested_channel_is_available =
|(wrequest[N][NS-1:0] & ~mwgrant
& ~wrequested[N][NS-1:0]);
if (wrequest[N][NS])
requested_channel_is_available = 1;
if (NM < 2)
requested_channel_is_available = m_awvalid[N];
end
reg linger;
if (OPT_LINGER == 0)
begin
always @(*)
linger = 0;
end else begin : WRITE_LINGER
reg [LGLINGER-1:0] linger_counter;
initial linger = 0;
initial linger_counter = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || wgrant[N][NS])
begin
linger <= 0;
linger_counter <= 0;
end else if (!swempty[N] || S_AXI_BVALID[N])
begin
linger_counter <= OPT_LINGER;
linger <= 1;
end else if (linger_counter > 0)
begin
linger <= (linger_counter > 1);
linger_counter <= linger_counter - 1;
end else
linger <= 0;
`ifdef FORMAL
always @(*)
assert(linger == (linger_counter != 0));
`endif
end
always @(*)
begin
leave_channel = 0;
if (!m_awvalid[N]
&& (!linger || wrequested[NM][swindex[N]]))
// Leave the channel after OPT_LINGER counts
// of the channel being idle, or when someone
// else asks for the channel
leave_channel = 1;
if (m_awvalid[N] && !wrequest[N][swindex[N]])
// Need to leave this channel to connect
// to any other channel
leave_channel = 1;
end
initial wgrant[N] = 0;
initial swgrant[N] = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
begin
wgrant[N] <= 0;
swgrant[N] <= 0;
end else if (!stay_on_channel)
begin
if (requested_channel_is_available)
begin
// Switching channels
swgrant[N] <= 1'b1;
wgrant[N] <= wrequest[N][NS:0];
end else if (leave_channel)
begin
swgrant[N] <= 1'b0;
wgrant[N] <= 0;
end
end
always @(*)
begin
requested_index = 0;
for(iM=0; iM<=NS; iM=iM+1)
if (wrequest[N][iM])
requested_index= requested_index | iM[LGNS-1:0];
end
// Now for swindex
initial swindex[N] = 0;
always @(posedge S_AXI_ACLK)
if (!stay_on_channel && requested_channel_is_available)
swindex[N] <= requested_index;
end for (N=NM; N<NMFULL; N=N+1)
begin
always @(*)
swindex[N] = 0;
end endgenerate
generate for(N=0; N<NM; N=N+1)
begin : ARBITRATE_READ_REQUESTS
reg stay_on_channel;
reg requested_channel_is_available;
reg leave_channel;
reg [LGNS-1:0] requested_index;
always @(*)
begin
stay_on_channel = |(rrequest[N][NS:0] & rgrant[N]);
if (srgrant[N] && !srempty[N])
stay_on_channel = 1;
end
always @(*)
begin
requested_channel_is_available =
|(rrequest[N][NS-1:0] & ~mrgrant
& ~rrequested[N][NS-1:0]);
if (rrequest[N][NS])
requested_channel_is_available = 1;
if (NM < 2)
requested_channel_is_available = m_arvalid[N];
end
reg linger;
if (OPT_LINGER == 0)
begin
always @(*)
linger = 0;
end else begin : READ_LINGER
reg [LGLINGER-1:0] linger_counter;
initial linger = 0;
initial linger_counter = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || rgrant[N][NS])
begin
linger <= 0;
linger_counter <= 0;
end else if (!srempty[N] || S_AXI_RVALID[N])
begin
linger_counter <= OPT_LINGER;
linger <= 1;
end else if (linger_counter > 0)
begin
linger <= (linger_counter > 1);
linger_counter <= linger_counter - 1;
end else
linger <= 0;
`ifdef FORMAL
always @(*)
assert(linger == (linger_counter != 0));
`endif
end
always @(*)
begin
leave_channel = 0;
if (!m_arvalid[N]
&& (!linger || rrequested[NM][srindex[N]]))
// Leave the channel after OPT_LINGER counts
// of the channel being idle, or when someone
// else asks for the channel
leave_channel = 1;
if (m_arvalid[N] && !rrequest[N][srindex[N]])
// Need to leave this channel to connect
// to any other channel
leave_channel = 1;
end
initial rgrant[N] = 0;
initial srgrant[N] = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
begin
rgrant[N] <= 0;
srgrant[N] <= 0;
end else if (!stay_on_channel)
begin
if (requested_channel_is_available)
begin
// Switching channels
srgrant[N] <= 1'b1;
rgrant[N] <= rrequest[N][NS:0];
end else if (leave_channel)
begin
srgrant[N] <= 1'b0;
rgrant[N] <= 0;
end
end
always @(*)
begin
requested_index = 0;
for(iM=0; iM<=NS; iM=iM+1)
if (rrequest[N][iM])
requested_index = requested_index|iM[LGNS-1:0];
end
// Now for srindex
initial srindex[N] = 0;
always @(posedge S_AXI_ACLK)
if (!stay_on_channel && requested_channel_is_available)
srindex[N] <= requested_index;
end for (N=NM; N<NMFULL; N=N+1)
begin
always @(*)
srindex[N] = 0;
end endgenerate
`ifdef FORMAL
generate for (N=0; N<NM; N=N+1)
begin
always @(*)
if (dcd_awvalid[N])
assert(m_awprot[N] == 0);
always @(*)
if (dcd_arvalid[N])
assert(m_arprot[N] == 0);
end endgenerate
`endif
// Calculate mwindex
generate for (M=0; M<NS; M=M+1)
begin : SLAVE_WRITE_INDEX
if (NM <= 1)
begin
always @(*)
mwindex[M] = 0;
end else begin : MULTIPLE_MASTERS
reg [LGNM-1:0] reswindex;
always @(*)
begin
reswindex = 0;
for(iN=0; iN<NM; iN=iN+1)
if ((!swgrant[iN] || swempty[iN])
&&(wrequest[iN][M] && !wrequested[iN][M]))
reswindex = reswindex | iN[LGNM-1:0];
end
always @(posedge S_AXI_ACLK)
if (!mwgrant[M])
mwindex[M] <= reswindex;
end
end for (M=NS; M<NSFULL; M=M+1)
begin
always @(*)
mwindex[M] = 0;
end endgenerate
// Calculate mrindex
generate for (M=0; M<NS; M=M+1)
begin : SLAVE_READ_INDEX
if (NM <= 1)
begin
always @(*)
mrindex[M] = 0;
end else begin : MULTIPLE_MASTERS
reg [LGNM-1:0] resrindex;
always @(*)
begin
resrindex = 0;
for(iN=0; iN<NM; iN=iN+1)
if ((!srgrant[iN] || srempty[iN])
&&(rrequest[iN][M] && !rrequested[iN][M]))
resrindex = resrindex | iN[LGNM-1:0];
end
always @(posedge S_AXI_ACLK)
if (!mrgrant[M])
mrindex[M] <= resrindex;
end
end for (M=NS; M<NSFULL; M=M+1)
begin
always @(*)
mrindex[M] = 0;
end endgenerate
// Assign outputs to the various slaves
generate for(M=0; M<NS; M=M+1)
begin : WRITE_SLAVE_OUTPUTS
reg axi_awvalid;
reg [AW-1:0] axi_awaddr;
reg [2:0] axi_awprot;
reg axi_wvalid;
reg [DW-1:0] axi_wdata;
reg [DW/8-1:0] axi_wstrb;
//
reg axi_bready;
reg sawstall, swstall, mbstall;
always @(*)
sawstall= (M_AXI_AWVALID[M]&& !M_AXI_AWREADY[M]);
always @(*)
swstall = (M_AXI_WVALID[M] && !M_AXI_WREADY[M]);
always @(*)
mbstall = (S_AXI_BVALID[mwindex[M]] && !S_AXI_BREADY[mwindex[M]]);
initial axi_awvalid = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || !mwgrant[M])
axi_awvalid <= 0;
else if (!sawstall)
begin
axi_awvalid <= m_awvalid[mwindex[M]]
&&(slave_awaccepts[mwindex[M]]);
end
initial axi_awaddr = 0;
initial axi_awprot = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
begin
axi_awaddr <= 0;
axi_awprot <= 0;
end else if (OPT_LOWPOWER && !mwgrant[M])
begin
axi_awaddr <= 0;
axi_awprot <= 0;
end else if (!sawstall)
begin
if (!OPT_LOWPOWER||(m_awvalid[mwindex[M]]&&slave_awaccepts[mwindex[M]]))
begin
axi_awaddr <= m_awaddr[mwindex[M]];
axi_awprot <= m_awprot[mwindex[M]];
end else begin
axi_awaddr <= 0;
axi_awprot <= 0;
end
end
initial axi_wvalid = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || !mwgrant[M])
axi_wvalid <= 0;
else if (!swstall)
begin
axi_wvalid <= (m_wvalid[mwindex[M]])
&&(slave_waccepts[mwindex[M]]);
end
initial axi_wdata = 0;
initial axi_wstrb = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
begin
axi_wdata <= 0;
axi_wstrb <= 0;
end else if (OPT_LOWPOWER && !mwgrant[M])
begin
axi_wdata <= 0;
axi_wstrb <= 0;
end else if (!swstall)
begin
if (!OPT_LOWPOWER || (m_wvalid[mwindex[M]]&&slave_waccepts[mwindex[M]]))
begin
axi_wdata <= m_wdata[mwindex[M]];
axi_wstrb <= m_wstrb[mwindex[M]];
end else begin
axi_wdata <= 0;
axi_wstrb <= 0;
end
end
//
initial axi_bready = 1;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || !mwgrant[M])
axi_bready <= 1;
else if (!mbstall)
axi_bready <= 1;
else if (M_AXI_BVALID[M]) // && mbstall
axi_bready <= 0;
//
assign M_AXI_AWVALID[M] = axi_awvalid;
assign M_AXI_AWADDR[M*AW +: AW] = axi_awaddr;
assign M_AXI_AWPROT[M*3 +: 3] = axi_awprot;
//
//
assign M_AXI_WVALID[M] = axi_wvalid;
assign M_AXI_WDATA[M*DW +: DW] = axi_wdata;
assign M_AXI_WSTRB[M*DW/8 +: DW/8] = axi_wstrb;
//
//
assign M_AXI_BREADY[M] = axi_bready;
//
`ifdef FORMAL
if (OPT_LOWPOWER)
begin
always @(*)
if (!axi_awvalid)
begin
assert(axi_awaddr == 0);
assert(axi_awprot == 0);
end
always @(*)
if (!axi_wvalid)
begin
assert(axi_wdata == 0);
assert(axi_wstrb == 0);
end
end
`endif
end endgenerate
generate for(M=0; M<NS; M=M+1)
begin : READ_SLAVE_OUTPUTS
reg axi_arvalid;
reg [C_AXI_ADDR_WIDTH-1:0] axi_araddr;
reg [2:0] axi_arprot;
//
reg axi_rready;
reg arstall, srstall;
always @(*)
arstall= (M_AXI_ARVALID[M]&& !M_AXI_ARREADY[M]);
always @(*)
srstall = (S_AXI_RVALID[mrindex[M]]
&& !S_AXI_RREADY[mrindex[M]]);
initial axi_arvalid = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || !mrgrant[M])
axi_arvalid <= 0;
else if (!arstall)
begin
axi_arvalid <= m_arvalid[mrindex[M]] && slave_raccepts[mrindex[M]];
end
initial axi_araddr = 0;
initial axi_arprot = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
begin
axi_araddr <= 0;
axi_arprot <= 0;
end else if (OPT_LOWPOWER && !mrgrant[M])
begin
axi_araddr <= 0;
axi_arprot <= 0;
end else if (!arstall)
begin
if (!OPT_LOWPOWER || (m_arvalid[mrindex[M]] && slave_raccepts[mrindex[M]]))
begin
if (NM == 1)
begin
axi_araddr <= m_araddr[0];
axi_arprot <= m_arprot[0];
end else begin
axi_araddr <= m_araddr[mrindex[M]];
axi_arprot <= m_arprot[mrindex[M]];
end
end else begin
axi_araddr <= 0;
axi_arprot <= 0;
end
end
initial axi_rready = 1;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN || !mrgrant[M])
axi_rready <= 1;
else if (!srstall)
axi_rready <= 1;
else if (M_AXI_RVALID[M] && M_AXI_RREADY[M]) // && srstall
axi_rready <= 0;
//
assign M_AXI_ARVALID[M] = axi_arvalid;
assign M_AXI_ARADDR[M*AW +: AW] = axi_araddr;
assign M_AXI_ARPROT[M*3 +: 3] = axi_arprot;
//
assign M_AXI_RREADY[M] = axi_rready;
//
`ifdef FORMAL
if (OPT_LOWPOWER)
begin
always @(*)
if (!axi_arvalid)
begin
assert(axi_araddr == 0);
assert(axi_arprot == 0);
end
end
`endif
end endgenerate
reg r_bvalid [0:NM-1];
reg [1:0] r_bresp [0:NM-1];
// Return values
generate for (N=0; N<NM; N=N+1)
begin : WRITE_RETURN_CHANNEL
reg axi_bvalid;
reg [1:0] axi_bresp;
reg i_axi_bvalid;
reg [1:0] i_axi_bresp;
reg mbstall;
always @(*)
if (wgrant[N][NS])
i_axi_bvalid = m_wvalid[N] && slave_waccepts[N];
else
i_axi_bvalid = m_axi_bvalid[swindex[N]];
always @(*)
i_axi_bresp = m_axi_bresp[swindex[N]];
always @(*)
mbstall = S_AXI_BVALID[N] && !S_AXI_BREADY[N];
initial r_bvalid[N] = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
r_bvalid[N] <= 0;
else if (mbstall && !r_bvalid[N] && !wgrant[N][NS])
r_bvalid[N] <= swgrant[N] && i_axi_bvalid;
else if (!mbstall)
r_bvalid[N] <= 1'b0;
initial r_bresp[N] = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
r_bresp[N] <= 0;
else if (OPT_LOWPOWER && (!swgrant[N] || S_AXI_BREADY[N]))
r_bresp[N] <= 0;
else if (!r_bvalid[N])
begin
if (!OPT_LOWPOWER ||(i_axi_bvalid && !wgrant[N][NS] && mbstall))
begin
r_bresp[N] <= i_axi_bresp;
end else
r_bresp[N] <= 0;
end
initial axi_bvalid = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
axi_bvalid <= 0;
else if (!mbstall)
axi_bvalid <= swgrant[N] && (r_bvalid[N] || i_axi_bvalid);
initial axi_bresp = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
axi_bresp <= 0;
else if (OPT_LOWPOWER && !swgrant[N])
axi_bresp <= 0;
else if (!mbstall)
begin
if (r_bvalid[N])
axi_bresp <= r_bresp[N];
else if (!OPT_LOWPOWER || i_axi_bvalid)
axi_bresp <= i_axi_bresp;
else
axi_bresp <= 0;
if (wgrant[N][NS] && (!OPT_LOWPOWER || i_axi_bvalid))
axi_bresp <= INTERCONNECT_ERROR;
end
//
assign S_AXI_BVALID[N] = axi_bvalid;
assign S_AXI_BRESP[N*2 +: 2] = axi_bresp;
`ifdef FORMAL
always @(*)
if (r_bvalid[N])
assert(r_bresp[N] != 2'b01);
always @(*)
if (swgrant[N])
assert(m_axi_bready[swindex[N]] == !r_bvalid[N]);
else
assert(!r_bvalid[N]);
always @(*)
if (OPT_LOWPOWER && !r_bvalid[N])
assert(r_bresp[N] == 0);
always @(*)
if (OPT_LOWPOWER && !axi_bvalid)
assert(axi_bresp == 0);
`endif
end endgenerate
always @(*)
begin
m_axi_arvalid = 0;
m_axi_arready = 0;
m_axi_rvalid = 0;
m_axi_rready = 0;
m_axi_arvalid[NS-1:0] = M_AXI_ARVALID;
m_axi_arready[NS-1:0] = M_AXI_ARREADY;
m_axi_rvalid[NS-1:0] = M_AXI_RVALID;
m_axi_rready[NS-1:0] = M_AXI_RREADY;
end
reg r_rvalid [0:NM-1];
reg [1:0] r_rresp [0:NM-1];
reg [DW-1:0] r_rdata [0:NM-1];
// Return values
generate for (N=0; N<NM; N=N+1)
begin : READ_RETURN_CHANNEL
reg axi_rvalid;
reg [1:0] axi_rresp;
reg [DW-1:0] axi_rdata;
reg srstall;
reg i_axi_rvalid;
always @(*)
if (rgrant[N][NS])
i_axi_rvalid = m_arvalid[N] && slave_raccepts[N];
else
i_axi_rvalid = m_axi_rvalid[srindex[N]];
always @(*)
srstall = S_AXI_RVALID[N] && !S_AXI_RREADY[N];
initial r_rvalid[N] = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
r_rvalid[N] <= 0;
else if (srstall && !r_rvalid[N])
r_rvalid[N] <= srgrant[N] && !rgrant[N][NS]&&i_axi_rvalid;
else if (!srstall)
r_rvalid[N] <= 0;
initial r_rresp[N] = 0;
initial r_rdata[N] = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
begin
r_rresp[N] <= 0;
r_rdata[N] <= 0;
end else if (OPT_LOWPOWER && (!srgrant[N] || S_AXI_RREADY[N]))
begin
r_rresp[N] <= 0;
r_rdata[N] <= 0;
end else if (!r_rvalid[N])
begin
if (!OPT_LOWPOWER || (i_axi_rvalid && !rgrant[N][NS] && srstall))
begin
if (NS == 1)
begin
r_rresp[N] <= m_axi_rresp[0];
r_rdata[N] <= m_axi_rdata[0];
end else begin
r_rresp[N] <= m_axi_rresp[srindex[N]];
r_rdata[N] <= m_axi_rdata[srindex[N]];
end
end else begin
r_rresp[N] <= 0;
r_rdata[N] <= 0;
end
end
initial axi_rvalid = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
axi_rvalid <= 0;
else if (!srstall)
axi_rvalid <= srgrant[N] && (r_rvalid[N] || i_axi_rvalid);
initial axi_rresp = 0;
initial axi_rdata = 0;
always @(posedge S_AXI_ACLK)
if (OPT_LOWPOWER && !S_AXI_ARESETN)
begin
axi_rresp <= 0;
axi_rdata <= 0;
end else if (OPT_LOWPOWER && !srgrant[N])
begin
axi_rresp <= 0;
axi_rdata <= 0;
end else if (!srstall)
begin
if (r_rvalid[N])
begin
axi_rresp <= r_rresp[N];
axi_rdata <= r_rdata[N];
end else if (!OPT_LOWPOWER || i_axi_rvalid)
begin
if (NS == 1)
begin
axi_rresp <= m_axi_rresp[0];
axi_rdata <= m_axi_rdata[0];
end else begin
axi_rresp <= m_axi_rresp[srindex[N]];
axi_rdata <= m_axi_rdata[srindex[N]];
end
if (rgrant[N][NS])
axi_rresp <= INTERCONNECT_ERROR;
end else begin
axi_rresp <= 0;
axi_rdata <= 0;
end
end
assign S_AXI_RVALID[N] = axi_rvalid;
assign S_AXI_RRESP[N*2 +: 2] = axi_rresp;
assign S_AXI_RDATA[N*DW +: DW]= axi_rdata;
`ifdef FORMAL
always @(*)
if (r_rvalid[N])
assert(r_rresp[N] != 2'b01);
always @(*)
if (srgrant[N] && !rgrant[N][NS])
assert(m_axi_rready[srindex[N]] == !r_rvalid[N]);
else
assert(!r_rvalid[N]);
always @(*)
if (OPT_LOWPOWER && !r_rvalid[N])
begin
assert(r_rresp[N] == 0);
assert(r_rdata[N] == 0);
end
always @(*)
if (OPT_LOWPOWER && !axi_rvalid)
begin
assert(axi_rresp == 0);
assert(axi_rdata == 0);
end
`endif
end endgenerate
// Count pending transactions
generate for (N=0; N<NM; N=N+1)
begin : COUNT_PENDING
reg [LGMAXBURST-1:0] wpending, awpending, rpending,
missing_wdata;
//reg rempty, awempty; // wempty;
(* keep *) reg r_wdata_expected;
initial awpending = 0;
initial swempty[N] = 1;
initial swfull[N] = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
begin
awpending <= 0;
swempty[N] <= 1;
swfull[N] <= 0;
end else case ({(m_awvalid[N] && slave_awaccepts[N]),
(S_AXI_BVALID[N] && S_AXI_BREADY[N])})
2'b01: begin
awpending <= awpending - 1;
swempty[N] <= (awpending <= 1);
swfull[N] <= 0;
end
2'b10: begin
awpending <= awpending + 1;
swempty[N] <= 0;
swfull[N] <= &awpending[LGMAXBURST-1:1];
end
default: begin end
endcase
initial wpending = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
wpending <= 0;
else case ({(m_wvalid[N] && slave_waccepts[N]),
(S_AXI_BVALID[N] && S_AXI_BREADY[N])})
2'b01: wpending <= wpending - 1;
2'b10: wpending <= wpending + 1;
default: begin end
endcase
initial missing_wdata = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
missing_wdata <= 0;
else begin
missing_wdata <= missing_wdata
+((m_awvalid[N] && slave_awaccepts[N])? 1:0)
-((m_wvalid[N] && slave_waccepts[N])? 1:0);
end
initial r_wdata_expected = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
r_wdata_expected <= 0;
else case({ m_awvalid[N] && slave_awaccepts[N],
m_wvalid[N] && slave_waccepts[N] })
2'b10: r_wdata_expected <= 1;
2'b01: r_wdata_expected <= (missing_wdata > 1);
default: begin end
endcase
initial rpending = 0;
initial srempty[N] = 1;
initial srfull[N] = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
begin
rpending <= 0;
srempty[N]<= 1;
srfull[N] <= 0;
end else case ({(m_arvalid[N] && slave_raccepts[N]),
(S_AXI_RVALID[N] && S_AXI_RREADY[N])})
2'b01: begin
rpending <= rpending - 1;
srempty[N] <= (rpending == 1);
srfull[N] <= 0;
end
2'b10: begin
rpending <= rpending + 1;
srfull[N] <= &rpending[LGMAXBURST-1:1];
srempty[N] <= 0;
end
default: begin end
endcase
assign w_sawpending[N] = awpending;
assign w_swpending[N] = wpending;
assign w_srpending[N] = rpending;
always @(*)
wdata_expected[N] = r_wdata_expected;
`ifdef FORMAL
reg [LGMAXBURST-1:0] f_missing_wdata;
always @(*)
assert(missing_wdata == awpending - wpending);
always @(*)
assert(r_wdata_expected == (missing_wdata > 0));
`endif
end endgenerate
initial begin
if (NM == 0) begin
$display("At least one master must be defined");
$stop;
end
if (NS == 0) begin
$display("At least one slave must be defined");
$stop;
end
end
`ifdef FORMAL
localparam F_LGDEPTH = LGMAXBURST+1;
wire [F_LGDEPTH-1:0] fm_rd_outstanding [0:NM-1];
wire [F_LGDEPTH-1:0] fm_wr_outstanding [0:NM-1];
wire [F_LGDEPTH-1:0] fm_awr_outstanding [0:NM-1];
wire [F_LGDEPTH-1:0] fs_rd_outstanding [0:NS-1];
wire [F_LGDEPTH-1:0] fs_wr_outstanding [0:NS-1];
wire [F_LGDEPTH-1:0] fs_awr_outstanding [0:NS-1];
initial assert(NS >= 1);
initial assert(NM >= 1);
`ifdef VERIFIC
reg f_past_valid;
initial f_past_valid = 0;
always @(posedge S_AXI_ACLK)
f_past_valid <= 1;
`ifdef VERIFIC
`define INITIAL_CHECK assume
`else
`define INITIAL_CHECK assert
`endif // VERIFIC
always @(*)
if (!f_past_valid)
begin
`INITIAL_CHECK(!S_AXI_ARESETN);
`INITIAL_CHECK(S_AXI_BVALID == 0);
`INITIAL_CHECK(S_AXI_RVALID == 0);
`INITIAL_CHECK(swgrant == 0);
`INITIAL_CHECK(srgrant == 0);
`INITIAL_CHECK(swfull == 0);
`INITIAL_CHECK(srfull == 0);
`INITIAL_CHECK(&swempty);
`INITIAL_CHECK(&srempty);
for(iN=0; iN<NM; iN=iN+1)
begin
`INITIAL_CHECK(wgrant[iN] == 0);
assume(swindex[iN] == 0);
`INITIAL_CHECK(rgrant[iN] == 0);
assume(srindex[iN] == 0);
`INITIAL_CHECK(r_bvalid[iN] == 0);
`INITIAL_CHECK(r_rvalid[iN] == 0);
//
`INITIAL_CHECK(r_bresp[iN] == 0);
//
`INITIAL_CHECK(r_rresp[iN] == 0);
`INITIAL_CHECK(r_rdata[iN] == 0);
end
`INITIAL_CHECK(M_AXI_AWVALID == 0);
`INITIAL_CHECK(M_AXI_WVALID == 0);
`INITIAL_CHECK(M_AXI_RVALID == 0);
end
`endif
generate for(N=0; N<NM; N=N+1)
begin : CHECK_MASTER_GRANTS
// Write grants
always @(*)
for(iM=0; iM<=NS; iM=iM+1)
begin
if (wgrant[N][iM])
begin
assert((wgrant[N] ^ (1<<iM))==0);
assert(swgrant[N]);
assert(swindex[N] == iM);
if (iM < NS)
begin
assert(mwgrant[iM]);
assert(mwindex[iM] == N);
end
end
end
always @(*)
if (swgrant[N])
assert(wgrant[N] != 0);
always @(*)
if (wrequest[N][NS])
assert(wrequest[N][NS-1:0] == 0);
////////////////////////////////////////////////////////////////
//
// Read grant checking
//
always @(*)
for(iM=0; iM<=NS; iM=iM+1)
begin
if (rgrant[N][iM])
begin
assert((rgrant[N] ^ (1<<iM))==0);
assert(srgrant[N]);
assert(srindex[N] == iM);
if (iM < NS)
begin
assert(mrgrant[iM]);
assert(mrindex[iM] == N);
end
end
end
always @(*)
if (srgrant[N])
assert(rgrant[N] != 0);
always @(*)
if (rrequest[N][NS])
assert(rrequest[N][NS-1:0] == 0);
end endgenerate
generate for(N=0; N<NM; N=N+1)
begin : CHECK_MASTERS
faxil_slave #(
.C_AXI_DATA_WIDTH(DW),
.C_AXI_ADDR_WIDTH(AW),
.F_OPT_HAS_CACHE(1'b0),
.F_OPT_ASSUME_RESET(1'b1),
.F_AXI_MAXWAIT(0),
.F_AXI_MAXDELAY(0),
.F_LGDEPTH(F_LGDEPTH))
mstri(.i_clk(S_AXI_ACLK),
.i_axi_reset_n(S_AXI_ARESETN),
//
.i_axi_awready(S_AXI_AWREADY[N]),
.i_axi_awaddr(S_AXI_AWADDR[N*AW +: AW]),
.i_axi_awcache(0),
.i_axi_awprot(S_AXI_AWPROT[N*3 +: 3]),
.i_axi_awvalid(S_AXI_AWVALID[N]),
//
.i_axi_wready(S_AXI_WREADY[N]),
.i_axi_wdata( S_AXI_WDATA[N*DW +: DW]),
.i_axi_wstrb( S_AXI_WSTRB[N*DW/8 +: DW/8]),
.i_axi_wvalid(S_AXI_WVALID[N]),
//
.i_axi_bresp( S_AXI_BRESP[N*2 +: 2]),
.i_axi_bvalid(S_AXI_BVALID[N]),
.i_axi_bready(S_AXI_BREADY[N]),
//
.i_axi_arready(S_AXI_ARREADY[N]),
.i_axi_araddr( S_AXI_ARADDR[N*AW +: AW]),
.i_axi_arcache(4'b0),
.i_axi_arprot( S_AXI_ARPROT[N*3 +: 3]),
.i_axi_arvalid(S_AXI_ARVALID[N]),
//
//
.i_axi_rresp( S_AXI_RRESP[N*2 +: 2]),
.i_axi_rvalid(S_AXI_RVALID[N]),
.i_axi_rdata( S_AXI_RDATA[N*DW +: DW]),
.i_axi_rready(S_AXI_RREADY[N]),
//
.f_axi_rd_outstanding( fm_rd_outstanding[N]),
.f_axi_wr_outstanding( fm_wr_outstanding[N]),
.f_axi_awr_outstanding(fm_awr_outstanding[N]));
//
// Check write counters
//
always @(*)
if (S_AXI_ARESETN)
assert(fm_awr_outstanding[N] == { 1'b0, w_sawpending[N] }
+((OPT_BUFFER_DECODER & dcd_awvalid[N]) ? 1:0)
+ (S_AXI_AWREADY[N] ? 0:1));
always @(*)
if (S_AXI_ARESETN)
assert(fm_wr_outstanding[N] == { 1'b0, w_swpending[N] }
+ (S_AXI_WREADY[N] ? 0:1));
always @(*)
if (S_AXI_ARESETN)
assert(fm_awr_outstanding[N] >=
(S_AXI_AWREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER & dcd_awvalid[N]) ? 1:0)
+ (S_AXI_BVALID[N] ? 1:0));
always @(*)
if (S_AXI_ARESETN)
assert(fm_wr_outstanding[N] >=
(S_AXI_WREADY[N] ? 0:1)
+ (S_AXI_BVALID[N]? 1:0));
always @(*)
if (S_AXI_ARESETN)
assert(fm_wr_outstanding[N]-(S_AXI_WREADY[N] ? 0:1)
<= fm_awr_outstanding[N]-(S_AXI_AWREADY[N] ? 0:1));
always @(*)
if (S_AXI_ARESETN && wgrant[N][NS])
assert(fm_wr_outstanding[N] == (S_AXI_WREADY[N] ? 0:1)
+ (S_AXI_BVALID[N] ? 1:0));
always @(*)
if (S_AXI_ARESETN && !swgrant[N])
begin
assert(!S_AXI_BVALID[N]);
assert(fm_awr_outstanding[N]==(S_AXI_AWREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER & dcd_awvalid[N]) ? 1:0));
assert(fm_wr_outstanding[N] == (S_AXI_WREADY[N] ? 0:1));
assert(w_sawpending[N] == 0);
assert(w_swpending[N] == 0);
end
//
// Check read counters
//
always @(*)
if (S_AXI_ARESETN)
assert(fm_rd_outstanding[N] >=
(S_AXI_ARREADY[N] ? 0:1)
+(S_AXI_RVALID[N] ? 1:0));
always @(*)
if (S_AXI_ARESETN && (!srgrant[N] || rgrant[N][NS]))
assert(fm_rd_outstanding[N] ==
(S_AXI_ARREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER & dcd_arvalid[N]) ? 1:0)
+(S_AXI_RVALID[N] ? 1:0));
always @(*)
if (S_AXI_ARESETN)
assert(fm_rd_outstanding[N] == { 1'b0, w_srpending[N] }
+((OPT_BUFFER_DECODER & dcd_arvalid[N]) ? 1:0)
+ (S_AXI_ARREADY[N] ? 0:1));
always @(*)
if (S_AXI_ARESETN && rgrant[N][NS])
assert(fm_rd_outstanding[N] == (S_AXI_ARREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER & dcd_arvalid[N]) ? 1:0)
+(S_AXI_RVALID[N] ? 1:0));
always @(*)
if (S_AXI_ARESETN && !srgrant[N])
begin
assert(!S_AXI_RVALID[N]);
assert(fm_rd_outstanding[N]== (S_AXI_ARREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER && dcd_arvalid[N])? 1:0));
assert(w_srpending[N] == 0);
end
//
// Check full/empty flags
//
localparam [LGMAXBURST-1:0] NEAR_THRESHOLD = -2;
always @(*)
begin
assert(swfull[N] == &w_sawpending[N]);
assert(swempty[N] == (w_sawpending[N] == 0));
end
always @(*)
begin
assert(srfull[N] == &w_srpending[N]);
assert(srempty[N] == (w_srpending[N] == 0));
end
end endgenerate
generate for(M=0; M<NS; M=M+1)
begin : CHECK_SLAVES
faxil_master #(
.C_AXI_DATA_WIDTH(DW),
.C_AXI_ADDR_WIDTH(AW),
.F_OPT_HAS_CACHE(1'b0),
.F_OPT_ASSUME_RESET(1'b1),
.F_AXI_MAXRSTALL(0),
.F_LGDEPTH(F_LGDEPTH))
slvi(.i_clk(S_AXI_ACLK),
.i_axi_reset_n(S_AXI_ARESETN),
//
.i_axi_awready(M_AXI_AWREADY[M]),
.i_axi_awaddr(M_AXI_AWADDR[M*AW +: AW]),
.i_axi_awcache(0),
.i_axi_awprot(M_AXI_AWPROT[M*3 +: 3]),
.i_axi_awvalid(M_AXI_AWVALID[M]),
//
.i_axi_wready(M_AXI_WREADY[M]),
.i_axi_wdata( M_AXI_WDATA[M*DW +: DW]),
.i_axi_wstrb( M_AXI_WSTRB[M*DW/8 +: DW/8]),
.i_axi_wvalid(M_AXI_WVALID[M]),
//
.i_axi_bresp( M_AXI_BRESP[M*2 +: 2]),
.i_axi_bvalid(M_AXI_BVALID[M]),
.i_axi_bready(M_AXI_BREADY[M]),
//
.i_axi_arready(M_AXI_ARREADY[M]),
.i_axi_araddr( M_AXI_ARADDR[M*AW +: AW]),
.i_axi_arcache(4'b0),
.i_axi_arprot( M_AXI_ARPROT[M*3 +: 3]),
.i_axi_arvalid(M_AXI_ARVALID[M]),
//
//
.i_axi_rresp( M_AXI_RRESP[M*2 +: 2]),
.i_axi_rvalid(M_AXI_RVALID[M]),
.i_axi_rdata( M_AXI_RDATA[M*DW +: DW]),
.i_axi_rready(M_AXI_RREADY[M]),
//
.f_axi_rd_outstanding( fs_rd_outstanding[M]),
.f_axi_wr_outstanding( fs_wr_outstanding[M]),
.f_axi_awr_outstanding(fs_awr_outstanding[M]));
always @(*)
assert(fs_wr_outstanding[M] + (M_AXI_WVALID[M] ? 1:0)
<= fs_awr_outstanding[M] + (M_AXI_AWVALID[M]? 1:0));
always @(*)
if (!mwgrant[M])
begin
assert(fs_awr_outstanding[M] == 0);
assert(fs_wr_outstanding[M] == 0);
end
always @(*)
if (!mrgrant[M])
assert(fs_rd_outstanding[M] == 0);
always @(*)
assert(fs_awr_outstanding[M] < { 1'b1, {(F_LGDEPTH-1){1'b0}}});
always @(*)
assert(fs_wr_outstanding[M] < { 1'b1, {(F_LGDEPTH-1){1'b0}}});
always @(*)
assert(fs_rd_outstanding[M] < { 1'b1, {(F_LGDEPTH-1){1'b0}}});
always @(*)
if (M_AXI_AWVALID[M])
assert(((M_AXI_AWADDR[M*AW +: AW]
^ SLAVE_ADDR[M*AW +: AW])
& SLAVE_MASK[M*AW +: AW]) == 0);
always @(*)
if (M_AXI_ARVALID[M])
assert(((M_AXI_ARADDR[M*AW +: AW]
^ SLAVE_ADDR[M*AW +: AW])
& SLAVE_MASK[M*AW +: AW]) == 0);
end endgenerate
generate for(N=0; N<NM; N=N+1)
begin : CORRELATE_OUTSTANDING
always @(*)
if (S_AXI_ARESETN && (swgrant[N] && (swindex[N] < NS)))
begin
assert((fm_awr_outstanding[N]
- (S_AXI_AWREADY[N] ? 0:1)
-((OPT_BUFFER_DECODER && dcd_awvalid[N]) ? 1:0)
- (S_AXI_BVALID[N] ? 1:0))
== (fs_awr_outstanding[swindex[N]]
+ (m_axi_awvalid[swindex[N]] ? 1:0)
+ (m_axi_bready[swindex[N]] ? 0:1)));
assert((fm_wr_outstanding[N]
- (S_AXI_WREADY[N] ? 0:1)
- (S_AXI_BVALID[N] ? 1:0))
== (fs_wr_outstanding[swindex[N]]
+ (m_axi_wvalid[swindex[N]] ? 1:0)
+ (m_axi_bready[swindex[N]] ? 0:1)));
end else if (S_AXI_ARESETN && (!swgrant[N] || (swindex[N]==NS)))
begin
if (!swgrant[N])
assert(fm_awr_outstanding[N] ==
(S_AXI_AWREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER && dcd_awvalid[N]) ? 1:0)
+(S_AXI_BVALID[N] ? 1:0));
else
assert(fm_awr_outstanding[N] >=
(S_AXI_AWREADY[N] ? 0:1)
+((OPT_BUFFER_DECODER && dcd_awvalid[N]) ? 1:0)
+(S_AXI_BVALID[N] ? 1:0));
assert(fm_wr_outstanding[N] ==
(S_AXI_WREADY[N] ? 0:1)
+(S_AXI_BVALID[N] ? 1:0));
end
always @(*)
if (srgrant[N] && (srindex[N] < NS))
begin
assert((fm_rd_outstanding[N]//17
- (S_AXI_ARREADY[N] ? 0:1)//1
-((OPT_BUFFER_DECODER && dcd_arvalid[N]) ? 1:0)
- (S_AXI_RVALID[N] ? 1:0))//0
== (fs_rd_outstanding[srindex[N]]//16
+ (m_axi_arvalid[srindex[N]] ? 1:0)//0
+ (m_axi_rready[srindex[N]] ? 0:1)));//0
end
end endgenerate
////////////////////////////////////////////////////////////////////////
//
// Cover properties
//
////////////////////////////////////////////////////////////////////////
//
//
// Can every master reach every slave?
// Can things transition without dropping the request line(s)?
generate for(N=0; N<NM; N=N+1)
begin : COVER_CONNECTIVITY_FROM_MASTER
reg [3:0] w_returns, r_returns;
reg err_wr_return, err_rd_return;
reg [NS-1:0] w_every, r_every;
reg was_wevery, was_revery, whsreturn, rhsreturn;
// w_returns is a speed check: Can we return one write
// acknowledgement per clock cycle?
initial w_returns = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
w_returns = 0;
else begin
w_returns <= { w_returns[2:0], 1'b0 };
if (S_AXI_BVALID[N] && S_AXI_BREADY[N] && !wgrant[N][NS])
w_returns[0] <= 1'b1;
end
initial whsreturn = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
whsreturn <= 0;
else
whsreturn <= whsreturn || (&w_returns);
// w_every is a connectivity test: Can we get a return from
// every slave?
initial w_every = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
w_every <= 0;
else if (!S_AXI_AWVALID[N])
w_every <= 0;
else begin
if (S_AXI_BVALID[N] && S_AXI_BREADY[N] && !wgrant[N][NS])
w_every[swindex[N]] <= 1'b1;
end
always @(posedge S_AXI_ACLK)
if (S_AXI_BVALID[N])
assert($stable(swindex[N]));
initial was_wevery = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
was_wevery <= 0;
else
was_wevery <= was_wevery || (&w_every);
// err_wr_return is a test to make certain we can return a
// bus error on the write channel.
initial err_wr_return = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
err_wr_return = 0;
else if (wgrant[N][NS] && S_AXI_BVALID[N]
&& (S_AXI_BRESP[2*N+:2]==INTERCONNECT_ERROR))
err_wr_return = 1;
`ifndef VERILATOR
always @(*)
cover(!swgrant[N] && whsreturn);
always @(*)
cover(!swgrant[N] && was_wevery);
always @(*)
cover(S_AXI_ARESETN && wrequest[N][NS]);
always @(*)
cover(S_AXI_ARESETN && wrequest[N][NS] && slave_awaccepts[N]);
always @(*)
cover(err_wr_return);
always @(*)
cover(!swgrant[N] && err_wr_return);
`endif
always @(*)
if (S_AXI_BVALID[N])
assert(swgrant[N]);
// r_returns is a speed check: Can we return one read
// acknowledgment per clock cycle?
initial r_returns = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
r_returns = 0;
else begin
r_returns <= { r_returns[2:0], 1'b0 };
if (S_AXI_RVALID[N] && S_AXI_RREADY[N])
r_returns[0] <= 1'b1;
end
initial rhsreturn = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
rhsreturn <= 0;
else
rhsreturn <= rhsreturn || (&r_returns);
// r_every is a connectivity test: Can we get a read return from
// every slave?
initial r_every = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
r_every = 0;
else if (!S_AXI_ARVALID[N])
r_every = 0;
else begin
if (S_AXI_RVALID[N] && S_AXI_RREADY[N])
r_every[srindex[N]] <= 1'b1;
end
// was_revery is a return to idle check following the
// connectivity test. Since the connectivity test is cleared
// if there's ever a drop in the valid line, we need a separate
// wire to check that this master can return to idle again.
initial was_revery = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
was_revery <= 0;
else
was_revery <= was_revery || (&r_every);
always @(posedge S_AXI_ACLK)
if (S_AXI_RVALID[N])
assert($stable(srindex[N]));
initial err_rd_return = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
err_rd_return = 0;
else if (rgrant[N][NS] && S_AXI_RVALID[N]
&& (S_AXI_RRESP[2*N+:2]==INTERCONNECT_ERROR))
err_rd_return = 1;
`ifndef VERILATOR
always @(*)
cover(!srgrant[N] && rhsreturn); // @26
always @(*)
cover(!srgrant[N] && was_revery); // @26
always @(*)
cover(S_AXI_ARVALID[N] && rrequest[N][NS]);
always @(*)
cover(rgrant[N][NS]);
always @(*)
cover(err_rd_return);
always @(*)
cover(!srgrant[N] && err_rd_return); //@!
`endif
always @(*)
if (S_AXI_BVALID[N] && wgrant[N][NS])
assert(S_AXI_BRESP[2*N+:2]==INTERCONNECT_ERROR);
always @(*)
if (S_AXI_RVALID[N] && rgrant[N][NS])
assert(S_AXI_RRESP[2*N+:2]==INTERCONNECT_ERROR);
end endgenerate
reg multi_write_hit, multi_read_hit;
initial multi_write_hit = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
multi_write_hit <= 0;
else if (fm_awr_outstanding[0] > 2 && !wgrant[0][NS])
multi_write_hit <= 1;
initial multi_read_hit = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
multi_read_hit <= 0;
else if (fm_rd_outstanding[0] > 2 && !rgrant[0][NS])
multi_read_hit <= 1;
always @(*)
cover(multi_write_hit);
always @(*)
cover(multi_read_hit);
always @(*)
cover(S_AXI_ARESETN && multi_write_hit & mwgrant == 0 && M_AXI_BVALID == 0);
always @(*)
cover(S_AXI_ARESETN && multi_read_hit & mrgrant == 0 && M_AXI_RVALID == 0);
////////////////////////////////////////////////////////////////////////
//
// Negation check
//
// Pick a particular value. Assume the value doesn't show up on the
// input. Prove it doesn't show up on the output. This will check for
// ...
// 1. Stuck bits on the output channel
// 2. Cross-talk between channels
//
////////////////////////////////////////////////////////////////////////
//
//
(* anyconst *) reg [LGNM-1:0] f_const_source;
(* anyconst *) reg [AW-1:0] f_const_addr;
(* anyconst *) reg [AW-1:0] f_const_addr_n;
(* anyconst *) reg [DW-1:0] f_const_data_n;
(* anyconst *) reg [DW/8-1:0] f_const_strb_n;
(* anyconst *) reg [3-1:0] f_const_prot_n;
(* anyconst *) reg [2-1:0] f_const_resp_n;
reg [LGNS-1:0] f_const_slave;
always @(*)
assume(f_const_source < NM);
always @(*)
begin
f_const_slave = NS;
for(iM=0; iM<NS; iM=iM+1)
begin
if (((f_const_addr ^ SLAVE_ADDR[iM*AW+:AW])
&SLAVE_MASK[iM*AW+:AW])==0)
f_const_slave = iM;
end
assume(f_const_slave < NS);
end
reg [AW-1:0] f_awaddr;
reg [AW-1:0] f_araddr;
always @(*)
f_awaddr = S_AXI_AWADDR[f_const_source * AW +: AW];
always @(*)
f_araddr = S_AXI_ARADDR[f_const_source * AW +: AW];
// The assumption check: assume our negated values are not found on
// the inputs
always @(*)
begin
if (S_AXI_AWVALID[f_const_source])
begin
assume(f_awaddr != f_const_addr_n);
assume(S_AXI_AWPROT[f_const_source*3+:3] != f_const_prot_n);
end
if (m_wvalid)
begin
assume(m_wdata[f_const_source] != f_const_data_n);
assume(m_wstrb[f_const_source] != f_const_strb_n);
end
if (S_AXI_ARVALID[f_const_source])
begin
assume(f_araddr != f_const_addr_n);
assume(S_AXI_ARPROT[f_const_source*3+:3] != f_const_prot_n);
end
if (M_AXI_BVALID[f_const_slave] && wgrant[f_const_source][f_const_slave])
begin
assume(m_axi_bresp[f_const_slave] != f_const_resp_n);
end
if (M_AXI_RVALID[f_const_slave] && rgrant[f_const_source][f_const_slave])
begin
assume(m_axi_rdata[f_const_slave] != f_const_data_n);
assume(m_axi_rresp[f_const_slave] != f_const_resp_n);
end
end
// Proof check: Prove these values are not found on our outputs
always @(*)
begin
if (skd_awvalid[f_const_source])
begin
assert(skd_awaddr[f_const_source] != f_const_addr_n);
assert(skd_awprot[f_const_source] != f_const_prot_n);
end
if (dcd_awvalid[f_const_source])
begin
assert(m_awaddr[f_const_source] != f_const_addr_n);
assert(m_awprot[f_const_source] != f_const_prot_n);
end
if (M_AXI_AWVALID[f_const_slave] && wgrant[f_const_source][f_const_slave])
begin
assert(M_AXI_AWADDR[f_const_slave*AW+:AW] != f_const_addr_n);
assert(M_AXI_AWPROT[f_const_slave*3+:3] != f_const_prot_n);
end
if (M_AXI_WVALID[f_const_slave] && wgrant[f_const_source][f_const_slave])
begin
assert(M_AXI_WDATA[f_const_slave*DW+:DW] != f_const_data_n);
assert(M_AXI_WSTRB[f_const_slave*(DW/8)+:(DW/8)] != f_const_strb_n);
end
if (skd_arvalid[f_const_source])
begin
assert(skd_araddr[f_const_source] != f_const_addr_n);
assert(skd_arprot[f_const_source] != f_const_prot_n);
end
if (dcd_arvalid[f_const_source])
begin
assert(m_araddr[f_const_source] != f_const_addr_n);
assert(m_arprot[f_const_source] != f_const_prot_n);
end
if (M_AXI_ARVALID[f_const_slave] && rgrant[f_const_source][f_const_slave])
begin
assert(M_AXI_ARADDR[f_const_slave*AW+:AW] != f_const_addr_n);
assert(M_AXI_ARPROT[f_const_slave*3+:3] != f_const_prot_n);
end
//
if (r_bvalid[f_const_source] && wgrant[f_const_source][f_const_slave])
assert(r_bresp[f_const_source] != f_const_resp_n);
if (S_AXI_BVALID[f_const_source] && wgrant[f_const_source][f_const_slave])
assert(S_AXI_BRESP[f_const_source*2+:2] != f_const_resp_n);
if (r_rvalid[f_const_source] && rgrant[f_const_source][f_const_slave])
begin
assert(r_rresp[f_const_source] != f_const_resp_n);
assert(r_rdata[f_const_source] != f_const_data_n);
end
if (S_AXI_RVALID[f_const_source] && rgrant[f_const_source][f_const_slave])
begin
assert(S_AXI_RRESP[f_const_source*2+:2]!=f_const_resp_n);
assert(S_AXI_RDATA[f_const_source*DW+:DW]!=f_const_data_n);
end
end
////////////////////////////////////////////////////////////////////////
//
// (Careless) constraining assumptions
//
////////////////////////////////////////////////////////////////////////
//
//
generate for(N=0; N<NM; N=N+1)
begin
end endgenerate
`endif
endmodule
`ifndef YOSYS
`default_nettype wire
`endif