summaryrefslogtreecommitdiff
path: root/rtl/wb2axip/axivdisplay.v
diff options
context:
space:
mode:
Diffstat (limited to 'rtl/wb2axip/axivdisplay.v')
-rw-r--r--rtl/wb2axip/axivdisplay.v1438
1 files changed, 1438 insertions, 0 deletions
diff --git a/rtl/wb2axip/axivdisplay.v b/rtl/wb2axip/axivdisplay.v
new file mode 100644
index 0000000..aac6c62
--- /dev/null
+++ b/rtl/wb2axip/axivdisplay.v
@@ -0,0 +1,1438 @@
+////////////////////////////////////////////////////////////////////////////////
+//
+// Filename: axivdisplay
+// {{{
+// Project: WB2AXIPSP: bus bridges and other odds and ends
+//
+// Purpose: Reads from memory for the purposes of serving a video frame
+// {{{
+// buffer. The result of this core is an AXI stream having the
+// word size of the memory interface in the first place. TLAST is set
+// based upon the end of the frame, and TUSER based upon the end of the
+// line. An option exists to use Xilinx's encoding instead where TLAST
+// is the end of the line and TUSER is the first pixel word of the frame.
+//
+// This core is in many ways similar to the AXI MM2S core, but with some
+// key differences: The AXI MM2S core generates a single transfer. This
+// core generates a repeating set of transfers--one per line, repeated
+// per frame.
+//
+// To insure high bandwidth, data is first copied into a FIFO of twice
+// the width of the longest burst.
+//
+// }}}
+// Registers:
+// {{{
+// 0: FBUF_CONTROL and status
+// bit 0: START(1)/STOP(0)
+// Command the core to start by writing a '1' to this bit. It
+// will then remain busy/active until either you tell it to halt,
+// or an error occurrs.
+// bit 1: BUSY
+// bit 2: ERR
+// If the core receives a bus error, it assumes it has been
+// inappropriately set up, sets this error bit and then halts.
+// It will not start again until this bit is cleared. Only a
+// write to the control register with the ERR bit set will clear
+// it. (Don't do this unless you know what caused it to halt ...)
+// bit 3: DIRTY
+// If you update core parameters while it is running, the busy
+// bit will be set. This bit is an indication that the current
+// configuration doesn't necessarily match the one you are reading
+// out. To clear DIRTY, deactivate the core, wait for it to be
+// no longer busy, and then start it again. This will also start
+// it under the new configuration so the two match.
+//
+// 2: FBUF_LINESTEP
+// Controls the distance from one line to the next. This is the
+// value added to the address of the beginning of the line to get
+// to the beginning of the next line. This should nominally be
+// equal to the number of bytes per line, although it doesn't
+// need to be.
+//
+// Any attempt to set this value to zero will simply copy the
+// number of data bytes per line into this value.
+//
+// 4: FBUF_LINEBYTES
+// This is the number of data bytes necessary to capture all of
+// the video data in a line. This value must be more than zero
+// in order to activate the core.
+//
+// At present, this core can only handle a number of bytes aligned
+// with the word size of the bus.
+//
+// 6: FBUF_NUMLINES
+// The number of lines of active video data in a frame. This
+// number must be greater than zero in order to activate and
+// operate the core.
+//
+// 8: FBUF_ADDRESS
+// The is the first address of video data in memory. Each frame
+// will start reading from this address.
+//
+// 12: (reserved for the upper FBUF_ADDRESS)
+//
+// BUGS:
+// 1. Memory reads are currently allowed to wrap around the end of memory.
+// I'm not (yet) sure if this is a good thing or a bad thing. I mean, its
+// a great thing for small dedicated memories designated for this purpose
+// alone, but perhaps a bad thing if the memory space is shared with
+// peripherals as well as a CPU.
+//
+// 2. I'd still like to add an option to handle memory addresses that
+// aren't aligned. Until that is done, the means of interacting with the
+// core will change from one implementation to another.
+//
+// 3. If the configuration changes mid-write, but without de-activating
+// the core and waiting for it to come to idle, the synchronization flags
+// might out-of-sync with the pixels. To resolve, deactivate the core and
+// let it come to whenever changing configuration parameters.
+// }}}
+//
+// Creator: Dan Gisselquist, Ph.D.
+// Gisselquist Technology, LLC
+//
+////////////////////////////////////////////////////////////////////////////////
+// }}}
+// Copyright (C) 2020-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 axivdisplay #(
+ // {{{
+ parameter C_AXI_ADDR_WIDTH = 32,
+ parameter C_AXI_DATA_WIDTH = 32,
+ parameter C_AXI_ID_WIDTH = 1,
+ //
+ // We support five 32-bit AXI-lite registers, requiring 5-bits
+ // of AXI-lite addressing
+ localparam C_AXIL_ADDR_WIDTH = 4,
+ localparam C_AXIL_DATA_WIDTH = 32,
+ //
+ // The bottom ADDRLSB bits of any AXI address are subword bits
+ localparam ADDRLSB = $clog2(C_AXI_DATA_WIDTH)-3,
+ localparam AXILLSB = $clog2(C_AXIL_DATA_WIDTH)-3,
+ //
+ // OPT_UNALIGNED: Allow unaligned accesses, address requests
+ // and sizes which may or may not match the underlying data
+ // width. If set, the core will quietly align these requests.
+ // parameter [0:0] OPT_UNALIGNED = 1'b0,
+ //
+ // OPT_LGMAXBURST
+ parameter OPT_LGMAXBURST = 8,
+ //
+ parameter [0:0] DEF_ACTIVE_ON_RESET = 0,
+ parameter [15:0] DEF_LINES_PER_FRAME = 1024,
+ parameter [16-ADDRLSB-1:0] DEF_WORDS_PER_LINE = (1280 * 32)/C_AXI_DATA_WIDTH,
+ //
+ // DEF_FRAMEADDR: the default AXI address of the frame buffer
+ // containing video memory. Unless OPT_UNALIGNED is set, this
+ // should be aligned so that DEF_FRAMEADDR[ADDRLSB-1:0] == 0.
+ parameter [C_AXI_ADDR_WIDTH-1:0] DEF_FRAMEADDR = 0,
+ //
+ // The (log-based two of the) size of the FIFO in words.
+ // I like to set this to the size of two AXI bursts, so that
+ // while one is being read out the second can be read in. Can
+ // also be set larger if desired.
+ parameter LGFIFO = OPT_LGMAXBURST+1,
+ //
+ // AXI_ID is the ID we will use for all of our AXI transactions
+ parameter AXI_ID = 0,
+ //
+ // OPT_TUSER_IS_SOF. Xilinx and I chose different stream
+ // encodings. I encode TLAST== VLAST and
+ // TUSER == (optional) HLAST. Xilinx chose TLAST == HLAST
+ // and TUSER == SOF(start of frame). Set OPT_TUSER_IS_SOF to
+ // use Xilinx's encoding.
+ parameter [0:0] OPT_TUSER_IS_SOF = 0
+ // }}}
+ ) (
+ // {{{
+ input wire S_AXI_ACLK,
+ input wire S_AXI_ARESETN,
+ //
+ // The video stream interface
+ // {{{
+ output wire M_AXIS_TVALID,
+ input wire M_AXIS_TREADY,
+ output wire [C_AXI_DATA_WIDTH-1:0] M_AXIS_TDATA,
+ output wire /* VLAST or HLAST */ M_AXIS_TLAST,
+ output wire /* HLAST or SOF */ M_AXIS_TUSER,
+ // }}}
+ //
+ // The control interface
+ // {{{
+ input wire S_AXIL_AWVALID,
+ output wire S_AXIL_AWREADY,
+ input wire [C_AXIL_ADDR_WIDTH-1:0] S_AXIL_AWADDR,
+ input wire [2:0] S_AXIL_AWPROT,
+ //
+ input wire S_AXIL_WVALID,
+ output wire S_AXIL_WREADY,
+ input wire [C_AXIL_DATA_WIDTH-1:0] S_AXIL_WDATA,
+ input wire [C_AXIL_DATA_WIDTH/8-1:0] S_AXIL_WSTRB,
+ //
+ output wire S_AXIL_BVALID,
+ input wire S_AXIL_BREADY,
+ output wire [1:0] S_AXIL_BRESP,
+ //
+ input wire S_AXIL_ARVALID,
+ output wire S_AXIL_ARREADY,
+ input wire [C_AXIL_ADDR_WIDTH-1:0] S_AXIL_ARADDR,
+ input wire [2:0] S_AXIL_ARPROT,
+ //
+ output wire S_AXIL_RVALID,
+ input wire S_AXIL_RREADY,
+ output wire [C_AXIL_DATA_WIDTH-1:0] S_AXIL_RDATA,
+ output wire [1:0] S_AXIL_RRESP,
+ // }}}
+ //
+
+ //
+ // The AXI (full) read interface
+ // {{{
+ output wire M_AXI_ARVALID,
+ input wire M_AXI_ARREADY,
+ output wire [C_AXI_ID_WIDTH-1:0] M_AXI_ARID,
+ output wire [C_AXI_ADDR_WIDTH-1:0] M_AXI_ARADDR,
+ output wire [7:0] M_AXI_ARLEN,
+ output wire [2:0] M_AXI_ARSIZE,
+ output wire [1:0] M_AXI_ARBURST,
+ output wire M_AXI_ARLOCK,
+ output wire [3:0] M_AXI_ARCACHE,
+ output wire [2:0] M_AXI_ARPROT,
+ output wire [3:0] M_AXI_ARQOS,
+ //
+ input wire M_AXI_RVALID,
+ output wire M_AXI_RREADY,
+ input wire [C_AXI_DATA_WIDTH-1:0] M_AXI_RDATA,
+ input wire M_AXI_RLAST,
+ input wire [C_AXI_ID_WIDTH-1:0] M_AXI_RID,
+ input wire [1:0] M_AXI_RRESP
+ // }}}
+ // }}}
+ );
+
+ // Core logic implementation
+ // {{{
+ // Local parameter declarations
+ // {{{
+ localparam [1:0] FBUF_CONTROL = 2'b00,
+ FBUF_FRAMEINFO = 2'b01,
+ FBUF_ADDRLO = 2'b10,
+ FBUF_ADDRHI = 2'b11;
+
+ localparam CBIT_ACTIVE = 0,
+ CBIT_BUSY = 1,
+ CBIT_ERR = 2,
+ CBIT_DIRTY = 3;
+
+ localparam TMPLGMAXBURST=(LGFIFO-1 > OPT_LGMAXBURST)
+ ? OPT_LGMAXBURST : LGFIFO-1;
+
+ localparam LGMAXBURST = (TMPLGMAXBURST+ADDRLSB > 12)
+ ? (12-ADDRLSB) : TMPLGMAXBURST;
+ // }}}
+
+ wire i_clk = S_AXI_ACLK;
+ wire i_reset = !S_AXI_ARESETN;
+
+ // Signal declarations
+ // {{{
+ reg soft_reset, r_err, r_stopped;
+ reg cfg_active, cfg_zero_length, cfg_dirty;
+ reg [C_AXI_ADDR_WIDTH-1:0] cfg_frame_addr;
+ reg [15:0] cfg_frame_lines, cfg_line_step;
+ reg [16-ADDRLSB-1:0] cfg_line_words;
+
+ // FIFO signals
+ wire reset_fifo, write_to_fifo,
+ read_from_fifo;
+ wire [C_AXI_DATA_WIDTH-1:0] write_data;
+ wire [LGFIFO:0] fifo_fill;
+ wire fifo_full, fifo_empty;
+
+ wire awskd_valid, axil_write_ready;
+ wire [C_AXIL_ADDR_WIDTH-AXILLSB-1:0] awskd_addr;
+ //
+ wire wskd_valid;
+ wire [C_AXIL_DATA_WIDTH-1:0] wskd_data;
+ wire [C_AXIL_DATA_WIDTH/8-1:0] wskd_strb;
+ reg axil_bvalid;
+ //
+ wire arskd_valid, axil_read_ready;
+ wire [C_AXIL_ADDR_WIDTH-AXILLSB-1:0] arskd_addr;
+ reg [C_AXIL_DATA_WIDTH-1:0] axil_read_data;
+ reg axil_read_valid;
+ reg [C_AXIL_DATA_WIDTH-1:0] w_status_word;
+ reg [2*C_AXIL_DATA_WIDTH-1:0] wide_address, new_wideaddr;
+ wire [C_AXIL_DATA_WIDTH-1:0] new_cmdaddrlo, new_cmdaddrhi;
+ reg [C_AXIL_DATA_WIDTH-1:0] wide_config;
+ wire [C_AXIL_DATA_WIDTH-1:0] new_config;
+
+ // reg partial_burst_requested;
+ // reg [LGMAXBURST-1:0] addralign;
+ // reg [LGFIFO:0] rd_uncommitted;
+ // reg [LGMAXBURST:0] initial_burstlen;
+ // reg [LGLENWA-1:0] rd_reads_remaining;
+ // reg rd_none_remaining,
+ // rd_last_remaining;
+
+ // wire realign_last_valid;
+
+ reg axi_arvalid, lag_start, phantom_start, start_burst,
+ ar_none_outstanding;
+ reg [C_AXI_ADDR_WIDTH-1:0] axi_araddr;
+ reg [LGMAXBURST:0] max_burst;
+ reg [7:0] axi_arlen;
+ reg [15:0] ar_bursts_outstanding;
+ //
+ wire vlast, hlast;
+ reg [15:0] r_frame_lines, r_line_step;
+ reg [16-ADDRLSB-1:0] r_line_words;
+
+ reg req_hlast, req_vlast;
+ reg [15:0] req_nlines;
+ reg [16-ADDRLSB-1:0] req_line_words;
+ reg [C_AXI_ADDR_WIDTH:0] req_addr, req_line_addr;
+ //
+ reg rd_hlast, rd_vlast;
+ reg [15:0] rd_lines;
+ reg [16-ADDRLSB-1:0] rd_line_beats;
+ wire no_fifo_space_available;
+ //
+ reg [LGMAXBURST-1:0] till_boundary;
+ reg [LGFIFO:0] fifo_space_available;
+
+
+`ifdef FORMAL
+ reg [C_AXI_ADDR_WIDTH:0] f_rd_line_addr, f_rd_addr;
+`endif
+
+ wire M_AXIS_VLAST, M_AXIS_HLAST;
+ // }}}
+
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // AXI-lite signaling
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // This is mostly the skidbuffer logic, and handling of the VALID
+ // and READY signals for the AXI-lite control logic in the next
+ // section.
+ // {{{
+
+ //
+ // Write signaling
+ //
+ // {{{
+
+ skidbuffer #(.OPT_OUTREG(0), .DW(C_AXIL_ADDR_WIDTH-AXILLSB))
+ axilawskid(//
+ .i_clk(S_AXI_ACLK), .i_reset(i_reset),
+ .i_valid(S_AXIL_AWVALID), .o_ready(S_AXIL_AWREADY),
+ .i_data(S_AXIL_AWADDR[C_AXIL_ADDR_WIDTH-1:AXILLSB]),
+ .o_valid(awskd_valid), .i_ready(axil_write_ready),
+ .o_data(awskd_addr));
+
+ skidbuffer #(.OPT_OUTREG(0), .DW(C_AXIL_DATA_WIDTH+C_AXIL_DATA_WIDTH/8))
+ axilwskid(//
+ .i_clk(S_AXI_ACLK), .i_reset(i_reset),
+ .i_valid(S_AXIL_WVALID), .o_ready(S_AXIL_WREADY),
+ .i_data({ S_AXIL_WDATA, S_AXIL_WSTRB }),
+ .o_valid(wskd_valid), .i_ready(axil_write_ready),
+ .o_data({ wskd_data, wskd_strb }));
+
+ assign axil_write_ready = awskd_valid && wskd_valid
+ && (!S_AXIL_BVALID || S_AXIL_BREADY);
+
+ initial axil_bvalid = 0;
+ always @(posedge i_clk)
+ if (i_reset)
+ axil_bvalid <= 0;
+ else if (axil_write_ready)
+ axil_bvalid <= 1;
+ else if (S_AXIL_BREADY)
+ axil_bvalid <= 0;
+
+ assign S_AXIL_BVALID = axil_bvalid;
+ assign S_AXIL_BRESP = 2'b00;
+ // }}}
+
+ //
+ // Read signaling
+ //
+ // {{{
+ skidbuffer #(.OPT_OUTREG(0), .DW(C_AXIL_ADDR_WIDTH-AXILLSB))
+ axilarskid(//
+ .i_clk(S_AXI_ACLK), .i_reset(i_reset),
+ .i_valid(S_AXIL_ARVALID), .o_ready(S_AXIL_ARREADY),
+ .i_data(S_AXIL_ARADDR[C_AXIL_ADDR_WIDTH-1:AXILLSB]),
+ .o_valid(arskd_valid), .i_ready(axil_read_ready),
+ .o_data(arskd_addr));
+
+ assign axil_read_ready = arskd_valid
+ && (!axil_read_valid || S_AXIL_RREADY);
+
+ initial axil_read_valid = 1'b0;
+ always @(posedge i_clk)
+ if (i_reset)
+ axil_read_valid <= 1'b0;
+ else if (axil_read_ready)
+ axil_read_valid <= 1'b1;
+ else if (S_AXIL_RREADY)
+ axil_read_valid <= 1'b0;
+
+ assign S_AXIL_RVALID = axil_read_valid;
+ assign S_AXIL_RDATA = axil_read_data;
+ assign S_AXIL_RRESP = 2'b00;
+ // }}}
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // AXI-lite controlled logic
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+
+ //
+ // soft_reset, r_err
+ // {{{
+ initial soft_reset = 1;
+ always @(posedge i_clk)
+ if (i_reset)
+ begin
+ soft_reset <= 1;
+ r_err <= 0;
+ end else if (soft_reset)
+ begin
+
+ if ((axil_write_ready && awskd_addr == FBUF_CONTROL)
+ && wskd_strb[0] && wskd_data[CBIT_ERR])
+ r_err <= cfg_zero_length;
+
+ if (cfg_active && !r_err && r_stopped)
+ soft_reset <= 0;
+
+ end else // if (!soft_reset)
+ begin
+ // Halt on any bus error. We'll require user intervention
+ // to start back up again
+ if (M_AXI_RREADY && M_AXI_RVALID && M_AXI_RRESP[1])
+ begin
+ soft_reset <= 1;
+ r_err <= 1;
+ end
+
+ // Halt on any user request
+ if (!cfg_active)
+ soft_reset <= 1;
+ end
+ // }}}
+
+ // wide_* and new_* write setup registers
+ // {{{
+ always @(*)
+ begin
+ wide_address = 0;
+ wide_address[C_AXI_ADDR_WIDTH-1:0] = cfg_frame_addr;
+ wide_address[ADDRLSB-1:0] = 0;
+
+ wide_config = { cfg_frame_lines, cfg_line_words,
+ {(ADDRLSB){1'b0}} };
+ end
+
+ assign new_cmdaddrlo = apply_wstrb(
+ wide_address[C_AXIL_DATA_WIDTH-1:0],
+ wskd_data, wskd_strb);
+
+ generate if (C_AXI_ADDR_WIDTH > 32)
+ begin : GEN_LARGE_AW
+
+ assign new_cmdaddrhi = apply_wstrb(
+ wide_address[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH],
+ wskd_data, wskd_strb);
+
+ end else begin : GEN_SINGLE_WORD_AW
+
+ assign new_cmdaddrhi = 0;
+
+ end endgenerate
+
+
+ wire [C_AXIL_DATA_WIDTH-1:0] new_control;
+ assign new_control = apply_wstrb(w_status_word, wskd_data, wskd_strb);
+ assign new_config = apply_wstrb(wide_config, wskd_data, wskd_strb);
+
+ always @(*)
+ begin
+ new_wideaddr = wide_address;
+
+ if (awskd_addr == FBUF_ADDRLO)
+ new_wideaddr[C_AXIL_DATA_WIDTH-1:0] = new_cmdaddrlo;
+ if (awskd_addr == FBUF_ADDRHI)
+ new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH] = new_cmdaddrhi;
+ new_wideaddr[ADDRLSB-1:0] = 0;
+ new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH] = 0;
+ end
+ // }}}
+
+ // Configuration registers (Write)
+ // {{{
+ initial cfg_active = 0;
+ initial cfg_frame_addr = DEF_FRAMEADDR;
+ initial cfg_frame_addr[ADDRLSB-1:0] = 0;
+ initial cfg_line_words = DEF_WORDS_PER_LINE;
+ initial cfg_frame_lines = DEF_LINES_PER_FRAME;
+ initial cfg_zero_length = (DEF_WORDS_PER_LINE == 0)
+ ||(DEF_LINES_PER_FRAME == 0);
+ always @(posedge i_clk)
+ if (i_reset)
+ begin
+ cfg_active <= DEF_ACTIVE_ON_RESET;
+ cfg_frame_addr <= DEF_FRAMEADDR;
+ cfg_line_words <= DEF_WORDS_PER_LINE;
+ cfg_line_step <= { DEF_WORDS_PER_LINE, {(ADDRLSB){1'b0}} };
+ cfg_frame_lines <= DEF_LINES_PER_FRAME;
+ cfg_zero_length <= (DEF_WORDS_PER_LINE==0)
+ ||(DEF_LINES_PER_FRAME == 0);
+ cfg_dirty <= 0;
+ end else begin
+ if (r_stopped)
+ cfg_dirty <= 0;
+ if (cfg_active && req_hlast && req_vlast && phantom_start)
+ cfg_dirty <= 0;
+ if (M_AXI_RREADY && M_AXI_RVALID && M_AXI_RRESP[1])
+ cfg_active <= 0;
+
+ if (axil_write_ready)
+ case(awskd_addr)
+ FBUF_CONTROL: begin
+ if (wskd_strb[0])
+ cfg_active <= wskd_data[CBIT_ACTIVE]
+ && (!r_err || wskd_data[CBIT_ERR])
+ && (!cfg_zero_length);
+
+ if (new_control[31:16] == 0)
+ begin
+ cfg_line_step <= 0;
+ cfg_line_step[16-1:ADDRLSB] <= cfg_line_words;
+ // Verilator lint_off WIDTH
+ cfg_dirty <= (cfg_line_step
+ != (cfg_line_words << ADDRLSB));
+ // Verilator lint_on WIDTH
+ end else begin
+ cfg_line_step <= new_control[31:16];
+ cfg_dirty <= (cfg_line_step != new_control[31:16]);
+ end end
+ FBUF_FRAMEINFO: begin
+ { cfg_frame_lines, cfg_line_words }
+ <= new_config[C_AXI_DATA_WIDTH-1:ADDRLSB];
+ cfg_zero_length <= (new_config[31:16] == 0)
+ ||(new_config[15:ADDRLSB] == 0);
+ if ((new_config[31:16] == 0)
+ ||(new_config[15:ADDRLSB] == 0))
+ cfg_active <= 0;
+ cfg_dirty <= 1;
+ end
+ FBUF_ADDRLO, FBUF_ADDRHI: begin
+ cfg_frame_addr <= new_wideaddr[C_AXI_ADDR_WIDTH-1:0];
+ cfg_dirty <= 1;
+ end
+ default: begin end
+ endcase
+ end
+ // }}}
+
+ // AXI-Lite read register data
+ // {{{
+ always @(*)
+ begin
+ w_status_word = 0;
+ w_status_word[31:16] = cfg_line_step;
+ w_status_word[CBIT_DIRTY] = cfg_dirty;
+ w_status_word[CBIT_ERR] = r_err;
+ w_status_word[CBIT_BUSY] = !soft_reset;
+ w_status_word[CBIT_ACTIVE] = cfg_active || (!soft_reset || !r_stopped);
+ end
+
+ always @(posedge i_clk)
+ if (!axil_read_valid || S_AXIL_RREADY)
+ begin
+ axil_read_data <= 0;
+ case(arskd_addr)
+ FBUF_CONTROL: axil_read_data <= w_status_word;
+ FBUF_FRAMEINFO: axil_read_data <= { cfg_frame_lines,
+ cfg_line_words, {(ADDRLSB){1'b0}} };
+ FBUF_ADDRLO: axil_read_data <= wide_address[C_AXIL_DATA_WIDTH-1:0];
+ FBUF_ADDRHI: axil_read_data <= wide_address[2*C_AXIL_DATA_WIDTH-1:C_AXIL_DATA_WIDTH];
+ default axil_read_data <= 0;
+ endcase
+ end
+ // }}}
+
+ // apply_wstrb function for applying wstrbs to register words
+ // {{{
+ function [C_AXIL_DATA_WIDTH-1:0] apply_wstrb;
+ input [C_AXIL_DATA_WIDTH-1:0] prior_data;
+ input [C_AXIL_DATA_WIDTH-1:0] new_data;
+ input [C_AXIL_DATA_WIDTH/8-1:0] wstrb;
+
+ integer k;
+ for(k=0; k<C_AXIL_DATA_WIDTH/8; k=k+1)
+ begin
+ apply_wstrb[k*8 +: 8]
+ = wstrb[k] ? new_data[k*8 +: 8] : prior_data[k*8 +: 8];
+ end
+ endfunction
+ // }}}
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // The data FIFO section
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+ // {{{
+ assign reset_fifo = r_stopped;
+
+ assign write_to_fifo = M_AXI_RVALID;
+ assign write_data = M_AXI_RDATA;
+ // assign realign_last_valid = 0;
+ assign vlast = rd_vlast;
+ assign hlast = rd_hlast;
+ assign M_AXI_RREADY = !fifo_full;
+ // }}}
+
+ generate if (LGFIFO > 0)
+ begin : GEN_SPACE_AVAILBLE
+ // Here's where we'll put the actual outgoing FIFO
+ // {{{
+ initial fifo_space_available = (1<<LGFIFO);
+ always @(posedge i_clk)
+ if (reset_fifo)
+ fifo_space_available <= (1<<LGFIFO);
+ else case({phantom_start, read_from_fifo && !fifo_empty })
+ 2'b00: begin end
+ // Verilator lint_off WIDTH
+ 2'b10: fifo_space_available <= fifo_space_available - (M_AXI_ARLEN+1);
+ 2'b11: fifo_space_available <= fifo_space_available - (M_AXI_ARLEN);
+ // Verilator lint_on WIDTH
+ 2'b01: fifo_space_available <= fifo_space_available + 1;
+ endcase
+
+ assign M_AXIS_TVALID = !fifo_empty;
+ assign read_from_fifo = M_AXIS_TVALID && M_AXIS_TREADY;
+
+ sfifo #(.BW(C_AXI_DATA_WIDTH+2), .LGFLEN(LGFIFO))
+ sfifo(i_clk, reset_fifo,
+ write_to_fifo, { vlast && hlast, hlast, write_data },
+ fifo_full, fifo_fill,
+ read_from_fifo, { M_AXIS_VLAST, M_AXIS_HLAST,
+ M_AXIS_TDATA }, fifo_empty);
+
+ assign no_fifo_space_available = (fifo_space_available < (1<<LGMAXBURST));
+ // }}}
+ end else begin : NO_FIFO
+ // {{{
+ assign fifo_full = !M_AXIS_TREADY;
+ assign fifo_fill = 0;
+ assign fifo_empty = !M_AXIS_TVALID;
+ assign M_AXIS_TVALID = write_to_fifo;
+
+ assign M_AXIS_VLAST = vlast && hlast;
+ assign M_AXIS_HLAST = hlast;
+ assign M_AXIS_TDATA = M_AXI_RDATA;
+
+ assign no_fifo_space_available = (ar_bursts_outstanding >= 3);
+ // }}}
+ end endgenerate
+ // }}}
+
+ // Switch between TLAST/TUSER encodings if necessary
+ // {{{
+ generate if (OPT_TUSER_IS_SOF)
+ begin : XILINX_ENCODING
+
+ reg SOF;
+
+ initial SOF = 1'b1;
+ always @(posedge S_AXI_ACLK)
+ if (!S_AXI_ARESETN || r_stopped)
+ SOF <= 1'b1;
+ else if (M_AXIS_TVALID && M_AXIS_TREADY)
+ SOF <= M_AXIS_VLAST;
+
+ assign M_AXIS_TLAST = M_AXIS_HLAST;
+ assign M_AXIS_TUSER = SOF;
+
+ end else begin : VLAST_EQUALS_TLAST
+
+ assign M_AXIS_TLAST = M_AXIS_VLAST;
+ assign M_AXIS_TUSER = M_AXIS_HLAST;
+ end endgenerate
+ // }}}
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Outoing frame address counting
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+ // {{{
+ always @(posedge i_clk)
+ if (i_reset || r_stopped || (phantom_start && req_hlast && req_vlast))
+ begin
+ r_frame_lines <= cfg_frame_lines;
+ r_line_words <= cfg_line_words;
+ r_line_step <= { {(ADDRLSB){1'b0}}, cfg_line_step[15:ADDRLSB] };
+ end
+
+ initial req_addr = 0;
+ initial req_line_addr = 0;
+ always @(posedge i_clk)
+ if (i_reset || r_stopped)
+ begin
+ req_addr <= { 1'b0, cfg_frame_addr };
+ req_line_addr <= { 1'b0, cfg_frame_addr };
+ req_line_words <= cfg_line_words;
+ end else if (phantom_start)
+ begin
+ if (req_hlast && req_vlast)
+ begin
+ req_addr <= { 1'b0, cfg_frame_addr };
+ req_line_addr <= { 1'b0, cfg_frame_addr };
+ req_line_words <= cfg_line_words;
+ end else if (req_hlast)
+ begin
+ // verilator lint_off WIDTH
+ req_addr <= req_line_addr
+ + (r_line_step << M_AXI_ARSIZE);
+ req_line_addr <= req_line_addr
+ + (r_line_step << M_AXI_ARSIZE);
+ // verilator lint_on WIDTH
+ req_line_words <= r_line_words;
+ end else begin
+ // verilator lint_off WIDTH
+ req_addr <= req_addr + (1<<(LGMAXBURST+ADDRLSB));
+ req_line_words <= req_line_words - (M_AXI_ARLEN+1);
+ // verilator lint_on WIDTH
+
+ req_addr[LGMAXBURST+ADDRLSB-1:0] <= 0;
+ end
+ end
+
+ always @(posedge i_clk)
+ if (i_reset || r_stopped)
+ begin
+ req_nlines <= cfg_frame_lines-1;
+ req_vlast <= (cfg_frame_lines <= 1);
+ end else if (phantom_start && req_hlast)
+ begin
+ if (req_vlast)
+ begin
+ req_nlines <= cfg_frame_lines-1;
+ req_vlast <= (cfg_frame_lines <= 1);
+ end else begin
+ req_nlines <= req_nlines - 1;
+ req_vlast <= (req_nlines <= 1);
+ end
+ end
+`ifdef FORMAL
+ always @(*)
+ if (!r_stopped)
+ begin
+ assert(req_vlast == (req_nlines == 0));
+ assert(req_addr >= { 1'b0, cfg_frame_addr });
+ assert(req_line_addr >= { 1'b0, cfg_frame_addr });
+ assert(req_line_addr <= req_addr);
+ end
+
+ always @(*)
+ if (cfg_active)
+ begin
+ assert(cfg_frame_lines != 0);
+ assert(cfg_line_words != 0);
+ end
+
+ always @(*)
+ if (!r_stopped)
+ begin
+ assert(r_frame_lines != 0);
+ assert(r_line_words != 0);
+ end
+`endif
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Incoming frame address counting
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+ // {{{
+ always @(posedge i_clk)
+ if (i_reset || r_stopped)
+ begin
+ rd_line_beats <= cfg_line_words-1;
+ rd_hlast <= (cfg_line_words == 1);
+ end else if (M_AXI_RVALID && M_AXI_RREADY)
+ begin
+ if (rd_hlast)
+ begin
+ rd_line_beats <= r_line_words - 1;
+ rd_hlast <= (r_line_words <= 1);
+ end else begin
+ rd_line_beats <= rd_line_beats - 1;
+ rd_hlast <= (rd_line_beats <= 1);
+ end
+ end
+
+ always @(posedge i_clk)
+ if (i_reset || r_stopped)
+ begin
+ rd_lines <= cfg_frame_lines-1;
+ rd_vlast <= (cfg_frame_lines == 1);
+ end else if (M_AXI_RVALID && M_AXI_RREADY && rd_hlast)
+ begin
+ if (vlast)
+ begin
+ rd_lines <= r_frame_lines - 1;
+ rd_vlast <= (r_frame_lines <= 1);
+ end else begin
+ rd_lines <= rd_lines - 1;
+ rd_vlast <= (rd_lines <= 1);
+ end
+ end
+
+`ifdef FORMAL
+ always @(posedge i_clk)
+ if (i_reset || r_stopped)
+ begin
+ f_rd_addr <= { 1'b0, cfg_frame_addr };
+ f_rd_line_addr <= { 1'b0, cfg_frame_addr };
+ end else if (M_AXI_RVALID && M_AXI_RREADY)
+ begin
+ if (rd_vlast && rd_hlast)
+ begin
+ f_rd_addr <= cfg_frame_addr;
+ f_rd_line_addr <= cfg_frame_addr;
+ end else if (rd_hlast)
+ begin
+ f_rd_addr <= f_rd_line_addr + (r_line_step << M_AXI_ARSIZE);
+ f_rd_line_addr <= f_rd_line_addr + (r_line_step << M_AXI_ARSIZE);
+ end else begin
+ f_rd_addr <= f_rd_addr + (1<<ADDRLSB);
+ end
+ end
+`endif
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // The incoming AXI (full) protocol section
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+ // {{{
+
+ // Some counters to keep track of our state
+ // {{{
+
+ // ar_bursts_outstanding
+ // {{{
+ // Count the number of bursts outstanding--these are the number of
+ // ARVALIDs that have been accepted, but for which the RVALID && RLAST
+ // has not (yet) been returned.
+ initial ar_none_outstanding = 1;
+ initial ar_bursts_outstanding = 0;
+ always @(posedge i_clk)
+ if (i_reset)
+ begin
+ ar_bursts_outstanding <= 0;
+ ar_none_outstanding <= 1;
+ end else case ({ phantom_start,
+ M_AXI_RVALID && M_AXI_RREADY && M_AXI_RLAST })
+ 2'b01: begin
+ ar_bursts_outstanding <= ar_bursts_outstanding - 1;
+ ar_none_outstanding <= (ar_bursts_outstanding == 1);
+ end
+ 2'b10: begin
+ ar_bursts_outstanding <= ar_bursts_outstanding + 1;
+ ar_none_outstanding <= 0;
+ end
+ default: begin end
+ endcase
+ // }}}
+
+ // r_stopped
+ // {{{
+ // Following an error or drop of cfg_active, soft_reset will go high.
+ // We then come to a stop once everything becomes inactive
+ initial r_stopped = 1;
+ always @(posedge i_clk)
+ if (i_reset)
+ r_stopped <= 1;
+ else if (r_stopped)
+ r_stopped <= soft_reset || !cfg_active;
+ else if (soft_reset && ar_none_outstanding && !M_AXI_ARVALID)
+ r_stopped <= 1;
+ // }}}
+
+ // }}}
+
+ //
+ // start_burst
+ // {{{
+ always @(*)
+ begin
+ start_burst = 1;
+ if (no_fifo_space_available)
+ start_burst = 0;
+ if (phantom_start || lag_start)
+ // Insist on a minimum of two clocks between burst
+ // starts, so we can get our lengths right
+ start_burst = 0;
+
+ // Can't start a new burst if the outgoing channel is still
+ // stalled.
+ if (M_AXI_ARVALID && !M_AXI_ARREADY)
+ start_burst = 0;
+
+ // If the user wants us to stop, then stop
+ if (!cfg_active || soft_reset)
+ start_burst = 0;
+ end
+ // }}}
+
+ // ARLEN
+ // {{{
+ // Coming in, req_addr and req_line_words can be trusted
+ // lag_start will be true to reflect this
+ always @(posedge i_clk)
+ if (lag_start)
+ begin
+ if (req_line_words >= (1<<LGMAXBURST))
+ max_burst <= (1<<LGMAXBURST);
+ else
+ // Verilator lint_off WIDTH
+ max_burst <= req_line_words;
+ // Verilator lint_on WIDTH
+ end
+
+ always @(*)
+ till_boundary = ~req_addr[ADDRLSB +: LGMAXBURST];
+
+ always @(posedge i_clk)
+ if (!M_AXI_ARVALID || M_AXI_ARREADY)
+ begin
+ // Verilator lint_off WIDTH
+ if (till_boundary > 0 && max_burst <= till_boundary)
+ axi_arlen <= max_burst-1;
+ // Verilator lint_on WIDTH
+ else
+ axi_arlen <= till_boundary;
+ end
+ // }}}
+
+ // req_hlast
+ // {{{
+ always @(posedge i_clk)
+ if (lag_start || start_burst)
+ begin
+ req_hlast <= 1;
+ // Verilator lint_off WIDTH
+ if (req_line_words > till_boundary+1)
+ req_hlast <= 0;
+ if (req_line_words > max_burst)
+ req_hlast <= 0;
+ // Verilator lint_on WIDTH
+ end
+
+`ifdef FORMAL
+ always @(*)
+ if (phantom_start)
+ begin
+ if (req_hlast)
+ begin
+ assert(axi_arlen+1 == req_line_words);
+ end else
+ assert(axi_arlen+1 < req_line_words);
+ end else if (!soft_reset && !r_stopped && !lag_start)
+ begin
+ if (max_burst != req_line_words)
+ begin
+ assert(!req_hlast);
+ end else if (!req_hlast && !M_AXI_ARVALID)
+ assert(axi_arlen < max_burst);
+
+ assert(max_burst > 0);
+ if (req_line_words > (1<<LGMAXBURST))
+ begin
+ assert(max_burst == (1<<LGMAXBURST));
+ end else
+ assert(max_burst == req_line_words);
+ end
+`endif
+ // }}}
+
+ // phantom_start
+ // {{{
+ initial phantom_start = 0;
+ always @(posedge i_clk)
+ if (i_reset)
+ phantom_start <= 0;
+ else
+ phantom_start <= start_burst;
+
+ initial lag_start = 1;
+ always @(posedge i_clk)
+ if (i_reset || r_stopped)
+ lag_start <= 1;
+ else
+ lag_start <= phantom_start;
+ // }}}
+
+ // ARVALID
+ // {{{
+ initial axi_arvalid = 0;
+ always @(posedge i_clk)
+ if (i_reset)
+ axi_arvalid <= 0;
+ else if (!M_AXI_ARVALID || M_AXI_ARREADY)
+ axi_arvalid <= start_burst;
+ // }}}
+
+ // ARADDR
+ // {{{
+ initial axi_araddr = 0;
+ always @(posedge i_clk)
+ begin
+ if (start_burst)
+ axi_araddr <= req_addr[C_AXI_ADDR_WIDTH-1:0];
+
+ axi_araddr[ADDRLSB-1:0] <= 0;
+ end
+ // }}}
+
+ // Set the constant M_AXI_* signals
+ // {{{
+ assign M_AXI_ARVALID= axi_arvalid;
+ assign M_AXI_ARID = AXI_ID;
+ assign M_AXI_ARADDR = axi_araddr;
+ assign M_AXI_ARLEN = axi_arlen;
+ // Verilator lint_off WIDTH
+ assign M_AXI_ARSIZE = $clog2(C_AXI_DATA_WIDTH)-3;
+ // Verilator lint_on WIDTH
+ assign M_AXI_ARBURST= 2'b01; // INCR
+ assign M_AXI_ARLOCK = 0;
+ assign M_AXI_ARCACHE= 0;
+ assign M_AXI_ARPROT = 0;
+ assign M_AXI_ARQOS = 0;
+ // }}}
+
+ // End AXI protocol section
+ // }}}
+
+ // Make Verilator happy
+ // {{{
+ // Verilator lint_off UNUSED
+ wire unused;
+ assign unused = &{ 1'b0, S_AXIL_AWPROT, S_AXIL_ARPROT, M_AXI_RID,
+ M_AXI_RRESP[0], fifo_full, wskd_strb[2:0],
+ S_AXIL_AWADDR[AXILLSB-1:0], S_AXIL_ARADDR[AXILLSB-1:0],
+ new_wideaddr[2*C_AXIL_DATA_WIDTH-1:C_AXI_ADDR_WIDTH],
+ new_control, new_config, fifo_fill };
+ // Verilator lint_on UNUSED
+ // }}}
+ // }}}
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+//
+// Formal properties
+//
+////////////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////////////
+`ifdef FORMAL
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // The following are only a subset of the formal properties currently
+ // being used to verify this module. They are not expected to be
+ // syntactically accurate.
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+ //
+ // ...
+ //
+
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Properties of the AXI-stream data interface
+ // {{{
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+
+ // (These are captured by the FIFO within)
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // The AXI-lite control interface
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+ localparam F_AXIL_LGDEPTH = 4;
+ wire [F_AXIL_LGDEPTH-1:0] faxil_rd_outstanding,
+ faxil_wr_outstanding, faxil_awr_outstanding;
+
+
+ faxil_slave #(
+ // {{{
+ .C_AXI_DATA_WIDTH(C_AXIL_DATA_WIDTH),
+ .C_AXI_ADDR_WIDTH(C_AXIL_ADDR_WIDTH),
+ .F_LGDEPTH(F_AXIL_LGDEPTH),
+ .F_AXI_MAXWAIT(2),
+ .F_AXI_MAXDELAY(2),
+ .F_AXI_MAXRSTALL(3)
+ // }}}
+ ) faxil(
+ // {{{
+ .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
+ //
+ .i_axi_awvalid(S_AXIL_AWVALID),
+ .i_axi_awready(S_AXIL_AWREADY),
+ .i_axi_awaddr( S_AXIL_AWADDR),
+ .i_axi_awprot( S_AXIL_AWPROT),
+ //
+ .i_axi_wvalid(S_AXIL_WVALID),
+ .i_axi_wready(S_AXIL_WREADY),
+ .i_axi_wdata( S_AXIL_WDATA),
+ .i_axi_wstrb( S_AXIL_WSTRB),
+ //
+ .i_axi_bvalid(S_AXIL_BVALID),
+ .i_axi_bready(S_AXIL_BREADY),
+ .i_axi_bresp( S_AXIL_BRESP),
+ //
+ .i_axi_arvalid(S_AXIL_ARVALID),
+ .i_axi_arready(S_AXIL_ARREADY),
+ .i_axi_araddr( S_AXIL_ARADDR),
+ .i_axi_arprot( S_AXIL_ARPROT),
+ //
+ .i_axi_rvalid(S_AXIL_RVALID),
+ .i_axi_rready(S_AXIL_RREADY),
+ .i_axi_rdata( S_AXIL_RDATA),
+ .i_axi_rresp( S_AXIL_RRESP),
+ //
+ .f_axi_rd_outstanding(faxil_rd_outstanding),
+ .f_axi_wr_outstanding(faxil_wr_outstanding),
+ .f_axi_awr_outstanding(faxil_awr_outstanding)
+ // }}}
+ );
+
+ always @(*)
+ begin
+ assert(faxil_rd_outstanding == (S_AXIL_RVALID ? 1:0)
+ +(S_AXIL_ARREADY ? 0:1));
+ assert(faxil_wr_outstanding == (S_AXIL_BVALID ? 1:0)
+ +(S_AXIL_WREADY ? 0:1));
+ assert(faxil_awr_outstanding== (S_AXIL_BVALID ? 1:0)
+ +(S_AXIL_AWREADY ? 0:1));
+ end
+
+ always @(*)
+ assert(cfg_zero_length ==
+ ((cfg_line_words == 0)||(cfg_frame_lines == 0)));
+
+ always @(*)
+ if (cfg_zero_length)
+ assert(!cfg_active);
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // The AXI master memory interface
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+
+ //
+ localparam F_AXI_LGDEPTH = 11; // LGLENW-LGMAXBURST+2 ??
+
+ //
+ // ...
+ //
+
+ faxi_master #(
+ // {{{
+ .C_AXI_ID_WIDTH(C_AXI_ID_WIDTH),
+ .C_AXI_ADDR_WIDTH(C_AXI_ADDR_WIDTH),
+ .C_AXI_DATA_WIDTH(C_AXI_DATA_WIDTH),
+ //
+ // ...
+ //
+ // }}}
+ ) faxi(
+ // {{{
+ .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN),
+ // The (unused) write interface
+ // {{{
+ .i_axi_awvalid(1'b0),
+ .i_axi_awready(1'b0),
+ .i_axi_awid( AXI_ID),
+ .i_axi_awaddr( 0),
+ .i_axi_awlen( 0),
+ .i_axi_awsize( 0),
+ .i_axi_awburst(0),
+ .i_axi_awlock( 0),
+ .i_axi_awcache(0),
+ .i_axi_awprot( 0),
+ .i_axi_awqos( 0),
+ //
+ .i_axi_wvalid(0),
+ .i_axi_wready(0),
+ .i_axi_wdata( 0),
+ .i_axi_wstrb( 0),
+ .i_axi_wlast( 0),
+ //
+ .i_axi_bvalid(1'b0),
+ .i_axi_bready(1'b0),
+ .i_axi_bid( AXI_ID),
+ .i_axi_bresp( 2'b00),
+ // }}}
+ // The read interface
+ // {{{
+ .i_axi_arvalid(M_AXI_ARVALID),
+ .i_axi_arready(M_AXI_ARREADY),
+ .i_axi_arid( M_AXI_ARID),
+ .i_axi_araddr( M_AXI_ARADDR),
+ .i_axi_arlen( M_AXI_ARLEN),
+ .i_axi_arsize( M_AXI_ARSIZE),
+ .i_axi_arburst(M_AXI_ARBURST),
+ .i_axi_arlock( M_AXI_ARLOCK),
+ .i_axi_arcache(M_AXI_ARCACHE),
+ .i_axi_arprot( M_AXI_ARPROT),
+ .i_axi_arqos( M_AXI_ARQOS),
+ //
+ .i_axi_rvalid(M_AXI_RVALID),
+ .i_axi_rready(M_AXI_RREADY),
+ .i_axi_rdata( M_AXI_RDATA),
+ .i_axi_rlast( M_AXI_RLAST),
+ .i_axi_rresp( M_AXI_RRESP),
+ // ...
+ // }}}
+ );
+
+
+ //
+ // ...
+ //
+ always @(*)
+ begin
+ // ...
+
+ assert(M_AXI_ARBURST == 2'b01);
+ end
+
+ always @(*)
+ if (faxi_rd_ckvalid)
+ begin
+ assert(!r_stopped);
+ //
+ // ...
+ //
+ end
+
+ //
+ // ...
+ //
+
+ reg [LGMAXBURST-1:0] f_rd_subaddr;
+ always @(*)
+ f_rd_subaddr = f_rd_addr[ADDRLSB +: LGMAXBURST];
+
+ always @(*)
+ begin
+ assert(cfg_frame_addr[ADDRLSB-1:0] == 0);
+ if (!r_stopped)
+ begin
+ assert(req_addr[ADDRLSB-1:0] == 0);
+ assert(req_line_addr[ADDRLSB-1:0] == 0);
+ end
+
+ if (M_AXI_RVALID)
+ assert(M_AXI_RLAST == (rd_hlast || (&f_rd_subaddr)));
+ end
+
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Read request to return address correlations
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+
+ if (M_AXI_RVALID)
+ begin
+ if (rd_hlast || (&f_rd_subaddr))
+ begin
+ // ...
+ assert(M_AXI_RLAST);
+ end else
+ // ...
+ assume(!M_AXI_RLAST);
+ end
+ end
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Other formal properties
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Contract checks
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Cover checks
+ //
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // {{{
+ reg cvr_full_frame, cvr_full_size;
+ (* anyconst *) reg cvr_hlast_rlast;
+
+ always @(posedge i_clk)
+ if (r_stopped)
+ cvr_full_size <= (cfg_line_step >= cfg_line_words)
+ &&(cfg_line_words > 5)
+ &&(cfg_frame_lines > 4);
+ else begin
+ if ($changed(cfg_line_step))
+ cvr_full_size <= 0;
+ if ($changed(cfg_line_words))
+ cvr_full_size <= 0;
+ if ($changed(cfg_frame_lines))
+ cvr_full_size <= 0;
+ if ($changed(cfg_frame_addr))
+ cvr_full_size <= 0;
+ end
+
+ always @(posedge i_clk)
+ if (r_stopped || !cvr_full_size)
+ cvr_full_frame <= 0;
+ else if (!cvr_full_frame)
+ cvr_full_frame <= rd_vlast && rd_hlast && M_AXI_RVALID && M_AXI_RREADY;
+
+ always @(*)
+ cover(!soft_reset);
+
+ always @(*)
+ cover(start_burst);
+
+ always @(*)
+ cover(M_AXI_ARVALID && M_AXI_ARREADY);
+
+ always @(*)
+ cover(M_AXI_RVALID);
+
+ always @(*)
+ cover(M_AXI_RVALID & M_AXI_RLAST);
+
+ always @(*)
+ cover(!r_stopped && cvr_full_frame);
+
+ always @(*)
+ cover(cvr_full_frame && phantom_start && !r_stopped);
+
+ always @(*)
+ if (cvr_hlast_rlast)
+ begin
+ // assume(M_AXI_RLAST == (rd_hlast && M_AXI_RVALID));
+ assume(M_AXI_ARREADY && M_AXI_RREADY);
+ assume(M_AXIS_TREADY);
+ assume(cfg_frame_addr[12:0] == 0);
+ assume(cfg_line_step[3:0] == 0);
+ end
+
+ always @(*)
+ cover(cvr_hlast_rlast && cvr_full_frame && phantom_start && !r_stopped);
+ // }}}
+ ////////////////////////////////////////////////////////////////////////
+ //
+ // Simplifying (careless) assumptions
+ // {{{
+ ////////////////////////////////////////////////////////////////////////
+ //
+ //
+ always @(posedge i_clk)
+ if (!r_stopped || cfg_active)
+ begin
+ assume($stable(cfg_frame_addr));
+ assume($stable(cfg_frame_lines));
+ assume($stable(cfg_line_words));
+ assume($stable(cfg_line_step));
+ end
+
+
+ always @(*)
+ assume(!f_sequential);
+
+ always @(*)
+ assume(!f_biglines);
+
+ always @(*)
+ assume(!req_addr[C_AXI_ADDR_WIDTH]);
+
+ always @(*)
+ assume(!req_line_addr[C_AXI_ADDR_WIDTH]);
+ // }}}
+ // }}}
+`endif
+endmodule
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 07:01:11 +0000