OpenCores
URL https://opencores.org/ocsvn/zipcpu/zipcpu/trunk

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [peripherals/] [wbdmac.v] - Diff between revs 201 and 209

Only display areas with differences | Details | Blame | View Log

Rev 201 Rev 209
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
// Filename:    wbdmac.v
// Filename:    wbdmac.v
//
//
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
//
//
// Purpose:     Wishbone DMA controller
// Purpose:     Wishbone DMA controller
//
//
//      This module is controllable via the wishbone, and moves values from
//      This module is controllable via the wishbone, and moves values from
//      one location in the wishbone address space to another.  The amount of
//      one location in the wishbone address space to another.  The amount of
//      memory moved at any given time can be up to 4kB, or equivalently 1kW.
//      memory moved at any given time can be up to 4kB, or equivalently 1kW.
//      Four registers control this DMA controller: a control/status register,
//      Four registers control this DMA controller: a control/status register,
//      a length register, a source WB address and a destination WB address.
//      a length register, a source WB address and a destination WB address.
//      These register may be read at any time, but they may only be written
//      These register may be read at any time, but they may only be written
//      to when the controller is idle.
//      to when the controller is idle.
//
//
//      The meanings of three of the setup registers should be self explanatory:
//      The meanings of three of the setup registers should be self explanatory:
//              - The length register controls the total number of words to
//              - The length register controls the total number of words to
//                      transfer.
//                      transfer.
//              - The source address register controls where the DMA controller
//              - The source address register controls where the DMA controller
//                      reads from.  This address may or may not be incremented
//                      reads from.  This address may or may not be incremented
//                      after each read, depending upon the setting in the
//                      after each read, depending upon the setting in the
//                      control/status register.
//                      control/status register.
//              - The destination address register, which controls where the DMA
//              - The destination address register, which controls where the DMA
//                      controller writes to.  This address may or may not be
//                      controller writes to.  This address may or may not be
//                      incremented after each write, also depending upon the
//                      incremented after each write, also depending upon the
//                      setting in the control/status register.
//                      setting in the control/status register.
//
//
//      It is the control/status register, at local address zero, that needs
//      It is the control/status register, at local address zero, that needs
//      more definition:
//      more definition:
//
//
//      Bits:
//      Bits:
//      31      R       Write protect   If this is set to one, it means the
//      31      R       Write protect   If this is set to one, it means the
//                              write protect bit is set and the controller
//                              write protect bit is set and the controller
//                              is therefore idle.  This bit will be set upon
//                              is therefore idle.  This bit will be set upon
//                              completing any transfer.
//                              completing any transfer.
//      30      R       Error.          The controller stopped mid-transfer
//      30      R       Error.          The controller stopped mid-transfer
//                                      after receiving a bus error.
//                                      after receiving a bus error.
//      29      R/W     inc_s_n         If set to one, the source address
//      29      R/W     inc_s_n         If set to one, the source address
//                              will not increment from one read to the next.
//                              will not increment from one read to the next.
//      28      R/W     inc_d_n         If set to one, the destination address
//      28      R/W     inc_d_n         If set to one, the destination address
//                              will not increment from one write to the next.
//                              will not increment from one write to the next.
//      27      R       Always 0
//      27      R       Always 0
//      26..16  R       nread           Indicates how many words have been read,
//      26..16  R       nread           Indicates how many words have been read,
//                              and not necessarily written (yet).  This
//                              and not necessarily written (yet).  This
//                              combined with the cfg_len parameter should tell
//                              combined with the cfg_len parameter should tell
//                              exactly where the controller is at mid-transfer.
//                              exactly where the controller is at mid-transfer.
//      27..16  W       WriteProtect    When a 12'h3db is written to these
//      27..16  W       WriteProtect    When a 12'h3db is written to these
//                              bits, the write protect bit will be cleared.
//                              bits, the write protect bit will be cleared.
//                              
//                              
//      15      R/W     on_dev_trigger  When set to '1', the controller will
//      15      R/W     on_dev_trigger  When set to '1', the controller will
//                              wait for an external interrupt before starting.
//                              wait for an external interrupt before starting.
//      14..10  R/W     device_id       This determines which external interrupt
//      14..10  R/W     device_id       This determines which external interrupt
//                              will trigger a transfer.
//                              will trigger a transfer.
//      9..0    R/W     transfer_len    How many bytes to transfer at one time.
//      9..0    R/W     transfer_len    How many bytes to transfer at one time.
//                              The minimum transfer length is one, while zero
//                              The minimum transfer length is one, while zero
//                              is mapped to a transfer length of 1kW.
//                              is mapped to a transfer length of 1kW.
//
//
 
//      Write 32'hffed00 to halt an ongoing transaction, completing anything
 
//      remaining, or 32'hafed00 to abort the current transaction leaving
 
//      any unfinished read/write in an undetermined state.
 
//
//
//
//      To use this, follow this checklist:
//      To use this, follow this checklist:
//      1. Wait for any prior DMA operation to complete
//      1. Wait for any prior DMA operation to complete
//              (Read address 0, wait 'till either top bit is set or cfg_len==0)
//              (Read address 0, wait 'till either top bit is set or cfg_len==0)
//      2. Write values into length, source and destination address. 
//      2. Write values into length, source and destination address. 
//              (writei(3, &vals) should be sufficient for this.)
//              (writei(3, &vals) should be sufficient for this.)
//      3. Enable the DMAC interrupt in whatever interrupt controller is present
//      3. Enable the DMAC interrupt in whatever interrupt controller is present
//              on the system.
//              on the system.
//      4. Write the final start command to the setup/control/status register:
//      4. Write the final start command to the setup/control/status register:
//              Set inc_s_n, inc_d_n, on_dev_trigger, dev_trigger,
//              Set inc_s_n, inc_d_n, on_dev_trigger, dev_trigger,
//                      appropriately for your task
//                      appropriately for your task
//              Write 12'h3db to the upper word.
//              Write 12'h3db to the upper word.
//              Set the lower word to either all zeros, or a smaller transfer
//              Set the lower word to either all zeros, or a smaller transfer
//              length if desired.
//              length if desired.
//      5. wait() for the interrupt and the operation to complete.
//      5. wait() for the interrupt and the operation to complete.
//              Prior to completion, number of items successfully transferred
//              Prior to completion, number of items successfully transferred
//              be read from the length register.  If the internal buffer is
//              be read from the length register.  If the internal buffer is
//              being used, then you can read how much has been read into that
//              being used, then you can read how much has been read into that
//              buffer by reading from bits 25..16 of this control/status
//              buffer by reading from bits 25..16 of this control/status
//              register.
//              register.
//
//
// Creator:     Dan Gisselquist, Ph.D.
// Creator:     Dan Gisselquist, Ph.D.
//              Gisselquist Technology, LLC
//              Gisselquist Technology, LLC
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
// Copyright (C) 2015-2017, Gisselquist Technology, LLC
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
//
//
// This program is free software (firmware): you can redistribute it and/or
// 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
// 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// your option) any later version.
//
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
// for more details.
// for more details.
//
//
// You should have received a copy of the GNU General Public License along
// 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
// 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
// target there if the PDF file isn't present.)  If not, see
// <http://www.gnu.org/licenses/> for a copy.
// <http://www.gnu.org/licenses/> for a copy.
//
//
// License:     GPL, v3, as defined and found on www.gnu.org,
// License:     GPL, v3, as defined and found on www.gnu.org,
//              http://www.gnu.org/licenses/gpl.html
//              http://www.gnu.org/licenses/gpl.html
//
//
//
//
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
//
//
//
//
`define DMA_IDLE        3'b000
`define DMA_IDLE        3'b000
`define DMA_WAIT        3'b001
`define DMA_WAIT        3'b001
`define DMA_READ_REQ    3'b010
`define DMA_READ_REQ    3'b010
`define DMA_READ_ACK    3'b011
`define DMA_READ_ACK    3'b011
`define DMA_PRE_WRITE   3'b100
`define DMA_PRE_WRITE   3'b100
`define DMA_WRITE_REQ   3'b101
`define DMA_WRITE_REQ   3'b101
`define DMA_WRITE_ACK   3'b110
`define DMA_WRITE_ACK   3'b110
 
 
module wbdmac(i_clk, i_rst,
module wbdmac(i_clk, i_reset,
                i_swb_cyc, i_swb_stb, i_swb_we, i_swb_addr, i_swb_data,
                i_swb_cyc, i_swb_stb, i_swb_we, i_swb_addr, i_swb_data,
                        o_swb_ack, o_swb_stall, o_swb_data,
                        o_swb_ack, o_swb_stall, o_swb_data,
                o_mwb_cyc, o_mwb_stb, o_mwb_we, o_mwb_addr, o_mwb_data,
                o_mwb_cyc, o_mwb_stb, o_mwb_we, o_mwb_addr, o_mwb_data,
                        i_mwb_ack, i_mwb_stall, i_mwb_data, i_mwb_err,
                        i_mwb_ack, i_mwb_stall, i_mwb_data, i_mwb_err,
                i_dev_ints,
                i_dev_ints,
                o_interrupt);
                o_interrupt);
        parameter       ADDRESS_WIDTH=32, LGMEMLEN = 10,
        parameter       ADDRESS_WIDTH=30, LGMEMLEN = 10, DW=32;
                        DW=32, LGDV=5,AW=ADDRESS_WIDTH;
        localparam      LGDV=5;
        input                   i_clk, i_rst;
        localparam      AW=ADDRESS_WIDTH;
 
        input   wire            i_clk, i_reset;
        // Slave/control wishbone inputs
        // Slave/control wishbone inputs
        input                   i_swb_cyc, i_swb_stb, i_swb_we;
        input   wire            i_swb_cyc, i_swb_stb, i_swb_we;
        input   [1:0]            i_swb_addr;
        input   wire    [1:0]    i_swb_addr;
        input   [(DW-1):0]       i_swb_data;
        input   wire [(DW-1):0]  i_swb_data;
        // Slave/control wishbone outputs
        // Slave/control wishbone outputs
        output  reg             o_swb_ack;
        output  reg             o_swb_ack;
        output  wire            o_swb_stall;
        output  wire            o_swb_stall;
        output  reg [(DW-1):0]   o_swb_data;
        output  reg [(DW-1):0]   o_swb_data;
        // Master/DMA wishbone control
        // Master/DMA wishbone control
        output  wire            o_mwb_cyc, o_mwb_stb, o_mwb_we;
        output  wire            o_mwb_cyc, o_mwb_stb, o_mwb_we;
        output  reg [(AW-1):0]   o_mwb_addr;
        output  reg [(AW-1):0]   o_mwb_addr;
        output  reg [(DW-1):0]   o_mwb_data;
        output  reg [(DW-1):0]   o_mwb_data;
        // Master/DMA wishbone responses from the bus
        // Master/DMA wishbone responses from the bus
        input                   i_mwb_ack, i_mwb_stall;
        input   wire            i_mwb_ack, i_mwb_stall;
        input   [(DW-1):0]       i_mwb_data;
        input   wire [(DW-1):0]  i_mwb_data;
        input                   i_mwb_err;
        input   wire            i_mwb_err;
        // The interrupt device interrupt lines
        // The interrupt device interrupt lines
        input   [(DW-1):0]       i_dev_ints;
        input   wire [(DW-1):0]  i_dev_ints;
        // An interrupt to be set upon completion
        // An interrupt to be set upon completion
        output  reg             o_interrupt;
        output  reg             o_interrupt;
        // Need to release the bus for a higher priority user
        // Need to release the bus for a higher priority user
        //      This logic had lots of problems, so it is being
        //      This logic had lots of problems, so it is being
        //      removed.  If you want to make sure the bus is available
        //      removed.  If you want to make sure the bus is available
        //      for a higher priority user, adjust the transfer length
        //      for a higher priority user, adjust the transfer length
        //      accordingly.
        //      accordingly.
        //
        //
        // input                        i_other_busmaster_requests_bus;
        // input                        i_other_busmaster_requests_bus;
        //
        //
 
 
 
        wire    s_cyc, s_stb, s_we;
 
        wire    [1:0]    s_addr;
 
        wire    [31:0]   s_data;
 
`define DELAY_ACCESS
 
`ifdef  DELAY_ACCESS
 
        reg     r_s_cyc, r_s_stb, r_s_we;
 
        reg     [1:0]    r_s_addr;
 
        reg     [31:0]   r_s_data;
 
 
 
        always @(posedge i_clk)
 
                r_s_cyc <= i_swb_cyc;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                r_s_stb <= 1'b0;
 
        else
 
                r_s_stb <= i_swb_stb;
 
        always @(posedge i_clk)
 
                r_s_we  <= i_swb_we;
 
        always @(posedge i_clk)
 
                r_s_addr<= i_swb_addr;
 
        always @(posedge i_clk)
 
                r_s_data<= i_swb_data;
 
 
 
        assign  s_cyc = r_s_cyc;
 
        assign  s_stb = r_s_stb;
 
        assign  s_we  = r_s_we;
 
        assign  s_addr= r_s_addr;
 
        assign  s_data= r_s_data;
 
`else
 
        assign  s_cyc = i_swb_cyc;
 
        assign  s_stb = i_swb_stb;
 
        assign  s_we  = i_swb_we;
 
        assign  s_addr= i_swb_addr;
 
        assign  s_data= i_swb_data;
 
`endif
 
 
        reg     [2:0]            dma_state;
        reg     [2:0]            dma_state;
        reg                     cfg_err, cfg_len_nonzero;
        reg                     cfg_err, cfg_len_nonzero;
        reg     [(AW-1):0]       cfg_waddr, cfg_raddr, cfg_len;
        reg     [(AW-1):0]       cfg_waddr, cfg_raddr, cfg_len;
        reg [(LGMEMLEN-1):0]     cfg_blocklen_sub_one;
        reg [(LGMEMLEN-1):0]     cfg_blocklen_sub_one;
        reg                     cfg_incs, cfg_incd;
        reg                     cfg_incs, cfg_incd;
        reg     [(LGDV-1):0]     cfg_dev_trigger;
        reg     [(LGDV-1):0]     cfg_dev_trigger;
        reg                     cfg_on_dev_trigger;
        reg                     cfg_on_dev_trigger;
 
 
        // Single block operations: We'll read, then write, up to a single
        // Single block operations: We'll read, then write, up to a single
        // memory block here.
        // memory block here.
 
 
        reg     [(DW-1):0]       dma_mem [0:(((1<<LGMEMLEN))-1)];
        reg     [(DW-1):0]       dma_mem [0:(((1<<LGMEMLEN))-1)];
        reg     [(LGMEMLEN):0]   nread, nwritten, nwacks, nracks;
        reg     [(LGMEMLEN):0]   nread, nwritten, nwacks, nracks;
        wire    [(AW-1):0]       bus_nracks;
        wire    [(AW-1):0]       bus_nracks;
        assign  bus_nracks = { {(AW-LGMEMLEN-1){1'b0}}, nracks };
        assign  bus_nracks = { {(AW-LGMEMLEN-1){1'b0}}, nracks };
 
 
        reg     last_read_request, last_read_ack,
        reg     last_read_request, last_read_ack,
                last_write_request, last_write_ack;
                last_write_request, last_write_ack;
        reg     trigger, abort, user_halt;
        reg     trigger, abort, user_halt;
 
 
        initial dma_state = `DMA_IDLE;
        initial dma_state = `DMA_IDLE;
        initial o_interrupt = 1'b0;
        initial o_interrupt = 1'b0;
        initial cfg_len     = {(AW){1'b0}};
 
        initial cfg_blocklen_sub_one = {(LGMEMLEN){1'b1}};
        initial cfg_blocklen_sub_one = {(LGMEMLEN){1'b1}};
        initial cfg_on_dev_trigger = 1'b0;
        initial cfg_on_dev_trigger = 1'b0;
        initial cfg_len_nonzero = 1'b0;
 
        always @(posedge i_clk)
        always @(posedge i_clk)
        case(dma_state)
        if (i_reset)
 
        begin
 
                dma_state <= `DMA_IDLE;
 
                cfg_on_dev_trigger <= 1'b0;
 
                cfg_incs  <= 1'b0;
 
                cfg_incd  <= 1'b0;
 
        end else case(dma_state)
        `DMA_IDLE: begin
        `DMA_IDLE: begin
                o_mwb_addr <= cfg_raddr;
                o_mwb_addr <= cfg_raddr;
                nwritten   <= 0;
 
                nread      <= 0;
 
                nracks     <= 0;
 
                nwacks     <= 0;
 
                cfg_len_nonzero <= (|cfg_len);
 
 
 
                // When the slave wishbone writes, and we are in this 
                // When the slave wishbone writes, and we are in this 
                // (ready) configuration, then allow the DMA to be controlled
                // (ready) configuration, then allow the DMA to be controlled
                // and thus to start.
                // and thus to start.
                if ((i_swb_stb)&&(i_swb_we))
                if ((s_stb)&&(s_we))
                begin
                begin
                        case(i_swb_addr)
                        case(s_addr)
                        2'b00: begin
                        2'b00: begin
                                if ((i_swb_data[31:16] == 16'h0fed)
                                if ((s_data[27:16] == 12'hfed)
 
                                        &&(s_data[31:30] == 2'b00)
                                                &&(cfg_len_nonzero))
                                                &&(cfg_len_nonzero))
                                        dma_state <= `DMA_WAIT;
                                        dma_state <= `DMA_WAIT;
                                cfg_blocklen_sub_one
                                cfg_blocklen_sub_one
                                        <= i_swb_data[(LGMEMLEN-1):0]
                                        <= s_data[(LGMEMLEN-1):0]
                                        + {(LGMEMLEN){1'b1}};
                                        + {(LGMEMLEN){1'b1}};
                                        // i.e. -1;
                                        // i.e. -1;
                                cfg_dev_trigger    <= i_swb_data[14:10];
                                cfg_dev_trigger    <= s_data[14:10];
                                cfg_on_dev_trigger <= i_swb_data[15];
                                cfg_on_dev_trigger <= s_data[15];
                                cfg_incs  <= ~i_swb_data[29];
                                cfg_incs  <= !s_data[29];
                                cfg_incd  <= ~i_swb_data[28];
                                cfg_incd  <= !s_data[28];
                                end
                                end
                        2'b01: begin
                        2'b01: begin end // This is done elsewhere
                                cfg_len   <=  i_swb_data[(AW-1):0];
                        2'b10: cfg_raddr <=  s_data[(AW+2-1):2];
                                cfg_len_nonzero <= (|i_swb_data[(AW-1):0]);
                        2'b11: cfg_waddr <=  s_data[(AW+2-1):2];
                                end
 
                        2'b10: cfg_raddr <=  i_swb_data[(AW-1):0];
 
                        2'b11: cfg_waddr <=  i_swb_data[(AW-1):0];
 
                        endcase
                        endcase
                end end
                end end
        `DMA_WAIT: begin
        `DMA_WAIT: begin
                o_mwb_addr <= cfg_raddr;
                o_mwb_addr <= cfg_raddr;
                nracks     <= 0;
 
                nwacks     <= 0;
 
                nwritten   <= 0;
 
                nread      <= 0;
 
                if (abort)
                if (abort)
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                else if (user_halt)
                else if (user_halt)
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                else if (trigger)
                else if (trigger)
                        dma_state <= `DMA_READ_REQ;
                        dma_state <= `DMA_READ_REQ;
                end
                end
        `DMA_READ_REQ: begin
        `DMA_READ_REQ: begin
                nwritten  <= 0;
                if (!i_mwb_stall)
 
 
                if (~i_mwb_stall)
 
                begin
                begin
                        // Number of read acknowledgements needed
                        // Number of read acknowledgements needed
                        nracks <= nracks+1;
                        if ((last_read_request)||(user_halt))
                        if (last_read_request)
 
        //((nracks == {1'b0, cfg_blocklen_sub_one})||(bus_nracks == cfg_len-1))
        //((nracks == {1'b0, cfg_blocklen_sub_one})||(bus_nracks == cfg_len-1))
                                // Wishbone interruptus
                                // Wishbone interruptus
                                dma_state <= `DMA_READ_ACK;
                                dma_state <= `DMA_READ_ACK;
                        if (cfg_incs)
                        if (cfg_incs)
                                o_mwb_addr <= o_mwb_addr
                                o_mwb_addr <= o_mwb_addr
                                                + {{(AW-1){1'b0}},1'b1};
                                                + {{(AW-1){1'b0}},1'b1};
                end
                end
 
 
                if (user_halt)
                if ((i_mwb_err)||(abort))
                        dma_state <= `DMA_READ_ACK;
 
                if (i_mwb_err)
 
                begin
 
                        cfg_len <= 0;
 
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                end
                else if (i_mwb_ack)
 
 
                if (abort)
 
                        dma_state <= `DMA_IDLE;
 
                if (i_mwb_ack)
 
                begin
                begin
                        nread <= nread+1;
 
                        if (cfg_incs)
                        if (cfg_incs)
                                cfg_raddr  <= cfg_raddr
                                cfg_raddr  <= cfg_raddr
                                                + {{(AW-1){1'b0}},1'b1};
                                                + {{(AW-1){1'b0}},1'b1};
 
                        if (last_read_ack)
 
                                dma_state <= `DMA_PRE_WRITE;
                end end
                end end
        `DMA_READ_ACK: begin
        `DMA_READ_ACK: begin
                nwritten  <= 0;
                if ((i_mwb_err)||(abort))
 
 
                if (i_mwb_err)
 
                begin
 
                        cfg_len <= 0;
 
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                end else if (i_mwb_ack)
                else if (i_mwb_ack)
                begin
                begin
                        nread <= nread+1;
 
                        if (last_read_ack) // (nread+1 == nracks)
                        if (last_read_ack) // (nread+1 == nracks)
                                dma_state  <= `DMA_PRE_WRITE;
                                dma_state  <= `DMA_PRE_WRITE;
                        if (user_halt)
                        if (user_halt)
                                dma_state <= `DMA_IDLE;
                                dma_state <= `DMA_IDLE;
                        if (cfg_incs)
                        if (cfg_incs)
                                cfg_raddr  <= cfg_raddr
                                cfg_raddr  <= cfg_raddr
                                                + {{(AW-1){1'b0}},1'b1};
                                                + {{(AW-1){1'b0}},1'b1};
                end
                end
                if (abort)
 
                        dma_state <= `DMA_IDLE;
 
                end
                end
        `DMA_PRE_WRITE: begin
        `DMA_PRE_WRITE: begin
                o_mwb_addr <= cfg_waddr;
                o_mwb_addr <= cfg_waddr;
                dma_state <= (abort)?`DMA_IDLE:`DMA_WRITE_REQ;
                dma_state <= (abort)?`DMA_IDLE:`DMA_WRITE_REQ;
                end
                end
        `DMA_WRITE_REQ: begin
        `DMA_WRITE_REQ: begin
                if (~i_mwb_stall)
                if (!i_mwb_stall)
                begin
                begin
                        nwritten <= nwritten+1;
 
                        if (last_write_request) // (nwritten == nread-1)
                        if (last_write_request) // (nwritten == nread-1)
                                // Wishbone interruptus
                                // Wishbone interruptus
                                dma_state <= `DMA_WRITE_ACK;
                                dma_state <= `DMA_WRITE_ACK;
                        if (cfg_incd)
                        if (cfg_incd)
                        begin
                        begin
                                o_mwb_addr <= o_mwb_addr
                                o_mwb_addr <= o_mwb_addr
                                                + {{(AW-1){1'b0}},1'b1};
                                                + {{(AW-1){1'b0}},1'b1};
                                cfg_waddr  <= cfg_waddr
                                cfg_waddr  <= cfg_waddr
                                                + {{(AW-1){1'b0}},1'b1};
                                                + {{(AW-1){1'b0}},1'b1};
                        end
                        end
                end
                end
 
 
                if (i_mwb_err)
                if ((i_mwb_err)||(abort))
                begin
 
                        cfg_len  <= 0;
 
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                end
                else if ((i_mwb_ack)&&(last_write_ack))
                if (i_mwb_ack)
                        dma_state <= (cfg_len <= 1)?`DMA_IDLE:`DMA_WAIT;
                begin
                else if (!cfg_len_nonzero)
                        nwacks <= nwacks+1;
 
                        cfg_len <= cfg_len +{(AW){1'b1}}; // -1
 
                end
 
                if (user_halt)
 
                        dma_state <= `DMA_WRITE_ACK;
 
                if (abort)
 
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                end
                end
        `DMA_WRITE_ACK: begin
        `DMA_WRITE_ACK: begin
                if (i_mwb_err)
                if ((i_mwb_err)||(abort))
                begin
 
                        cfg_len  <= 0;
 
                        nread    <= 0;
 
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                end else if (i_mwb_ack)
                else if ((i_mwb_ack)&&(last_write_ack))
                begin
                        // (nwacks+1 == nwritten)
                        nwacks <= nwacks+1;
                        dma_state <= (cfg_len <= 1)?`DMA_IDLE:`DMA_WAIT;
                        cfg_len <= cfg_len +{(AW){1'b1}};//cfg_len -= 1;
                else if (!cfg_len_nonzero)
                        if (last_write_ack) // (nwacks+1 == nwritten)
 
                        begin
 
                                nread <= 0;
 
                                dma_state <= (cfg_len == 1)?`DMA_IDLE:`DMA_WAIT;
 
                        end
 
                end
 
 
 
                if (abort)
 
                        dma_state <= `DMA_IDLE;
                        dma_state <= `DMA_IDLE;
                end
                end
        default:
        default:
                dma_state <= `DMA_IDLE;
                dma_state <= `DMA_IDLE;
        endcase
        endcase
 
 
        initial o_interrupt = 1'b0;
        initial o_interrupt = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
 
                o_interrupt <= 1'b0;
 
        else
                o_interrupt <= ((dma_state == `DMA_WRITE_ACK)&&(i_mwb_ack)
                o_interrupt <= ((dma_state == `DMA_WRITE_ACK)&&(i_mwb_ack)
                                        &&(last_write_ack)
                                        &&(last_write_ack)
                                        &&(cfg_len == {{(AW-1){1'b0}},1'b1}))
                                        &&(cfg_len == {{(AW-1){1'b0}},1'b1}))
                                ||((dma_state != `DMA_IDLE)&&(i_mwb_err));
                                ||((dma_state != `DMA_IDLE)&&(i_mwb_err));
 
 
 
 
 
        initial cfg_len     = 0;
 
        initial cfg_len_nonzero = 1'b0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
        begin
 
                cfg_len <= 0;
 
                cfg_len_nonzero <= 1'b0;
 
        end else if ((dma_state == `DMA_IDLE)
 
                        &&(s_stb)&&(s_we)&&(s_addr == 2'b01))
 
        begin
 
                cfg_len   <=  s_data[(AW-1):0];
 
                cfg_len_nonzero <= (|s_data[(AW-1):0]);
 
        end else if ((o_mwb_cyc)&&(o_mwb_we)&&(i_mwb_ack))
 
        begin
 
                cfg_len <= cfg_len - 1'b1;
 
                cfg_len_nonzero <= (cfg_len > 1);
 
        end
 
 
 
        initial nracks   = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                nracks <= 0;
 
        else if ((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT))
 
                nracks <= 0;
 
        else if ((o_mwb_stb)&&(!o_mwb_we)&&(!i_mwb_stall))
 
                nracks <= nracks + 1'b1;
 
 
 
        initial nread   = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                nread <= 0;
 
        else if ((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT))
 
                nread <= 0;
 
        else if ((!o_mwb_we)&&(i_mwb_ack))
 
                nread <= nread + 1'b1;
 
 
 
        initial nwritten = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                nwritten <= 0;
 
        else if ((!o_mwb_cyc)||(!o_mwb_we))
 
                nwritten <= 0;
 
        else if ((o_mwb_stb)&&(!i_mwb_stall))
 
                nwritten <= nwritten + 1'b1;
 
 
 
        initial nwacks   = 0;
 
        always @(posedge i_clk)
 
        if (i_reset)
 
                nwacks <= 0;
 
        else if ((!o_mwb_cyc)||(!o_mwb_we))
 
                nwacks <= 0;
 
        else if (i_mwb_ack)
 
                nwacks <= nwacks + 1'b1;
 
 
        initial cfg_err = 1'b0;
        initial cfg_err = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (dma_state == `DMA_IDLE)
        if (i_reset)
 
                cfg_err <= 1'b0;
 
        else if (dma_state == `DMA_IDLE)
                begin
                begin
                        if ((i_swb_stb)&&(i_swb_we)&&(i_swb_addr==2'b00))
                if ((s_stb)&&(s_we)&&(s_addr==2'b00))
                                cfg_err <= 1'b0;
                                cfg_err <= 1'b0;
                end else if (((i_mwb_err)&&(o_mwb_cyc))||(abort))
        end else if (((i_mwb_err)&&(o_mwb_cyc))||(abort))
                        cfg_err <= 1'b1;
                cfg_err <= 1'b1;
 
 
        initial last_read_request = 1'b0;
        initial last_read_request = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((dma_state == `DMA_WAIT)||(dma_state == `DMA_READ_REQ))
        if (i_reset)
 
                last_read_request <= 1'b0;
 
        else if ((dma_state == `DMA_WAIT)||(dma_state == `DMA_READ_REQ))
                begin
                begin
                        if ((~i_mwb_stall)&&(dma_state == `DMA_READ_REQ))
                if ((!i_mwb_stall)&&(dma_state == `DMA_READ_REQ))
                        begin
                        begin
                                last_read_request <=
                        last_read_request <=
                                (nracks + 1 == { 1'b0, cfg_blocklen_sub_one})
                        (nracks + 1 == { 1'b0, cfg_blocklen_sub_one})
                                        ||(bus_nracks == cfg_len-2);
                                ||(bus_nracks == cfg_len-2);
                        end else
                end else
                                last_read_request <=
                        last_read_request <=
                                        (nracks== { 1'b0, cfg_blocklen_sub_one})
                                (nracks== { 1'b0, cfg_blocklen_sub_one})
                                        ||(bus_nracks == cfg_len-1);
                                ||(bus_nracks == cfg_len-1);
                end else
        end else
                        last_read_request <= 1'b0;
                last_read_request <= 1'b0;
 
 
 
 
 
        wire    [(LGMEMLEN):0]   next_nread;
 
        assign  next_nread = nread + 1'b1;
 
 
        initial last_read_ack = 1'b0;
        initial last_read_ack = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((dma_state == `DMA_READ_REQ)||(dma_state == `DMA_READ_ACK))
        if (i_reset)
 
                last_read_ack <= 0;
 
        else if (dma_state == `DMA_READ_REQ)
 
        begin
 
                if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
 
                        last_read_ack <= (next_nread == { 1'b0, cfg_blocklen_sub_one });
 
                else
 
                        last_read_ack <= (nread == { 1'b0, cfg_blocklen_sub_one });
 
        end else if (dma_state == `DMA_READ_ACK)
                begin
                begin
                        if ((i_mwb_ack)&&((~o_mwb_stb)||(i_mwb_stall)))
                if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
                                last_read_ack <= (nread+2 == nracks);
                                last_read_ack <= (nread+2 == nracks);
                        else
                        else
                                last_read_ack <= (nread+1 == nracks);
                        last_read_ack <= (next_nread == nracks);
                end else
                end else
                        last_read_ack <= 1'b0;
                last_read_ack <= 1'b0;
 
 
        initial last_write_request = 1'b0;
        initial last_write_request = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (dma_state == `DMA_PRE_WRITE)
        if (i_reset)
 
                last_write_request <= 1'b0;
 
        else if (dma_state == `DMA_PRE_WRITE)
                        last_write_request <= (nread <= 1);
                        last_write_request <= (nread <= 1);
                else if (dma_state == `DMA_WRITE_REQ)
        else if (dma_state == `DMA_WRITE_REQ)
                begin
        begin
                        if (i_mwb_stall)
                if (i_mwb_stall)
                                last_write_request <= (nwritten >= nread-1);
                        last_write_request <= (nwritten >= nread-1);
                        else
                else
                                last_write_request <= (nwritten >= nread-2);
                        last_write_request <= (nwritten >= nread-2);
                end else
        end else
                        last_write_request <= 1'b0;
                last_write_request <= 1'b0;
 
 
        initial last_write_ack = 1'b0;
        initial last_write_ack = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if((dma_state == `DMA_WRITE_REQ)||(dma_state == `DMA_WRITE_ACK))
        if (i_reset)
 
                last_write_ack <= 1'b0;
 
        else if((dma_state == `DMA_WRITE_REQ)||(dma_state == `DMA_WRITE_ACK))
                begin
                begin
                        if ((i_mwb_ack)&&((~o_mwb_stb)||(i_mwb_stall)))
                if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
                                last_write_ack <= (nwacks+2 == nwritten);
                                last_write_ack <= (nwacks+2 == nwritten);
                        else
                else
                                last_write_ack <= (nwacks+1 == nwritten);
                        last_write_ack <= (nwacks+1 == nwritten);
                end else
        end else
                        last_write_ack <= 1'b0;
                last_write_ack <= 1'b0;
 
 
 
 
        assign  o_mwb_cyc = (dma_state == `DMA_READ_REQ)
        assign  o_mwb_cyc = (dma_state == `DMA_READ_REQ)
                        ||(dma_state == `DMA_READ_ACK)
                        ||(dma_state == `DMA_READ_ACK)
                        ||(dma_state == `DMA_WRITE_REQ)
                        ||(dma_state == `DMA_WRITE_REQ)
                        ||(dma_state == `DMA_WRITE_ACK);
                        ||(dma_state == `DMA_WRITE_ACK);
 
 
        assign  o_mwb_stb = (dma_state == `DMA_READ_REQ)
        assign  o_mwb_stb = (dma_state == `DMA_READ_REQ)
                        ||(dma_state == `DMA_WRITE_REQ);
                        ||(dma_state == `DMA_WRITE_REQ);
 
 
        assign  o_mwb_we = (dma_state == `DMA_PRE_WRITE)
        assign  o_mwb_we = (dma_state == `DMA_PRE_WRITE)
                        ||(dma_state == `DMA_WRITE_REQ)
                        ||(dma_state == `DMA_WRITE_REQ)
                        ||(dma_state == `DMA_WRITE_ACK);
                        ||(dma_state == `DMA_WRITE_ACK);
 
 
        //
        //
        // This is tricky.  In order for Vivado to consider dma_mem to be a 
        // This is tricky.  In order for Vivado to consider dma_mem to be a 
        // proper memory, it must have a simple address fed into it.  Hence
        // proper memory, it must have a simple address fed into it.  Hence
        // the read_address (rdaddr) register.  The problem is that this
        // the read_address (rdaddr) register.  The problem is that this
        // register must always be one greater than the address we actually
        // register must always be one greater than the address we actually
        // want to read from, unless we are idling.  So ... the math is touchy.
        // want to read from, unless we are idling.  So ... the math is touchy.
        //
        //
        reg     [(LGMEMLEN-1):0] rdaddr;
        reg     [(LGMEMLEN-1):0] rdaddr;
 
 
 
        initial rdaddr = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT)
        if (i_reset)
 
                rdaddr <= 0;
 
        else if((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT)
                                ||(dma_state == `DMA_WRITE_ACK))
                                ||(dma_state == `DMA_WRITE_ACK))
                        rdaddr <= 0;
                rdaddr <= 0;
                else if ((dma_state == `DMA_PRE_WRITE)
                else if ((dma_state == `DMA_PRE_WRITE)
                                ||((dma_state==`DMA_WRITE_REQ)&&(~i_mwb_stall)))
                        ||((dma_state==`DMA_WRITE_REQ)&&(!i_mwb_stall)))
                        rdaddr <= rdaddr + {{(LGMEMLEN-1){1'b0}},1'b1};
                        rdaddr <= rdaddr + {{(LGMEMLEN-1){1'b0}},1'b1};
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                if ((dma_state != `DMA_WRITE_REQ)||(~i_mwb_stall))
        if (i_reset)
 
                o_mwb_data <= 0;
 
        else if ((dma_state != `DMA_WRITE_REQ)||(!i_mwb_stall))
                        o_mwb_data <= dma_mem[rdaddr];
                        o_mwb_data <= dma_mem[rdaddr];
        always @(posedge i_clk)
        always @(posedge i_clk)
                if((dma_state == `DMA_READ_REQ)||(dma_state == `DMA_READ_ACK))
                if((dma_state == `DMA_READ_REQ)||(dma_state == `DMA_READ_ACK))
                        dma_mem[nread[(LGMEMLEN-1):0]] <= i_mwb_data;
                        dma_mem[nread[(LGMEMLEN-1):0]] <= i_mwb_data;
 
 
        always @(posedge i_clk)
        always @(posedge i_clk)
                casez(i_swb_addr)
        if (i_reset)
 
                o_swb_data <= 0;
 
        else casez(s_addr)
                2'b00: o_swb_data <= {  (dma_state != `DMA_IDLE), cfg_err,
                2'b00: o_swb_data <= {  (dma_state != `DMA_IDLE), cfg_err,
                                        ~cfg_incs, ~cfg_incd,
                                        !cfg_incs, !cfg_incd,
                                        1'b0, nread,
                                        1'b0, nread,
                                        cfg_on_dev_trigger, cfg_dev_trigger,
                                        cfg_on_dev_trigger, cfg_dev_trigger,
                                        cfg_blocklen_sub_one
                                        cfg_blocklen_sub_one
                                        };
                                        };
                2'b01: o_swb_data <= { {(DW-AW){1'b0}}, cfg_len  };
                2'b01: o_swb_data <= { {(DW-AW){1'b0}}, cfg_len  };
                2'b10: o_swb_data <= { {(DW-AW){1'b0}}, cfg_raddr};
                2'b10: o_swb_data <= { {(DW-2-AW){1'b0}}, cfg_raddr, 2'b00 };
                2'b11: o_swb_data <= { {(DW-AW){1'b0}}, cfg_waddr};
                2'b11: o_swb_data <= { {(DW-2-AW){1'b0}}, cfg_waddr, 2'b00 };
                endcase
                endcase
 
 
        // This causes us to wait a minimum of two clocks before starting: One
        // This causes us to wait a minimum of two clocks before starting: One
        // to go into the wait state, and then one while in the wait state to
        // to go into the wait state, and then one while in the wait state to
        // develop the trigger.
        // develop the trigger.
        initial trigger = 1'b0;
        initial trigger = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
 
                trigger <= 1'b0;
 
        else
                trigger <=  (dma_state == `DMA_WAIT)
                trigger <=  (dma_state == `DMA_WAIT)
                                &&((~cfg_on_dev_trigger)
                                &&((!cfg_on_dev_trigger)
                                        ||(i_dev_ints[cfg_dev_trigger]));
                                        ||(i_dev_ints[cfg_dev_trigger]));
 
 
        // Ack any access.  We'll quietly ignore any access where we are busy,
        // Ack any access.  We'll quietly ignore any access where we are busy,
        // but ack it anyway.  In other words, before writing to the device,
        // but ack it anyway.  In other words, before writing to the device,
        // double check that it isn't busy, and then write.
        // double check that it isn't busy, and then write.
 
        initial o_swb_ack = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                o_swb_ack <= (i_swb_stb);
        if (i_reset)
 
                o_swb_ack <= 1'b0;
 
        else if (!i_swb_cyc)
 
                o_swb_ack <= 1'b0;
 
        else
 
                o_swb_ack <= (s_stb);
 
 
        assign  o_swb_stall = 1'b0;
        assign  o_swb_stall = 1'b0;
 
 
        initial abort = 1'b0;
        initial abort = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                abort <= (i_rst)||((i_swb_stb)&&(i_swb_we)
        if (i_reset)
                        &&(i_swb_addr == 2'b00)
                abort <= 1'b0;
                        &&(i_swb_data == 32'hffed0000));
        else if (dma_state == `DMA_IDLE)
 
                abort <= 1'b0;
 
        else
 
                abort <= ((s_stb)&&(s_we)
 
                        &&(s_addr == 2'b00)
 
                        &&(s_data == 32'hffed0000));
 
 
        initial user_halt = 1'b0;
        initial user_halt = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                user_halt <= ((user_halt)&&(dma_state != `DMA_IDLE))
                user_halt <= ((user_halt)&&(dma_state != `DMA_IDLE))
                        ||((i_swb_stb)&&(i_swb_we)&&(dma_state != `DMA_IDLE)
                        ||((s_stb)&&(s_we)&&(dma_state != `DMA_IDLE)
                                &&(i_swb_addr == 2'b00)
                                &&(s_addr == 2'b00)
                                &&(i_swb_data == 32'hafed0000));
                                &&(s_data == 32'hafed0000));
 
 
 
 
 
        // Make verilator happy
 
        // verilator lint_off UNUSED
 
        wire    unused;
 
        assign  unused = s_cyc;
 
        // verilator lint_on  UNUSED
 
`ifdef  FORMAL
 
        reg     f_past_valid;
 
        initial f_past_valid = 1'b0;
 
        always @(posedge i_clk)
 
                f_past_valid <= 1'b1;
 
 
 
        always @(*)
 
        if (!f_past_valid)
 
                assume(i_reset);
 
 
 
        always @(posedge i_clk)
 
        if ((!f_past_valid)||($past(i_reset)))
 
                assert(dma_state == `DMA_IDLE);
 
 
 
        parameter       F_SLV_LGDEPTH = 3;
 
        parameter       F_MSTR_LGDEPTH = LGMEMLEN+1;
 
 
 
        wire [F_SLV_LGDEPTH-1:0] f_swb_nreqs, f_swb_nacks, f_swb_outstanding;
 
        wire [F_MSTR_LGDEPTH-1:0] f_mwb_nreqs, f_mwb_nacks, f_mwb_outstanding;
 
 
 
        fwb_slave #(
 
                .AW(2), .DW(32), .F_MAX_STALL(0), .F_MAX_ACK_DELAY(2),
 
                        .F_LGDEPTH(F_SLV_LGDEPTH)
 
                ) control_port(i_clk, i_reset,
 
                i_swb_cyc, i_swb_stb, i_swb_we, i_swb_addr, i_swb_data,4'b1111,
 
                        o_swb_ack, o_swb_stall, o_swb_data, 1'b0,
 
                        f_swb_nreqs, f_swb_nacks, f_swb_outstanding);
 
        always @(*)
 
                assert(o_swb_stall == 0);
 
`ifdef  DELAY_ACCESS
 
        always @(*)
 
        if ((!i_reset)&&(i_swb_cyc))
 
        begin
 
                if ((!s_stb)&&(!o_swb_ack))
 
                        assert(f_swb_outstanding == 0);
 
                else if ((s_stb)&&(!o_swb_ack))
 
                        assert(f_swb_outstanding == 1);
 
                else if ((!s_stb)&&(o_swb_ack))
 
                        assert(f_swb_outstanding == 1);
 
                else if ((s_stb)&&(o_swb_ack))
 
                        assert(f_swb_outstanding == 2);
 
        end
 
`else
 
        always @(*)
 
        if ((!i_reset)&&(!o_swb_ack))
 
                assert(f_swb_outstanding == 0);
 
`endif
 
 
 
        fwb_master #(.AW(AW), .DW(32), .F_MAX_STALL(4), .F_MAX_ACK_DELAY(8),
 
                        .F_LGDEPTH(F_MSTR_LGDEPTH),
 
                        .F_OPT_RMW_BUS_OPTION(1'b1),
 
                        .F_OPT_DISCONTINUOUS(1'b0),
 
                        .F_OPT_SOURCE(1'b1)
 
                ) external_bus(i_clk, i_reset,
 
                o_mwb_cyc, o_mwb_stb, o_mwb_we, o_mwb_addr, o_mwb_data,4'b1111,
 
                        i_mwb_ack, i_mwb_stall, i_mwb_data, i_mwb_err,
 
                        f_mwb_nreqs, f_mwb_nacks, f_mwb_outstanding);
 
 
endmodule
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(dma_state == `DMA_IDLE)))
 
                assert(o_mwb_cyc == 1'b0);
 
 
 
        always @(*)
 
        if ((o_mwb_cyc)&&(!o_mwb_we))
 
        begin
 
                assert(nracks == f_mwb_nreqs);
 
                assert(nread == f_mwb_nacks);
 
        end
 
 
 
        always @(*)
 
        if ((o_mwb_cyc)&&(o_mwb_we))
 
        begin
 
                assert(nwacks   == f_mwb_nacks);
 
                assert(nwritten == f_mwb_nreqs);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(abort))&&($past(dma_state != `DMA_IDLE)))
 
                assert(dma_state == `DMA_IDLE);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_mwb_cyc))&&(o_mwb_cyc)&&(
 
                        ((  !cfg_incs)&&(!o_mwb_we))
 
                        ||((!cfg_incd)&&( o_mwb_we))))
 
        begin
 
                assert(o_mwb_addr == $past(o_mwb_addr));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_mwb_cyc))&&(
 
                        ((!cfg_incs)||($past(o_mwb_we))||(!$past(i_mwb_ack)))))
 
                assert(cfg_raddr == $past(cfg_raddr));
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(dma_state == `DMA_WRITE_REQ))
 
                assert(cfg_waddr == o_mwb_addr);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))
 
                        &&($past(o_mwb_stb))&&(!$past(i_mwb_stall)))
 
        begin
 
                assert(   ((!cfg_incs)&&(!$past(o_mwb_we)))
 
                        ||((!cfg_incd)&&( $past(o_mwb_we)))
 
                        ||(o_mwb_addr==$past(o_mwb_addr)+1'b1));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(o_mwb_cyc))&&(o_mwb_cyc))
 
        begin
 
                if (o_mwb_we)
 
                        assert(o_mwb_addr == cfg_waddr);
 
                else
 
                        assert(o_mwb_addr == cfg_raddr);
 
        end
 
 
 
        always @(*)
 
        assert(cfg_len_nonzero == (cfg_len != 0));
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_reset)))
 
        begin
 
                assert(cfg_len == 0);
 
                assert(!cfg_len_nonzero);
 
        end else if ((f_past_valid)&&($past(o_mwb_cyc)))
 
        begin
 
                if (($past(i_mwb_ack))&&($past(o_mwb_we)))
 
                        assert(cfg_len == $past(cfg_len)-1'b1);
 
                else
 
                        assert(cfg_len == $past(cfg_len));
 
        end else if ((f_past_valid)&&(($past(dma_state) != `DMA_IDLE)
 
                        ||(!$past(s_stb))||(!$past(s_we))
 
                        ||($past(s_addr)!=2'b01)))
 
                assert(cfg_len == $past(cfg_len));
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(o_mwb_cyc))&&($past(cfg_len == 0))
 
                        &&(!$past(user_halt)))
 
        begin
 
                assert(cfg_len == 0);
 
                assert((dma_state != $past(dma_state))||(!o_mwb_cyc));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if (cfg_len == 0)
 
                assert(!o_mwb_stb);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(dma_state) != `DMA_IDLE))
 
        begin
 
                assert(cfg_incs == $past(cfg_incs));
 
                assert(cfg_incd == $past(cfg_incd));
 
                assert(cfg_blocklen_sub_one == $past(cfg_blocklen_sub_one));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(dma_state) == `DMA_IDLE))
 
                assert(cfg_len_nonzero == (cfg_len != 0));
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(o_mwb_cyc))||(!$past(o_mwb_we)))
 
                assert((nwritten == 0)&&(nwacks == 0));
 
        always @(posedge i_clk)
 
        if ((o_mwb_cyc)&&(!o_mwb_we))
 
                assert(bus_nracks <= cfg_len);
 
        always @(posedge i_clk)
 
        if ((o_mwb_cyc)&&(!o_mwb_we))
 
                assert(nread <= nracks);
 
        always @(posedge i_clk)
 
        if ((o_mwb_cyc)&&(o_mwb_we))
 
                assert(nwritten-nwacks
 
                        +((o_mwb_stb)? 1'b1:1'b0)
 
                        - f_mwb_outstanding
 
                        // -((i_mwb_ack)? 1'b1:1'b0)
 
                        <= cfg_len);
 
        always @(*)
 
                assert(f_mwb_outstanding
 
                        + ((o_mwb_stb)? 1'b1:1'b0) <= cfg_len);
 
 
 
        wire    [LGMEMLEN:0]     f_cfg_blocklen;
 
        assign  f_cfg_blocklen = { 1'b0, cfg_blocklen_sub_one}  + 1'b1;
 
 
 
        always @(*)
 
        if (dma_state == `DMA_WAIT)
 
                assert(cfg_len > 0);
 
 
 
        always @(*)
 
        if ((o_mwb_stb)&&(o_mwb_we))
 
                assert(nread == nracks);
 
 
 
        always @(*)
 
        if (o_mwb_stb)
 
                assert(nwritten <= cfg_blocklen_sub_one);
 
        always @(posedge i_clk)
 
                assert(nwritten <= f_cfg_blocklen);
 
 
 
        always @(*)
 
        if ((o_mwb_stb)&&(!o_mwb_we))
 
                assert(nracks < f_cfg_blocklen);
 
        else
 
                assert(nracks <= f_cfg_blocklen);
 
        always @(*)
 
        if ((o_mwb_cyc)&&(i_mwb_ack)&&(!o_mwb_we))
 
                assert(nread < f_cfg_blocklen);
 
        always @(*)
 
                assert(nread <= nracks);
 
 
 
        always @(*)
 
        if ((o_mwb_cyc)&&(o_mwb_we)&&(!user_halt))
 
                assert(nread == nracks);
 
 
 
        always @(*)
 
        if ((o_mwb_cyc)&&(o_mwb_we))
 
                assert(nwritten >= nwacks);
 
 
 
        always @(*)
 
        if (dma_state == `DMA_WRITE_REQ)
 
                assert(last_write_request == (nwritten == nread-1));
 
 
 
        always @(*)
 
                assert(nwritten >= nwacks);
 
 
 
        always @(*)
 
                assert(nread >= nwritten);
 
 
 
        always @(*)
 
                assert(nracks >= nread);
 
 
 
        wire    [LGMEMLEN:0]     f_npending;
 
        assign  f_npending = nread-nwacks;
 
        always @(*)
 
        if (dma_state != `DMA_IDLE)
 
                assert({ {(AW-LGMEMLEN-1){1'b0}}, f_npending} <= cfg_len);
 
 
 
        always @(posedge i_clk)
 
        begin
 
                assert(cfg_len_nonzero == (cfg_len != 0));
 
                if ((f_past_valid)&&($past(dma_state != `DMA_IDLE))&&($past(cfg_len == 0)))
 
                        assert(cfg_len == 0);
 
        end
 
 
 
 
 
`endif
 
endmodule
 
 
 No newline at end of file
 No newline at end of file

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.