URL
https://opencores.org/ocsvn/wbscope/wbscope/trunk
Subversion Repositories wbscope
[/] [wbscope/] [trunk/] [rtl/] [axi4lscope.v] - Rev 14
Compare with Previous | Blame | View Log
`timescale 1 ns / 1 ps //////////////////////////////////////////////////////////////////////////////// // // Filename: axi4lscope.v // // Project: WBScope, a wishbone hosted scope // // Purpose: This is a generic/library routine for providing a bus accessed // 'scope' or (perhaps more appropriately) a bus accessed logic analyzer. // The general operation is such that this 'scope' can record and report // on any 32 bit value transiting through the FPGA. Once started and // reset, the scope records a copy of the input data every time the clock // ticks with the circuit enabled. That is, it records these values up // until the trigger. Once the trigger goes high, the scope will record // for br_holdoff more counts before stopping. Values may then be read // from the buffer, oldest to most recent. After reading, the scope may // then be reset for another run. // // In general, therefore, operation happens in this fashion: // 1. A reset is issued. // 2. Recording starts, in a circular buffer, and continues until // 3. The trigger line is asserted. // The scope registers the asserted trigger by setting // the 'o_triggered' output flag. // 4. A counter then ticks until the last value is written // The scope registers that it has stopped recording by // setting the 'o_stopped' output flag. // 5. The scope recording is then paused until the next reset. // 6. While stopped, the CPU can read the data from the scope // 7. -- oldest to most recent // 8. -- one value per i_rd&i_data_clk // 9. Writes to the data register reset the address to the // beginning of the buffer // // Although the data width DW is parameterized, it is not very changable, // since the width is tied to the width of the data bus, as is the // control word. Therefore changing the data width would require changing // the interface. It's doable, but it would be a change to the interface. // // The SYNCHRONOUS parameter turns on and off meta-stability // synchronization. Ideally a wishbone scope able to handle one or two // clocks would have a changing number of ports as this SYNCHRONOUS // parameter changed. Other than running another script to modify // this, I don't know how to do that so ... we'll just leave it running // off of two clocks or not. // // // Internal to this routine, registers and wires are named with one of the // following prefixes: // // i_ An input port to the routine // o_ An output port of the routine // br_ A register, controlled by the bus clock // dr_ A register, controlled by the data clock // bw_ A wire/net, controlled by the bus clock // dw_ A wire/net, controlled by the data clock // // And, of course, since AXI wants to be particular about their port // naming conventions, anything beginning with // // S_AXI_ // // is a signal associated with this function as an AXI slave. // // // Creator: Dan Gisselquist, Ph.D. // Gisselquist Technology, LLC // //////////////////////////////////////////////////////////////////////////////// // // Copyright (C) 2015-2018, Gisselquist Technology, LLC // // This program is free software (firmware): you can redistribute it and/or // modify it under the terms of the GNU General Public License as published // by the Free Software Foundation, either version 3 of the License, or (at // your option) any later version. // // This program is distributed in the hope that it will be useful, but WITHOUT // ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or // FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License // for more details. // // You should have received a copy of the GNU General Public License along // with this program. (It's in the $(ROOT)/doc directory. Run make with no // target there if the PDF file isn't present.) If not, see // <http://www.gnu.org/licenses/> for a copy. // // License: GPL, v3, as defined and found on www.gnu.org, // http://www.gnu.org/licenses/gpl.html // // //////////////////////////////////////////////////////////////////////////////// // // `default_nettype none // module axi4lscope #( // Users to add parameters here parameter [4:0] LGMEM = 5'd10, parameter BUSW = 32, parameter SYNCHRONOUS=1, parameter HOLDOFFBITS = 20, parameter [(HOLDOFFBITS-1):0] DEFAULT_HOLDOFF = ((1<<(LGMEM-1))-4), // User parameters ends // DO NOT EDIT BELOW THIS LINE --------------------- // Do not modify the parameters beyond this line // Width of S_AXI data bus parameter integer C_S_AXI_DATA_WIDTH = 32, // Width of S_AXI address bus parameter integer C_S_AXI_ADDR_WIDTH = 4 ) ( // Users to add ports here input wire i_data_clk, // The data clock, can be set to ACLK input wire i_ce, // = '1' when recordable data is present input wire i_trigger,// = '1' when interesting event hapns input wire [31:0] i_data, output wire o_interrupt, // ='1' when scope has stopped // User ports ends // DO NOT EDIT BELOW THIS LINE --------------------- // Do not modify the ports beyond this line // Global Clock Signal input wire S_AXI_ACLK, // Global Reset Signal. This Signal is Active LOW input wire S_AXI_ARESETN, // Write address (issued by master, acceped by Slave) input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_AWADDR, // Write channel Protection type. This signal indicates the // privilege and security level of the transaction, and whether // the transaction is a data access or an instruction access. input wire [2 : 0] S_AXI_AWPROT, // Write address valid. This signal indicates that the master // signaling valid write address and control information. input wire S_AXI_AWVALID, // Write address ready. This signal indicates that the slave // is ready to accept an address and associated control signals. output wire S_AXI_AWREADY, // Write data (issued by master, acceped by Slave) input wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_WDATA, // Write strobes. This signal indicates which byte lanes hold // valid data. There is one write strobe bit for each eight // bits of the write data bus. input wire [(C_S_AXI_DATA_WIDTH/8)-1 : 0] S_AXI_WSTRB, // Write valid. This signal indicates that valid write // data and strobes are available. input wire S_AXI_WVALID, // Write ready. This signal indicates that the slave // can accept the write data. output wire S_AXI_WREADY, // Write response. This signal indicates the status // of the write transaction. output wire [1 : 0] S_AXI_BRESP, // Write response valid. This signal indicates that the channel // is signaling a valid write response. output wire S_AXI_BVALID, // Response ready. This signal indicates that the master // can accept a write response. input wire S_AXI_BREADY, // Read address (issued by master, acceped by Slave) input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_ARADDR, // Protection type. This signal indicates the privilege // and security level of the transaction, and whether the // transaction is a data access or an instruction access. input wire [2 : 0] S_AXI_ARPROT, // Read address valid. This signal indicates that the channel // is signaling valid read address and control information. input wire S_AXI_ARVALID, // Read address ready. This signal indicates that the slave is // ready to accept an address and associated control signals. output wire S_AXI_ARREADY, // Read data (issued by slave) output wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_RDATA, // Read response. This signal indicates the status of the // read transfer. output wire [1 : 0] S_AXI_RRESP, // Read valid. This signal indicates that the channel is // signaling the required read data. output wire S_AXI_RVALID, // Read ready. This signal indicates that the master can // accept the read data and response information. input wire S_AXI_RREADY // DO NOT EDIT ABOVE THIS LINE --------------------- ); // AXI4LITE signals reg [C_S_AXI_ADDR_WIDTH-1 : 0] axi_awaddr; reg axi_awready; // reg [1 : 0] axi_bresp; reg axi_bvalid; reg [C_S_AXI_ADDR_WIDTH-1 : 0] axi_araddr; reg axi_arready; // reg [1 : 0] axi_rresp; wire write_stb; /////////////////////////////////////////////////// // // Decode and handle the AXI/Bus signaling // /////////////////////////////////////////////////// // // Sadly, the AXI bus is *way* more complicated to // deal with than it needs to be. Still, we offer // the following as a simple means of dealing with // it. The majority of the code in this section // comes directly from a Xilinx/Vivado generated // file. // // Gisselquist Technology, LLC, claims no copyright // or ownership of this section of the code. // wire i_reset, axi_bstall, axi_rstall; assign i_reset = !S_AXI_ARESETN; always @(*) if ((!axi_bstall)&&(S_AXI_AWVALID)&&(S_AXI_WVALID)) axi_awready <= 1'b1; else axi_awready <= 1'b0; assign S_AXI_AWREADY = axi_awready; assign S_AXI_WREADY = axi_awready; always @(posedge S_AXI_ACLK) if ((S_AXI_AWVALID)&&(S_AXI_AWREADY)) axi_awaddr <= S_AXI_AWADDR; initial axi_bvalid = 0; always @(posedge S_AXI_ACLK) if (i_reset) axi_bvalid <= 0; else if (write_stb) axi_bvalid <= 1'b1; else if (S_AXI_BREADY) axi_bvalid <= 1'b0; assign S_AXI_BRESP = 2'b00; // An 'OKAY' response assign S_AXI_BVALID= axi_bvalid; assign axi_bstall = (S_AXI_BVALID)&&(!S_AXI_BREADY); always @(*) if (i_reset) axi_arready = 1'b0; else if (axi_rstall) axi_arready = 1'b0; else axi_arready = 1'b1; always @(posedge S_AXI_ACLK) if (i_reset) axi_araddr <= 0; else if ((axi_arready)&&(S_AXI_ARVALID)) axi_araddr <= S_AXI_ARADDR; assign S_AXI_ARREADY = axi_arready; reg [1:0] rvalid; initial rvalid = 2'b00; always @(posedge S_AXI_ACLK) if (i_reset) rvalid <= 2'b00; else if ((axi_arready)&&(S_AXI_ARVALID)) rvalid <= 2'b01; else if (rvalid == 2'b01) rvalid <= 2'b10; else if (S_AXI_RREADY) rvalid <= 2'b00; assign S_AXI_RVALID = rvalid[1]; assign S_AXI_RRESP = 2'b00; assign axi_rstall = ((rvalid[0])||(S_AXI_RVALID)&&(!S_AXI_RREADY)); /////////////////////////////////////////////////// // // Final simplification of the AXI code // /////////////////////////////////////////////////// // // Now that we've provided all of the bus signaling // above, can we make any sense of it? // // The following wires are here to provide some // simplification of the complex bus protocol. In // particular, are we reading or writing during this // clock? The two *should* be mutually exclusive // (i.e., you *shouldn't* be able to both read and // write on the same clock) ... but Xilinx's default // implementation does nothing to ensure that this // would be the case. // // From here on down, Gisselquist Technology, LLC, // claims a copyright on the code. // wire bus_clock; assign bus_clock = S_AXI_ACLK; wire read_from_data; assign read_from_data = (S_AXI_ARVALID)&&(S_AXI_ARREADY) &&(axi_araddr[0]); assign write_stb = ((axi_awready)&&(S_AXI_AWVALID) &&(S_AXI_WVALID)); wire write_to_control; assign write_to_control = (write_stb)&&(!axi_awaddr[0]); reg read_address; always @(posedge bus_clock) if ((axi_arready)&&(S_AXI_ARVALID)) read_address <= axi_araddr[0]; wire [31:0] i_wb_data; assign i_wb_data = S_AXI_WDATA; /////////////////////////////////////////////////// // // The actual SCOPE // /////////////////////////////////////////////////// // // Now that we've finished reading/writing from the // bus, ... or at least acknowledging reads and // writes from and to the bus--even if they haven't // happened yet, now we implement our actual scope. // This includes implementing the actual reads/writes // from/to the bus. // // From here on down, is the heart of the scope itself. // reg [(LGMEM-1):0] raddr; reg [(BUSW-1):0] mem[0:((1<<LGMEM)-1)]; // Our status/config register wire bw_reset_request, bw_manual_trigger, bw_disable_trigger, bw_reset_complete; reg [2:0] br_config; reg [(HOLDOFFBITS-1):0] br_holdoff; initial br_config = 3'b0; initial br_holdoff = DEFAULT_HOLDOFF; always @(posedge bus_clock) if (write_to_control) begin br_config <= { i_wb_data[31], i_wb_data[27], i_wb_data[26] }; br_holdoff <= i_wb_data[(HOLDOFFBITS-1):0]; end else if (bw_reset_complete) br_config[2] <= 1'b1; assign bw_reset_request = (!br_config[2]); assign bw_manual_trigger = (br_config[1]); assign bw_disable_trigger = (br_config[0]); wire dw_reset, dw_manual_trigger, dw_disable_trigger; generate if (SYNCHRONOUS > 0) begin assign dw_reset = bw_reset_request; assign dw_manual_trigger = bw_manual_trigger; assign dw_disable_trigger = bw_disable_trigger; assign bw_reset_complete = bw_reset_request; end else begin reg r_reset_complete; (* ASYNC_REG = "TRUE" *) reg [2:0] q_iflags; reg [2:0] r_iflags; // Resets are synchronous to the bus clock, not the data clock // so do a clock transfer here initial { q_iflags, r_iflags } = 6'h0; initial r_reset_complete = 1'b0; always @(posedge i_data_clk) begin q_iflags <= { bw_reset_request, bw_manual_trigger, bw_disable_trigger }; r_iflags <= q_iflags; r_reset_complete <= (dw_reset); end assign dw_reset = r_iflags[2]; assign dw_manual_trigger = r_iflags[1]; assign dw_disable_trigger = r_iflags[0]; (* ASYNC_REG = "TRUE" *) reg q_reset_complete; reg qq_reset_complete; // Pass an acknowledgement back from the data clock to the bus // clock that the reset has been accomplished initial q_reset_complete = 1'b0; initial qq_reset_complete = 1'b0; always @(posedge bus_clock) begin q_reset_complete <= r_reset_complete; qq_reset_complete <= q_reset_complete; end assign bw_reset_complete = qq_reset_complete; `ifdef FORMAL always @($global_clock) if (f_past_valid_data) begin if ($rose(r_reset_complete)) assert(bw_reset_request); end `endif end endgenerate // // Set up the trigger // // // Write with the i-clk, or input clock. All outputs read with the // bus clock, or bus_clock as we've called it here. reg dr_triggered, dr_primed; wire dw_trigger; assign dw_trigger = (dr_primed)&&( ((i_trigger)&&(!dw_disable_trigger)) ||(dw_manual_trigger)); initial dr_triggered = 1'b0; always @(posedge i_data_clk) if (dw_reset) dr_triggered <= 1'b0; else if ((i_ce)&&(dw_trigger)) dr_triggered <= 1'b1; // // Determine when memory is full and capture is complete // // Writes take place on the data clock // The counter is unsigned (* ASYNC_REG="TRUE" *) reg [(HOLDOFFBITS-1):0] counter; reg dr_stopped; initial dr_stopped = 1'b0; initial counter = 0; always @(posedge i_data_clk) if (dw_reset) counter <= 0; else if ((i_ce)&&(dr_triggered)&&(!dr_stopped)) counter <= counter + 1'b1; always @(posedge i_data_clk) if ((!dr_triggered)||(dw_reset)) dr_stopped <= 1'b0; else if (HOLDOFFBITS > 1) // if (i_ce) dr_stopped <= (counter >= br_holdoff); else if (HOLDOFFBITS <= 1) dr_stopped <= ((i_ce)&&(dw_trigger)); // // Actually do our writes to memory. Record, via 'primed' when // the memory is full. // // The 'waddr' address that we are using really crosses two clock // domains. While writing and changing, it's in the data clock // domain. Once stopped, it becomes part of the bus clock domain. // The clock transfer on the stopped line handles the clock // transfer for these signals. // reg [(LGMEM-1):0] waddr; initial waddr = {(LGMEM){1'b0}}; initial dr_primed = 1'b0; always @(posedge i_data_clk) if (dw_reset) // For simulation purposes, supply a valid value begin waddr <= 0; // upon reset. dr_primed <= 1'b0; end else if ((i_ce)&&(!dr_stopped)) begin // mem[waddr] <= i_data; waddr <= waddr + {{(LGMEM-1){1'b0}},1'b1}; if (!dr_primed) begin //if (br_holdoff[(HOLDOFFBITS-1):LGMEM]==0) // dr_primed <= (waddr >= br_holdoff[(LGMEM-1):0]); // else dr_primed <= (&waddr); end end // Delay the incoming data so that we can get our trigger // logic to line up with the data. The goal is to have a // hold off of zero place the trigger in the last memory // address. localparam STOPDELAY = 1; wire [(BUSW-1):0] wr_piped_data; generate if (STOPDELAY == 0) // No delay ... just assign the wires to our input lines assign wr_piped_data = i_data; else if (STOPDELAY == 1) begin // // Delay by one means just register this once reg [(BUSW-1):0] data_pipe; always @(posedge i_data_clk) if (i_ce) data_pipe <= i_data; assign wr_piped_data = data_pipe; end else begin // Arbitrary delay ... use a longer pipe reg [(STOPDELAY*BUSW-1):0] data_pipe; always @(posedge i_data_clk) if (i_ce) data_pipe <= { data_pipe[((STOPDELAY-1)*BUSW-1):0], i_data }; assign wr_piped_data = { data_pipe[(STOPDELAY*BUSW-1):((STOPDELAY-1)*BUSW)] }; end endgenerate always @(posedge i_data_clk) if ((i_ce)&&(!dr_stopped)) mem[waddr] <= wr_piped_data; // // Clock transfer of the status signals // wire bw_stopped, bw_triggered, bw_primed; generate if (SYNCHRONOUS > 0) begin assign bw_stopped = dr_stopped; assign bw_triggered = dr_triggered; assign bw_primed = dr_primed; end else begin // These aren't a problem, since none of these are strobe // signals. They goes from low to high, and then stays high // for many clocks. Swapping is thus easy--two flip flops to // protect against meta-stability and we're done. // (* ASYNC_REG = "TRUE" *) reg [2:0] q_oflags; reg [2:0] r_oflags; initial q_oflags = 3'h0; initial r_oflags = 3'h0; always @(posedge bus_clock) if (bw_reset_request) begin q_oflags <= 3'h0; r_oflags <= 3'h0; end else begin q_oflags <= { dr_stopped, dr_triggered, dr_primed }; r_oflags <= q_oflags; end assign bw_stopped = r_oflags[2]; assign bw_triggered = r_oflags[1]; assign bw_primed = r_oflags[0]; end endgenerate // Reads use the bus clock initial raddr = 0; always @(posedge bus_clock) begin if ((bw_reset_request)||(write_to_control)) raddr <= 0; else if ((read_from_data)&&(bw_stopped)) raddr <= raddr + 1'b1; // Data read, when stopped end reg [(LGMEM-1):0] this_addr; always @(posedge bus_clock) if ((bw_stopped)&&(read_from_data)) this_addr <= raddr + waddr + 1'b1; else this_addr <= raddr + waddr; reg [31:0] nxt_mem; always @(posedge bus_clock) if (read_from_data) nxt_mem <= mem[this_addr]; wire [19:0] full_holdoff; assign full_holdoff[(HOLDOFFBITS-1):0] = br_holdoff; generate if (HOLDOFFBITS < 20) assign full_holdoff[19:(HOLDOFFBITS)] = 0; endgenerate reg [31:0] o_bus_data; wire [4:0] bw_lgmem; assign bw_lgmem = LGMEM; always @(posedge bus_clock) if (rvalid[0]) begin if (!read_address) // Control register read o_bus_data <= { bw_reset_request, bw_stopped, bw_triggered, bw_primed, bw_manual_trigger, bw_disable_trigger, (raddr == {(LGMEM){1'b0}}), bw_lgmem, full_holdoff }; else if (!bw_stopped) // read, prior to stopping o_bus_data <= i_data; else // if (i_wb_addr) // Read from FIFO memory o_bus_data <= nxt_mem; // mem[raddr+waddr]; end assign S_AXI_RDATA = o_bus_data; reg br_level_interrupt; initial br_level_interrupt = 1'b0; assign o_interrupt = (bw_stopped)&&(!bw_disable_trigger) &&(!br_level_interrupt); always @(posedge bus_clock) if ((bw_reset_complete)||(bw_reset_request)) br_level_interrupt<= 1'b0; else br_level_interrupt<= (bw_stopped)&&(!bw_disable_trigger); // verilator lint_off UNUSED // Make verilator happy wire [44:0] unused; assign unused = { S_AXI_WSTRB, S_AXI_ARPROT, S_AXI_AWPROT, axi_awaddr[3:1], axi_araddr[3:1], i_wb_data[30:28], i_wb_data[25:0] }; // verilator lint_on UNUSED `ifdef FORMAL generate if (SYNCHRONOUS) begin always @(*) assume(i_data_clk == S_AXI_ACLK); end else begin localparam CKSTEP_BITS = 3; localparam [CKSTEP_BITS-1:0] MAX_STEP = { 1'b0, {(CKSTEP_BITS-1){1'b1}} }; // "artificially" generate two clocks `ifdef VERIFIC (* gclk *) wire gbl_clock; global clocking @(posedge gbl_clock); endclocking `endif (* anyconst *) wire [CKSTEP_BITS-1:0] f_data_step, f_bus_step; reg [CKSTEP_BITS-1:0] f_data_count, f_bus_count; always @(*) begin assume(f_data_step > 0); assume(f_bus_step > 0); assume(f_data_step <= MAX_STEP); assume(f_bus_step <= MAX_STEP); assume((f_data_step == MAX_STEP) ||(f_bus_step == MAX_STEP)); end always @($global_clock) begin f_data_count <= f_data_count + f_data_step; f_bus_count <= f_bus_count + f_bus_step; assume(i_data_clk == f_data_count[CKSTEP_BITS-1]); assume(bus_clock == f_bus_count[CKSTEP_BITS-1]); end always @($global_clock) if (!$rose(i_data_clk)) begin assume($stable(i_trigger)); assume($stable(i_data)); end always @($global_clock) if (!$rose(S_AXI_ACLK)) begin assume($stable(S_AXI_ARESETN)); // assume($stable(S_AXI_AWADDR)); assume($stable(S_AXI_AWPROT)); assume($stable(S_AXI_AWVALID)); // assume($stable(S_AXI_WDATA)); assume($stable(S_AXI_WSTRB)); assume($stable(S_AXI_WVALID)); // assume($stable(S_AXI_BREADY)); // assume($stable(S_AXI_ARADDR)); assume($stable(S_AXI_ARPROT)); assume($stable(S_AXI_ARVALID)); // assume($stable(S_AXI_RREADY)); // end end endgenerate reg f_past_valid_bus, f_past_valid_gbl, f_past_valid_data; initial { f_past_valid_bus, f_past_valid_gbl, f_past_valid_data }= 3'b0; always @(posedge S_AXI_ACLK) f_past_valid_bus = 1'b1; generate if (!SYNCHRONOUS) begin always @($global_clock) f_past_valid_gbl <= 1'b1; always @(posedge i_data_clk) f_past_valid_data = 1'b1; always @(posedge i_data_clk) if (f_past_valid_data) assert($stable(o_interrupt)); always @($global_clock) if ((f_past_valid_gbl)&&(!$rose(S_AXI_ACLK))) begin assert($stable(S_AXI_AWREADY)); assert($stable(S_AXI_ARREADY)); assert($stable(S_AXI_RDATA)); assert($stable(S_AXI_RRESP)); assert($stable(S_AXI_RVALID)); assert($stable(S_AXI_WREADY)); assert($stable(S_AXI_BRESP)); assert($stable(S_AXI_BVALID)); end end else begin always @(*) f_past_valid_data = f_past_valid_bus; always @(*) f_past_valid_gbl = f_past_valid_bus; end endgenerate localparam F_LGDEPTH = 5; wire [F_LGDEPTH-1:0] f_axi_rd_outstanding, f_axi_wr_outstanding, f_axi_awr_outstanding; faxil_slave #( // .C_S_AXI_DATA_WIDth(C_S_AXI_DATA_WIDTH), // Width of S_AXI address bus .C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH), .F_LGDEPTH(F_LGDEPTH), .F_OPT_HAS_CACHE(1'b0), // .F_OPT_CLK2FFLOGIC(!SYNCHRONOUS), .F_AXI_MAXWAIT(5'h6), .F_AXI_MAXDELAY(5'h6), ) faxil_slave( .i_clk(S_AXI_ACLK), .i_axi_reset_n(S_AXI_ARESETN), // .i_axi_awaddr(S_AXI_AWADDR), .i_axi_awprot(S_AXI_AWPROT), .i_axi_awcache(4'h0), .i_axi_awvalid(S_AXI_AWVALID), .i_axi_awready(S_AXI_AWREADY), // .i_axi_wdata(S_AXI_WDATA), .i_axi_wstrb(S_AXI_WSTRB), .i_axi_wvalid(S_AXI_WVALID), .i_axi_wready(S_AXI_WREADY), // .i_axi_bresp(S_AXI_BRESP), .i_axi_bvalid(S_AXI_BVALID), .i_axi_bready(S_AXI_BREADY), // .i_axi_araddr(S_AXI_ARADDR), .i_axi_arprot(S_AXI_ARPROT), .i_axi_arvalid(S_AXI_ARVALID), .i_axi_arready(S_AXI_ARREADY), .i_axi_arcache(4'h0), // .i_axi_rdata(S_AXI_RDATA), .i_axi_rresp(S_AXI_RRESP), .i_axi_rvalid(S_AXI_RVALID), .i_axi_rready(S_AXI_RREADY), // .f_axi_rd_outstanding(f_axi_rd_outstanding), .f_axi_wr_outstanding(f_axi_wr_outstanding), .f_axi_awr_outstanding(f_axi_awr_outstanding)); always @(*) begin assert(f_axi_wr_outstanding == f_axi_awr_outstanding); if (axi_bvalid) assert(f_axi_wr_outstanding == 1); else assert(f_axi_wr_outstanding == 0); if (|rvalid) assert(f_axi_rd_outstanding == 1); else assert(f_axi_rd_outstanding == 0); assert(rvalid != 2'b11); end always @(*) if (dr_triggered) assert(dr_primed); always @(*) if (dr_stopped) assert((dr_primed)&&(dr_triggered)); reg dr_triggered, dr_primed; wire dw_trigger; assign dw_trigger = (dr_primed)&&( ((i_trigger)&&(!dw_disable_trigger)) ||(dw_manual_trigger)); (* anyconst *) wire [(LGMEM-1):0] f_addr; reg [31:0] f_data; reg f_filled; initial f_filled = 1'b0; always @(posedge i_data_clk) if (dw_reset) f_filled <= 1'b0; else if ((i_ce)&&(!dr_stopped)&&(waddr == f_addr)) f_filled <= 1'b1; always @(posedge i_data_clk) if (waddr > f_addr) assert(f_filled); always @(posedge i_data_clk) if (!f_filled) assert(!dr_primed); always @(posedge i_data_clk) if ((i_ce)&&(!dr_stopped)&&(waddr == f_addr)) f_data <= wr_piped_data; always @(posedge i_data_clk) if (f_filled) assert(mem[f_addr] == f_data); `endif endmodule