summaryrefslogtreecommitdiff
path: root/rtl/wb2axip/axispacker.v
diff options
context:
space:
mode:
Diffstat (limited to 'rtl/wb2axip/axispacker.v')
-rw-r--r--rtl/wb2axip/axispacker.v890
1 files changed, 890 insertions, 0 deletions
diff --git a/rtl/wb2axip/axispacker.v b/rtl/wb2axip/axispacker.v
new file mode 100644
index 0000000..74b8f5b
--- /dev/null
+++ b/rtl/wb2axip/axispacker.v
@@ -0,0 +1,890 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: axispacker
+// {{{
+// Project: WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose: AXI-Stream packer: This uses TKEEP to pack bytes in a stream.
+// Bytes with TKEEP clear on input will be removed from the
+// output stream.
+//
+// TID, TDEST, and TUSER fields are not (currently) implemented, although
+// they shouldn't be too hard to add back in.
+//
+// This design *ASSUMES* that TLAST will only be set if TKEEP is not zero.
+// This assumption is not required by the AXI-stream specification, and
+// should be removed in the future.
+//
+// Creator: Dan Gisselquist, Ph.D.
+// Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2021-2024, 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 axispacker #(
+ parameter C_AXIS_DATA_WIDTH = 32,
+ parameter [0:0] OPT_LOWPOWER = 1
+ ) (
+ // {{{
+ input wire S_AXI_ACLK, S_AXI_ARESETN,
+ // Incoming slave interface
+ // {{{
+ input wire S_AXIS_TVALID,
+ output wire S_AXIS_TREADY,
+ input wire [C_AXIS_DATA_WIDTH-1:0] S_AXIS_TDATA,
+ input wire [C_AXIS_DATA_WIDTH/8-1:0] S_AXIS_TSTRB,
+ input wire [C_AXIS_DATA_WIDTH/8-1:0] S_AXIS_TKEEP,
+ input wire S_AXIS_TLAST,
+ // }}}
+ // Outgoing AXI-Stream master interface
+ // {{{
+ output reg M_AXIS_TVALID,
+ input wire M_AXIS_TREADY,
+ output reg [C_AXIS_DATA_WIDTH-1:0] M_AXIS_TDATA,
+ output reg [C_AXIS_DATA_WIDTH/8-1:0] M_AXIS_TSTRB,
+ output reg [C_AXIS_DATA_WIDTH/8-1:0] M_AXIS_TKEEP,
+ output reg M_AXIS_TLAST
+ // }}}
+ // }}}
+ );
+
+ // Local declarations
+ // {{{
+ localparam DW = C_AXIS_DATA_WIDTH;
+
+ wire pre_tvalid, pre_tready;
+ wire [DW-1:0] pre_tdata;
+ wire [DW/8-1:0] pre_tstrb, pre_tkeep;
+ wire pre_tlast;
+
+ localparam MAX_COUNT = DW/8;
+ localparam COUNT_BITS = $clog2(MAX_COUNT+1)+1;
+
+ reg [DW-1:0] pck_tdata;
+ reg [DW/8-1:0] pck_tstrb, pck_tkeep;
+ reg pck_tlast;
+ reg [COUNT_BITS-1:0] pck_count;
+
+ reg axis_ready;
+
+ wire skd_valid;
+ wire [DW-1:0] skd_data;
+ wire [DW/8-1:0] skd_strb, skd_keep;
+ wire [COUNT_BITS-1:0] skd_count;
+ wire skd_last;
+
+ reg [COUNT_BITS-1:0] mid_fill;
+ reg [DW-1:0] mid_data;
+ reg [DW/8-1:0] mid_strb, mid_keep;
+ reg mid_last;
+
+ reg [2*DW-1:0] w_packed_data;
+ reg [2*DW/8-1:0] w_packed_strb, w_packed_keep;
+
+ localparam TRIM_MAX = MAX_COUNT[COUNT_BITS-1:0];
+ reg next_valid, next_last;
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Incoming skid buffer
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ // This makes it so that we can control VALID && DATA (and so
+ // backpressure) with a combinatorial value, something that would
+ // otherwise be against protocol.
+ //
+
+`ifdef FORMAL
+ // {{{
+ assign pre_tvalid = S_AXIS_TVALID;
+ assign S_AXIS_TREADY = pre_tready;
+ assign pre_tdata = S_AXIS_TDATA;
+ assign pre_tstrb = S_AXIS_TSTRB;
+ assign pre_tkeep = S_AXIS_TKEEP;
+ assign pre_tlast = S_AXIS_TLAST;
+ // }}}
+`else
+ skidbuffer #(
+ // {{{
+ .DW(DW + DW/8 + DW/8 + 1),
+ .OPT_OUTREG(1'b1)
+ // }}}
+ ) slave_skd (
+ // {{{
+ .i_clk(S_AXI_ACLK),
+ .i_reset(!S_AXI_ARESETN),
+ .i_valid(S_AXIS_TVALID), .o_ready(S_AXIS_TREADY),
+ .i_data({ S_AXIS_TDATA, S_AXIS_TSTRB,
+ S_AXIS_TKEEP, S_AXIS_TLAST }),
+ .o_valid(pre_tvalid), .i_ready(pre_tready),
+ .o_data({ pre_tdata, pre_tstrb, pre_tkeep, pre_tlast })
+ // }}}
+ );
+`endif
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Beat packing stage
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ always @(*)
+ begin
+ { pck_tdata, pck_tstrb, pck_tkeep }
+ = pack( pre_tdata, pre_tstrb,
+ (pre_tvalid) ? pre_tkeep : {(DW/8){1'b0}} );
+ pck_tlast = pre_tlast;
+ // Verilator lint_off WIDTH
+ pck_count = $countones(pre_tkeep);
+ // Verilator lint_on WIDTH
+ end
+
+`ifdef FORMAL
+ // {{{
+ assign skd_valid = pre_tvalid;
+ assign pre_tready = axis_ready;
+ assign skd_data = pck_tdata;
+ assign skd_strb = pck_tstrb;
+ assign skd_keep = pck_tkeep;
+ assign skd_last = pck_tlast;
+ assign skd_count= pck_count;
+ // }}}
+`else
+ skidbuffer #(
+ // {{{
+ .DW(DW + DW/8 + DW/8 + 1 + COUNT_BITS),
+ .OPT_OUTREG(1'b1)
+ // }}}
+ ) beat_skd (
+ // {{{
+ .i_clk(S_AXI_ACLK),
+ .i_reset(!S_AXI_ARESETN),
+ .i_valid(pre_tvalid), .o_ready(pre_tready),
+ .i_data({ pck_count, pck_tdata, pck_tstrb,
+ pck_tkeep, pck_tlast }),
+ .o_valid(skd_valid), .i_ready(axis_ready),
+ .o_data({ skd_count, skd_data, skd_strb, skd_keep,
+ skd_last })
+ // }}}
+ );
+`endif
+
+ function [DW+DW/8+DW/8-1:0] pack; // (i_data, i_strb, i_keep)
+ // {{{
+ input [DW-1:0] i_data;
+ input [DW/8-1:0] i_strb;
+ input [DW/8-1:0] i_keep;
+
+ reg [DW-1:0] p_data;
+ reg [DW/8-1:0] p_strb;
+ reg [DW/8-1:0] p_keep;
+
+ integer rounds, ik;
+ begin
+ p_data = i_data;
+ p_strb = i_strb;
+ p_keep = i_keep;
+ for(ik=0; ik < DW/8; ik=ik+1)
+ begin
+ if (!p_keep[ik])
+ begin
+ p_data[ik*8 +: 8]= 8'h00;
+ p_strb[ik] = 1'b0;
+ end
+ end
+ for(rounds = 0; rounds < DW/8; rounds = rounds+1)
+ begin
+ for(ik=0; ik < DW/8-1; ik=ik+1)
+ begin
+ if (!p_keep[ik])
+ begin
+ p_data[ik*8 +: 8]=p_data[(ik+1)*8 +: 8];
+ p_keep[ik] = p_keep[ik+1];
+ p_strb[ik] = p_strb[ik+1];
+
+ p_keep[ik+1] = 0;
+ p_data[(ik+1)*8 +: 8] = 0;
+ p_strb[ik+1] = 0;
+ end
+ end
+ end
+
+ pack = { p_data, p_strb, p_keep };
+/*
+ p_data = 0;
+ p_strb = 0;
+ p_keep = 0;
+
+ for(fill=0; fill<2*DW; fill=fill+1)
+ begin
+ p_data[(fill *8) +: 8] = i_data[fill*8 +: 8];
+ p_strb[ fill ] = i_strb[fill];
+ p_keep[ fill ] = i_keep[fill];
+ if (fill != 0)
+ p_keep[ fill ] = i_keep[fill]
+ && $countones(i_keep[((fill > 0)?(fill-1):0):0]) == fill;
+ for(ik=fill; ik<2*DW; ik=ik+1)
+ if (i_keep[ik] && $countones(i_keep[ik-1:0]) == fill)
+ begin
+ p_data[fill*8 +: 8] = i_data[ik*8 +: 8];
+ p_strb[fill ] = i_strb[ik];
+ p_keep[fill ] = i_keep[ik];
+ end
+
+ if (!p_keep[fill])
+ begin
+ p_strb[fill] = 1'b0;
+ if (OPT_LOWPOWER)
+ p_data[(fill *8) +: 8] = 8'h00;
+ end
+ end
+
+ pack = { p_data, p_strb, p_keep };
+*/
+ end endfunction
+ // }}}
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Word Packing stage
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ // axis_ready
+ // {{{
+ always @(*)
+ begin
+ axis_ready = 1;
+ if ((mid_last || (skd_count + mid_fill >= TRIM_MAX))
+ &&(M_AXIS_TVALID && !M_AXIS_TREADY))
+ axis_ready = 0;
+ if (!skd_valid)
+ axis_ready = 0;
+ end
+ // }}}
+
+ // mid_fill
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ mid_fill <= 0;
+ else if (mid_last && (!M_AXIS_TVALID || M_AXIS_TREADY))
+ mid_fill <= (axis_ready) ? skd_count : 0;
+ else if (skd_valid && skd_last && (!M_AXIS_TVALID || M_AXIS_TREADY))
+ mid_fill <= (skd_count + mid_fill <= TRIM_MAX) ? 0 : skd_count + mid_fill - TRIM_MAX;
+ else
+ mid_fill <= mid_fill + (axis_ready ? skd_count : 0)
+ - ((next_valid && (!M_AXIS_TVALID || M_AXIS_TREADY))
+ ? TRIM_MAX : 0);
+ // }}}
+
+ // mid_last
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ mid_last <= 0;
+ else if (axis_ready)
+ begin
+ mid_last <= !next_last || (M_AXIS_TVALID && !M_AXIS_TREADY);
+ if (mid_last)
+ mid_last <= 1'b1;
+ if (!skd_last)
+ mid_last <= 1'b0;
+ end else if (!M_AXIS_TVALID || M_AXIS_TREADY)
+ mid_last <= 0;
+ // }}}
+
+ // mid_data, mid_strb, mid_keep
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ begin
+ mid_data <= 0;
+ mid_strb <= 0;
+ mid_keep <= 0;
+ end else if (mid_last && (!M_AXIS_TVALID || M_AXIS_TREADY))
+ begin
+ mid_data <= (axis_ready) ? skd_data : 0;
+ mid_strb <= (axis_ready) ? skd_strb : 0;
+ mid_keep <= (axis_ready) ? skd_keep : 0;
+ end else if (skd_valid && skd_last && (!M_AXIS_TVALID || M_AXIS_TREADY))
+ begin
+ if (skd_count + mid_fill <= TRIM_MAX)
+ begin
+ mid_data <= 0;
+ mid_strb <= 0;
+ mid_keep <= 0;
+ end else begin
+ mid_data <= w_packed_data[2*DW-1:DW];
+ mid_strb <= w_packed_strb[2*DW/8-1:DW/8];
+ mid_keep <= w_packed_keep[2*DW/8-1:DW/8];
+ end
+ end else if (axis_ready)
+ begin
+ if (mid_fill + skd_count >= TRIM_MAX)
+ begin
+ mid_data <= w_packed_data[2*DW-1:DW];
+ mid_strb <= w_packed_strb[2*DW/8-1:DW/8];
+ mid_keep <= w_packed_keep[2*DW/8-1:DW/8];
+ end else begin
+ mid_data <= w_packed_data[DW-1:0];
+ mid_strb <= w_packed_strb[DW/8-1:0];
+ mid_keep <= w_packed_keep[DW/8-1:0];
+ end
+ end
+ // }}}
+
+ // w_packed_data, w_packed_strb, w_packed_keep
+ // {{{
+ always @(*)
+ begin
+ w_packed_data = 0;
+ w_packed_strb = 0;
+
+ w_packed_data = { {(DW){1'b0}}, mid_data }
+ | ( { {(DW){1'b0}}, skd_data } << (mid_fill * 8));
+ w_packed_strb = { {(DW/8){1'b0}}, mid_strb }
+ | ( { {(DW/8){1'b0}}, skd_strb } << (mid_fill));
+ w_packed_keep = { {(DW/8){1'b0}}, mid_keep }
+ | ( { {(DW/8){1'b0}}, skd_keep } << (mid_fill));
+ end
+ // }}}
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Outputs
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ // next_valid
+ // {{{
+ always @(*)
+ begin
+ next_valid = skd_valid && (skd_count + mid_fill >= TRIM_MAX);
+ if (mid_last || (skd_last && skd_valid))
+ next_valid = 1;
+ if (skd_count + mid_fill == 0)
+ next_valid = 0;
+ end
+ // }}}
+
+ // next_last
+ // {{{
+ always @(*)
+ begin
+ next_last = mid_last;
+ if (skd_valid && skd_last && (skd_count + mid_fill <= TRIM_MAX))
+ next_last = 1;
+ if (!next_valid)
+ next_last = 0;
+ end
+ // }}}
+
+ // M_AXIS_TVALID
+ // {{{
+ initial M_AXIS_TVALID = 0;
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ M_AXIS_TVALID <= 0;
+ else if (!M_AXIS_TVALID || M_AXIS_TREADY)
+ M_AXIS_TVALID <= next_valid;
+ // }}}
+
+ // M_AXIS_TDATA, M_AXIS_TSTRB, M_AXIS_TKEEP, M_AXIS_TLAST
+ // {{{
+ initial M_AXIS_TDATA = 0;
+ initial M_AXIS_TSTRB = 0;
+ initial M_AXIS_TKEEP = 0;
+ initial M_AXIS_TLAST = 0;
+ always @(posedge S_AXI_ACLK)
+ if (OPT_LOWPOWER && !S_AXI_ARESETN)
+ begin
+ M_AXIS_TDATA <= 0;
+ M_AXIS_TSTRB <= 0;
+ M_AXIS_TKEEP <= 0;
+ M_AXIS_TLAST <= 0;
+ end else if (!M_AXIS_TVALID || M_AXIS_TREADY)
+ begin
+ if (mid_last)
+ begin
+ M_AXIS_TDATA <= mid_data;
+ M_AXIS_TSTRB <= mid_strb;
+ M_AXIS_TKEEP <= mid_keep;
+ M_AXIS_TLAST <= 1'b1;
+ end else begin
+ M_AXIS_TDATA <= w_packed_data[DW-1:0];
+ M_AXIS_TSTRB <= w_packed_strb[DW/8-1:0];
+ M_AXIS_TKEEP <= w_packed_keep[DW/8-1:0];
+ M_AXIS_TLAST <= next_last;
+ end
+
+
+ if (OPT_LOWPOWER && !next_valid)
+ begin
+ M_AXIS_TDATA <= 0;
+ M_AXIS_TSTRB <= 0;
+ M_AXIS_TKEEP <= 0;
+ M_AXIS_TLAST <= 0;
+ end
+ end
+ // }}}
+
+ // }}}
+ // Keep Verilator happy
+ // {{{
+ // Verilator lint_off UNUSED
+ wire unused;
+ assign unused = &{ 1'b0 };
+ // Verilator lint_on UNUSED
+ // }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal properties
+// {{{
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef FORMAL
+ reg f_past_valid;
+ localparam F_COUNT = COUNT_BITS + 4 + 16;
+ reg [F_COUNT-1:0] f_icount, f_ocount, f_ibeat, f_obeat,
+ f_mcount, f_mbeat;
+
+ initial f_past_valid = 0;
+ always @(posedge S_AXI_ACLK)
+ f_past_valid <= 1;
+
+ always @(*)
+ if (!f_past_valid)
+ assume(!S_AXI_ARESETN);
+
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Incoming stream assumptions
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ always @(posedge S_AXI_ACLK)
+ if (!f_past_valid || $past(!S_AXI_ARESETN))
+ begin
+ assume(!S_AXIS_TVALID);
+ end else if ($past(S_AXIS_TVALID && !S_AXIS_TREADY))
+ begin
+ assume(S_AXIS_TVALID);
+ assume($stable(S_AXIS_TDATA));
+ assume($stable(S_AXIS_TSTRB));
+ assume($stable(S_AXIS_TKEEP));
+ assume($stable(S_AXIS_TLAST));
+ end
+
+ // If TKEEP is low, TSTRB must be low as well
+ always @(*)
+ if (S_AXI_ARESETN)
+ assume(((~S_AXIS_TKEEP) & S_AXIS_TSTRB) == 0);
+
+ // TLAST requires at least one beat
+ always @(*)
+ if (S_AXI_ARESETN && S_AXIS_TVALID && S_AXIS_TLAST)
+ assume(S_AXIS_TKEEP != 0);
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Outgoing stream assertions
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ always @(posedge S_AXI_ACLK)
+ if (!f_past_valid || $past(!S_AXI_ARESETN))
+ begin
+ assert(!M_AXIS_TVALID);
+ end else if ($past(S_AXIS_TVALID && !S_AXIS_TREADY))
+ begin
+ assert(M_AXIS_TVALID);
+ assert($stable(M_AXIS_TDATA));
+ assert($stable(M_AXIS_TSTRB));
+ assert($stable(M_AXIS_TKEEP));
+ assert($stable(M_AXIS_TLAST));
+ end
+
+ // If TKEEP is low, TSTRB must be low as well
+ always @(*)
+ if (S_AXI_ARESETN && M_AXIS_TVALID)
+ assert(((~M_AXIS_TKEEP) & M_AXIS_TSTRB) == 0);
+
+ // Our output requirement is that if TLAST is ever low, TKEEP must
+ // be all ones
+ always @(*)
+ if (S_AXI_ARESETN && M_AXIS_TVALID && !M_AXIS_TLAST)
+ assert(&M_AXIS_TKEEP);
+
+ always @(*)
+ if (S_AXI_ARESETN && OPT_LOWPOWER && !M_AXIS_TVALID)
+ begin
+ assert(M_AXIS_TDATA == 0);
+ assert(M_AXIS_TSTRB == 0);
+ assert(M_AXIS_TKEEP == 0);
+ assert(M_AXIS_TLAST == 0);
+ end
+
+ // TLAST requires at least one beat
+ always @(*)
+ if (S_AXI_ARESETN && M_AXIS_TVALID && M_AXIS_TLAST)
+ assert(M_AXIS_TKEEP != 0);
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Induction assertions for the middle
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+ genvar gk;
+
+ always @(*)
+ if (S_AXI_ARESETN)
+ assert(mid_fill == { 1'b0, $countones(mid_keep) });
+
+ always @(*)
+ if (S_AXI_ARESETN && mid_last)
+ assert(mid_fill > 0);
+
+ // If TKEEP is low, TSTRB must be low as well
+ always @(*)
+ if (S_AXI_ARESETN)
+ begin
+ if (mid_fill > 0)
+ begin
+ assert(((~mid_keep) & mid_strb) == 0);
+ end else begin
+ // assert(mid_data == 0);
+ assert(mid_strb == 0);
+ end
+ end
+
+ // Our output requirement is that if TLAST is ever low, TKEEP must
+ // be all ones
+ generate for(gk=1; gk<DW/8; gk=gk+1)
+ begin
+ always @(*)
+ if (S_AXI_ARESETN && mid_fill > 0 && mid_keep[gk])
+ assert(&mid_keep[gk-1:0]);
+ end endgenerate
+
+ always @(*)
+ if (S_AXI_ARESETN && OPT_LOWPOWER && !M_AXIS_TVALID)
+ begin
+ assert(M_AXIS_TDATA == 0);
+ assert(M_AXIS_TSTRB == 0);
+ assert(M_AXIS_TKEEP == 0);
+ assert(M_AXIS_TLAST == 0);
+ end
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Contract properties
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ // Pick a byte of the given packet. Force that byte to have a known
+ // value. Prove that the same byte on the output has the same known
+ // value.
+
+ (* anyconst *) reg [F_COUNT-1:0] fc_count;
+ (* anyconst *) reg [8-1:0] fc_data;
+ (* anyconst *) reg fc_strb, fc_last;
+ wire [F_COUNT:0] f_chk_count;
+
+ // Assume the special input
+ // {{{
+ generate for(gk=0; gk<DW/8; gk=gk+1)
+ begin
+ if (gk == 0)
+ begin
+ always @(*)
+ if (S_AXIS_TVALID && S_AXIS_TKEEP[0]
+ && f_icount == fc_count)
+ begin
+ assume(fc_data == S_AXIS_TDATA[7:0]);
+ assume(fc_strb == S_AXIS_TSTRB[0]);
+ if (fc_last)
+ begin
+ assume(S_AXIS_TKEEP[DW/8-1:1] == 0);
+ assume(S_AXIS_TLAST);
+ end else if (S_AXIS_TLAST)
+ assume(S_AXIS_TKEEP[DW/8-1:1] != 0);
+ end
+ end else begin
+
+ always @(*)
+ if (S_AXIS_TKEEP[gk] && (f_icount
+ // Verilator lint_off WIDTH
+ + $countones(S_AXIS_TKEEP[gk-1:0]) == fc_count))
+ // Verilator lint_on WIDTH
+ begin
+ assume(S_AXIS_TDATA[gk*8 +: 8] == fc_data);
+ assume(S_AXIS_TSTRB[gk] == fc_strb);
+ if (fc_last)
+ begin
+ if (gk < DW/8-1)
+ assume(S_AXIS_TKEEP[DW/8-1:gk+1] == 0);
+ assume(S_AXIS_TLAST);
+ end else if (gk < DW/8-1)
+ begin
+ if (S_AXIS_TLAST)
+ assume(S_AXIS_TKEEP[DW/8-1:gk+1] != 0);
+ end else
+ assume(!S_AXIS_TLAST);
+ end
+ end
+ end endgenerate
+ // }}}
+
+ // Assert the special output
+ // {{{
+ generate for(gk=0; gk<DW/8; gk=gk+1)
+ begin
+ if (gk == 0)
+ begin
+ always @(*)
+ if (S_AXI_ARESETN && M_AXIS_TVALID && M_AXIS_TKEEP[0]
+ && f_ocount == fc_count)
+ begin
+ assert(M_AXIS_TDATA[7:0] == fc_data);
+ assert(M_AXIS_TSTRB[0] == fc_strb);
+ if (fc_last)
+ begin
+ assert(M_AXIS_TKEEP[DW/8-1:1] == 0);
+ assert(M_AXIS_TLAST);
+ end else if (M_AXIS_TLAST)
+ assert(M_AXIS_TKEEP[DW/8-1:1] != 0);
+ end
+ end else begin
+
+ always @(*)
+ if (S_AXI_ARESETN && M_AXIS_TKEEP[gk] &&
+ // Verilator lint_off WIDTH
+ (f_ocount + $countones(M_AXIS_TKEEP[gk-1:0])
+ == fc_count))
+ // Verilator lint_on WIDTH
+ begin
+ assert(M_AXIS_TDATA[gk*8 +: 8] == fc_data);
+ assert(M_AXIS_TSTRB[gk] == fc_strb);
+ if (fc_last)
+ begin
+ if (gk < DW/8-1)
+ assert(M_AXIS_TKEEP[DW/8-1:gk+1] == 0);
+ assert(M_AXIS_TLAST);
+ end else if (gk < DW/8-1)
+ begin
+ if (M_AXIS_TLAST)
+ assert(M_AXIS_TKEEP[DW/8-1:gk+1] != 0);
+ end else
+ assert(!M_AXIS_TLAST);
+ end
+ end
+ end endgenerate
+ // }}}
+
+ // f_icount
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ f_icount <= 0;
+ else if (S_AXIS_TVALID && S_AXIS_TREADY)
+ // Verilator lint_off WIDTH
+ f_icount <= f_icount + $countones(S_AXIS_TKEEP);
+ // Verilator lint_on WIDTH
+ // }}}
+
+ // f_ocount
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ f_ocount <= 0;
+ else if (M_AXIS_TVALID && M_AXIS_TREADY)
+ // Verilator lint_off WIDTH
+ f_ocount <= f_ocount + $countones(M_AXIS_TKEEP);
+ // Verilator lint_on WIDTH
+ // }}}
+
+ // Induction assertion(s) on mid_*
+ // {{{
+ always @(*)
+ // Verilator lint_off WIDTH
+ f_mcount = f_icount - mid_fill;
+ // Verilator lint_on WIDTH
+
+ generate for(gk=0; gk<DW/8; gk=gk+1)
+ begin
+ if (gk == 0)
+ begin
+ always @(*)
+ if (S_AXI_ARESETN && mid_fill > 0
+ && f_mcount == fc_count)
+ begin
+ assert(mid_data[7:0] == fc_data);
+ assert(mid_strb[0] == fc_strb);
+ assert(mid_keep[0]);
+ if (fc_last)
+ begin
+ assert(mid_fill == 1);
+ assert(mid_last);
+ end else if (mid_last)
+ assert(mid_fill > 1);
+ end else if (S_AXI_ARESETN && mid_fill == 0)
+ begin
+ assert(mid_data[7:0] == 8'h00);
+ assert(!mid_strb[0]);
+ assert(!mid_keep[0]);
+ end
+ end else begin
+
+ always @(*)
+ if (S_AXI_ARESETN && mid_fill > gk
+ && (f_mcount + gk == fc_count))
+ begin
+ assert(mid_data[gk*8 +: 8] == fc_data);
+ assert(mid_strb[gk] == fc_strb);
+ assert(mid_keep[gk]);
+ if (fc_last)
+ begin
+ assert(mid_fill == gk + 1);
+ assert(mid_last);
+ end else if (gk < DW/8-1)
+ begin
+ if (mid_last)
+ assert(mid_fill > gk + 1);
+ end else
+ assert(!mid_last);
+ end else if (S_AXI_ARESETN && mid_fill <= gk)
+ begin
+ assert(mid_data[gk*8 +: 8] == 8'h00);
+ assert(!mid_strb[gk]);
+ assert(!mid_keep[gk]);
+ end
+ end
+ end endgenerate
+ // }}}
+
+ // Relate icount to ocount
+ // {{{
+ // Verilator lint_off WIDTH
+ assign f_chk_count = f_ocount + mid_fill + $countones(M_AXIS_TKEEP);
+ // Verilator lint_on WIDTH
+
+ always @(*)
+ if (S_AXI_ARESETN)
+ begin
+ assume(f_chk_count[F_COUNT] == 1'b0);
+ assert(f_icount == f_chk_count[F_COUNT-1:0]);
+ end
+ // }}}
+
+ // f_ibeat
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ f_ibeat <= 0;
+ else if (S_AXIS_TVALID && S_AXIS_TREADY)
+ begin
+ // Verilator lint_off WIDTH
+ f_ibeat <= f_ibeat + $countones(S_AXIS_TKEEP);
+ // Verilator lint_on WIDTH
+ if (M_AXIS_TLAST)
+ f_ibeat <= 0;
+ end
+ // }}}
+
+ // f_obeat
+ // {{{
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN)
+ f_obeat <= 0;
+ else if (M_AXIS_TVALID && M_AXIS_TREADY)
+ begin
+ // Verilator lint_off WIDTH
+ f_obeat <= f_obeat + $countones(M_AXIS_TKEEP);
+ // Verilator lint_on WIDTH
+ if (M_AXIS_TLAST)
+ f_obeat <= 0;
+ end
+ // }}}
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Cover checks
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ always @(posedge S_AXI_ACLK)
+ if (S_AXI_ARESETN && $past(S_AXI_ARESETN))
+ cover(M_AXIS_TVALID && M_AXIS_TREADY && M_AXIS_TLAST
+ && $past(M_AXIS_TVALID&& M_AXIS_TREADY&& M_AXIS_TLAST));
+
+ always @(posedge S_AXI_ACLK)
+ if (S_AXI_ARESETN && $past(S_AXI_ARESETN))
+ cover(M_AXIS_TVALID && !M_AXIS_TLAST
+ && $past(M_AXIS_TVALID&& M_AXIS_TREADY&& M_AXIS_TLAST));
+
+ always @(posedge S_AXI_ACLK)
+ if (S_AXI_ARESETN && $past(S_AXI_ARESETN))
+ cover(M_AXIS_TVALID && M_AXIS_TLAST
+ && $past(M_AXIS_TVALID&& M_AXIS_TREADY&&!M_AXIS_TLAST));
+
+ // }}}
+
+ // Keep Verilator happy
+ // {{{
+ // Verilator lint_off UNUSED
+ wire unused_formal;
+ assign unused_formal = &{ 1'b0, f_ibeat, f_obeat, f_icount, f_ocount };
+ // Verilator lint_on UNUSED
+ // }}}
+`endif // FORMAL
+// }}}
+endmodule
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 06:58:55 +0000