Permalink
Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
840 lines (761 sloc) 23.7 KB
////////////////////////////////////////////////////////////////////////////////
//
// Filename: wbdmac.v
//
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose: Wishbone DMA controller
//
// This module is controllable via the wishbone, and moves values from
// 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.
// Four registers control this DMA controller: a control/status register,
// 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
// to when the controller is idle.
//
// The meanings of three of the setup registers should be self explanatory:
// - The length register controls the total number of words to
// transfer.
// - The source address register controls where the DMA controller
// reads from. This address may or may not be incremented
// after each read, depending upon the setting in the
// control/status register.
// - The destination address register, which controls where the DMA
// controller writes to. This address may or may not be
// incremented after each write, also depending upon the
// setting in the control/status register.
//
// It is the control/status register, at local address zero, that needs
// more definition:
//
// Bits:
// 31 R Write protect If this is set to one, it means the
// write protect bit is set and the controller
// is therefore idle. This bit will be set upon
// completing any transfer.
// 30 R Error. The controller stopped mid-transfer
// after receiving a bus error.
// 29 R/W inc_s_n If set to one, the source address
// will not increment from one read to the next.
// 28 R/W inc_d_n If set to one, the destination address
// will not increment from one write to the next.
// 27 R Always 0
// 26..16 R nread Indicates how many words have been read,
// and not necessarily written (yet). This
// combined with the cfg_len parameter should tell
// exactly where the controller is at mid-transfer.
// 27..16 W WriteProtect When a 12'h3db is written to these
// bits, the write protect bit will be cleared.
//
// 15 R/W on_dev_trigger When set to '1', the controller will
// wait for an external interrupt before starting.
// 14..10 R/W device_id This determines which external interrupt
// will trigger a transfer.
// 9..0 R/W transfer_len How many bytes to transfer at one time.
// The minimum transfer length is one, while zero
// 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:
// 1. Wait for any prior DMA operation to complete
// (Read address 0, wait 'till either top bit is set or cfg_len==0)
// 2. Write values into length, source and destination address.
// (writei(3, &vals) should be sufficient for this.)
// 3. Enable the DMAC interrupt in whatever interrupt controller is present
// on the system.
// 4. Write the final start command to the setup/control/status register:
// Set inc_s_n, inc_d_n, on_dev_trigger, dev_trigger,
// appropriately for your task
// Write 12'h3db to the upper word.
// Set the lower word to either all zeros, or a smaller transfer
// length if desired.
// 5. wait() for the interrupt and the operation to complete.
// Prior to completion, number of items successfully transferred
// be read from the length register. If the internal buffer is
// being used, then you can read how much has been read into that
// buffer by reading from bits 25..16 of this control/status
// register.
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2015-2017, 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
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
`define DMA_IDLE 3'b000
`define DMA_WAIT 3'b001
`define DMA_READ_REQ 3'b010
`define DMA_READ_ACK 3'b011
`define DMA_PRE_WRITE 3'b100
`define DMA_WRITE_REQ 3'b101
`define DMA_WRITE_ACK 3'b110
module wbdmac(i_clk, i_reset,
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_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_dev_ints,
o_interrupt);
parameter ADDRESS_WIDTH=30, LGMEMLEN = 10, DW=32;
localparam LGDV=5;
localparam AW=ADDRESS_WIDTH;
input wire i_clk, i_reset;
// Slave/control wishbone inputs
input wire i_swb_cyc, i_swb_stb, i_swb_we;
input wire [1:0] i_swb_addr;
input wire [(DW-1):0] i_swb_data;
// Slave/control wishbone outputs
output reg o_swb_ack;
output wire o_swb_stall;
output reg [(DW-1):0] o_swb_data;
// Master/DMA wishbone control
output wire o_mwb_cyc, o_mwb_stb, o_mwb_we;
output reg [(AW-1):0] o_mwb_addr;
output reg [(DW-1):0] o_mwb_data;
// Master/DMA wishbone responses from the bus
input wire i_mwb_ack, i_mwb_stall;
input wire [(DW-1):0] i_mwb_data;
input wire i_mwb_err;
// The interrupt device interrupt lines
input wire [(DW-1):0] i_dev_ints;
// An interrupt to be set upon completion
output reg o_interrupt;
// Need to release the bus for a higher priority user
// This logic had lots of problems, so it is being
// removed. If you want to make sure the bus is available
// for a higher priority user, adjust the transfer length
// accordingly.
//
// 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 cfg_err, cfg_len_nonzero;
reg [(AW-1):0] cfg_waddr, cfg_raddr, cfg_len;
reg [(LGMEMLEN-1):0] cfg_blocklen_sub_one;
reg cfg_incs, cfg_incd;
reg [(LGDV-1):0] cfg_dev_trigger;
reg cfg_on_dev_trigger;
// Single block operations: We'll read, then write, up to a single
// memory block here.
reg [(DW-1):0] dma_mem [0:(((1<<LGMEMLEN))-1)];
reg [(LGMEMLEN):0] nread, nwritten, nwacks, nracks;
wire [(AW-1):0] bus_nracks;
assign bus_nracks = { {(AW-LGMEMLEN-1){1'b0}}, nracks };
reg last_read_request, last_read_ack,
last_write_request, last_write_ack;
reg trigger, abort, user_halt;
initial dma_state = `DMA_IDLE;
initial o_interrupt = 1'b0;
initial cfg_blocklen_sub_one = {(LGMEMLEN){1'b1}};
initial cfg_on_dev_trigger = 1'b0;
always @(posedge i_clk)
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
o_mwb_addr <= cfg_raddr;
// When the slave wishbone writes, and we are in this
// (ready) configuration, then allow the DMA to be controlled
// and thus to start.
if ((s_stb)&&(s_we))
begin
case(s_addr)
2'b00: begin
if ((s_data[27:16] == 12'hfed)
&&(s_data[31:30] == 2'b00)
&&(cfg_len_nonzero))
dma_state <= `DMA_WAIT;
cfg_blocklen_sub_one
<= s_data[(LGMEMLEN-1):0]
+ {(LGMEMLEN){1'b1}};
// i.e. -1;
cfg_dev_trigger <= s_data[14:10];
cfg_on_dev_trigger <= s_data[15];
cfg_incs <= !s_data[29];
cfg_incd <= !s_data[28];
end
2'b01: begin end // This is done elsewhere
2'b10: cfg_raddr <= s_data[(AW+2-1):2];
2'b11: cfg_waddr <= s_data[(AW+2-1):2];
endcase
end end
`DMA_WAIT: begin
o_mwb_addr <= cfg_raddr;
if (abort)
dma_state <= `DMA_IDLE;
else if (user_halt)
dma_state <= `DMA_IDLE;
else if (trigger)
dma_state <= `DMA_READ_REQ;
end
`DMA_READ_REQ: begin
if (!i_mwb_stall)
begin
// Number of read acknowledgements needed
if ((last_read_request)||(user_halt))
//((nracks == {1'b0, cfg_blocklen_sub_one})||(bus_nracks == cfg_len-1))
// Wishbone interruptus
dma_state <= `DMA_READ_ACK;
if (cfg_incs)
o_mwb_addr <= o_mwb_addr
+ {{(AW-1){1'b0}},1'b1};
end
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
else if (i_mwb_ack)
begin
if (cfg_incs)
cfg_raddr <= cfg_raddr
+ {{(AW-1){1'b0}},1'b1};
if (last_read_ack)
dma_state <= `DMA_PRE_WRITE;
end end
`DMA_READ_ACK: begin
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
else if (i_mwb_ack)
begin
if (last_read_ack) // (nread+1 == nracks)
dma_state <= `DMA_PRE_WRITE;
if (user_halt)
dma_state <= `DMA_IDLE;
if (cfg_incs)
cfg_raddr <= cfg_raddr
+ {{(AW-1){1'b0}},1'b1};
end
end
`DMA_PRE_WRITE: begin
o_mwb_addr <= cfg_waddr;
dma_state <= (abort)?`DMA_IDLE:`DMA_WRITE_REQ;
end
`DMA_WRITE_REQ: begin
if (!i_mwb_stall)
begin
if (last_write_request) // (nwritten == nread-1)
// Wishbone interruptus
dma_state <= `DMA_WRITE_ACK;
if (cfg_incd)
begin
o_mwb_addr <= o_mwb_addr
+ {{(AW-1){1'b0}},1'b1};
cfg_waddr <= cfg_waddr
+ {{(AW-1){1'b0}},1'b1};
end
end
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
else if ((i_mwb_ack)&&(last_write_ack))
dma_state <= (cfg_len <= 1)?`DMA_IDLE:`DMA_WAIT;
else if (!cfg_len_nonzero)
dma_state <= `DMA_IDLE;
end
`DMA_WRITE_ACK: begin
if ((i_mwb_err)||(abort))
dma_state <= `DMA_IDLE;
else if ((i_mwb_ack)&&(last_write_ack))
// (nwacks+1 == nwritten)
dma_state <= (cfg_len <= 1)?`DMA_IDLE:`DMA_WAIT;
else if (!cfg_len_nonzero)
dma_state <= `DMA_IDLE;
end
default:
dma_state <= `DMA_IDLE;
endcase
initial o_interrupt = 1'b0;
always @(posedge i_clk)
if (i_reset)
o_interrupt <= 1'b0;
else
o_interrupt <= ((dma_state == `DMA_WRITE_ACK)&&(i_mwb_ack)
&&(last_write_ack)
&&(cfg_len == {{(AW-1){1'b0}},1'b1}))
||((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;
always @(posedge i_clk)
if (i_reset)
cfg_err <= 1'b0;
else if (dma_state == `DMA_IDLE)
begin
if ((s_stb)&&(s_we)&&(s_addr==2'b00))
cfg_err <= 1'b0;
end else if (((i_mwb_err)&&(o_mwb_cyc))||(abort))
cfg_err <= 1'b1;
initial last_read_request = 1'b0;
always @(posedge i_clk)
if (i_reset)
last_read_request <= 1'b0;
else if ((dma_state == `DMA_WAIT)||(dma_state == `DMA_READ_REQ))
begin
if ((!i_mwb_stall)&&(dma_state == `DMA_READ_REQ))
begin
last_read_request <=
(nracks + 1 == { 1'b0, cfg_blocklen_sub_one})
||(bus_nracks == cfg_len-2);
end else
last_read_request <=
(nracks== { 1'b0, cfg_blocklen_sub_one})
||(bus_nracks == cfg_len-1);
end else
last_read_request <= 1'b0;
wire [(LGMEMLEN):0] next_nread;
assign next_nread = nread + 1'b1;
initial last_read_ack = 1'b0;
always @(posedge i_clk)
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
if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
last_read_ack <= (nread+2 == nracks);
else
last_read_ack <= (next_nread == nracks);
end else
last_read_ack <= 1'b0;
initial last_write_request = 1'b0;
always @(posedge i_clk)
if (i_reset)
last_write_request <= 1'b0;
else if (dma_state == `DMA_PRE_WRITE)
last_write_request <= (nread <= 1);
else if (dma_state == `DMA_WRITE_REQ)
begin
if (i_mwb_stall)
last_write_request <= (nwritten >= nread-1);
else
last_write_request <= (nwritten >= nread-2);
end else
last_write_request <= 1'b0;
initial last_write_ack = 1'b0;
always @(posedge i_clk)
if (i_reset)
last_write_ack <= 1'b0;
else if((dma_state == `DMA_WRITE_REQ)||(dma_state == `DMA_WRITE_ACK))
begin
if ((i_mwb_ack)&&((!o_mwb_stb)||(i_mwb_stall)))
last_write_ack <= (nwacks+2 == nwritten);
else
last_write_ack <= (nwacks+1 == nwritten);
end else
last_write_ack <= 1'b0;
assign o_mwb_cyc = (dma_state == `DMA_READ_REQ)
||(dma_state == `DMA_READ_ACK)
||(dma_state == `DMA_WRITE_REQ)
||(dma_state == `DMA_WRITE_ACK);
assign o_mwb_stb = (dma_state == `DMA_READ_REQ)
||(dma_state == `DMA_WRITE_REQ);
assign o_mwb_we = (dma_state == `DMA_PRE_WRITE)
||(dma_state == `DMA_WRITE_REQ)
||(dma_state == `DMA_WRITE_ACK);
//
// 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
// the read_address (rdaddr) register. The problem is that this
// register must always be one greater than the address we actually
// want to read from, unless we are idling. So ... the math is touchy.
//
reg [(LGMEMLEN-1):0] rdaddr;
initial rdaddr = 0;
always @(posedge i_clk)
if (i_reset)
rdaddr <= 0;
else if((dma_state == `DMA_IDLE)||(dma_state == `DMA_WAIT)
||(dma_state == `DMA_WRITE_ACK))
rdaddr <= 0;
else if ((dma_state == `DMA_PRE_WRITE)
||((dma_state==`DMA_WRITE_REQ)&&(!i_mwb_stall)))
rdaddr <= rdaddr + {{(LGMEMLEN-1){1'b0}},1'b1};
always @(posedge i_clk)
if (i_reset)
o_mwb_data <= 0;
else if ((dma_state != `DMA_WRITE_REQ)||(!i_mwb_stall))
o_mwb_data <= dma_mem[rdaddr];
always @(posedge i_clk)
if((dma_state == `DMA_READ_REQ)||(dma_state == `DMA_READ_ACK))
dma_mem[nread[(LGMEMLEN-1):0]] <= i_mwb_data;
always @(posedge i_clk)
if (i_reset)
o_swb_data <= 0;
else casez(s_addr)
2'b00: o_swb_data <= { (dma_state != `DMA_IDLE), cfg_err,
!cfg_incs, !cfg_incd,
1'b0, nread,
cfg_on_dev_trigger, cfg_dev_trigger,
cfg_blocklen_sub_one
};
2'b01: o_swb_data <= { {(DW-AW){1'b0}}, cfg_len };
2'b10: o_swb_data <= { {(DW-2-AW){1'b0}}, cfg_raddr, 2'b00 };
2'b11: o_swb_data <= { {(DW-2-AW){1'b0}}, cfg_waddr, 2'b00 };
endcase
// 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
// develop the trigger.
initial trigger = 1'b0;
always @(posedge i_clk)
if (i_reset)
trigger <= 1'b0;
else
trigger <= (dma_state == `DMA_WAIT)
&&((!cfg_on_dev_trigger)
||(i_dev_ints[cfg_dev_trigger]));
// 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,
// double check that it isn't busy, and then write.
initial o_swb_ack = 1'b0;
always @(posedge i_clk)
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;
initial abort = 1'b0;
always @(posedge i_clk)
if (i_reset)
abort <= 1'b0;
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;
always @(posedge i_clk)
user_halt <= ((user_halt)&&(dma_state != `DMA_IDLE))
||((s_stb)&&(s_we)&&(dma_state != `DMA_IDLE)
&&(s_addr == 2'b00)
&&(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 [0:0] F_OPT_CLK2FFLOGIC = 1'b0;
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),
.F_OPT_CLK2FFLOGIC(F_OPT_CLK2FFLOGIC)
) 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_CLK2FFLOGIC(F_OPT_CLK2FFLOGIC),
.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);
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