.. _fifo_source:

fifo Source File
================

.. code-block:: verilog
   :linenos:

   // blockram based FIFO
   // exchangeable with shortfifo.v

   module fifo #(
   	parameter aw = 3,
   	parameter dw = 8
   ) (
   	input clk,

   	input [dw - 1: 0] din,
   	input we,

   	output [dw - 1: 0] dout,
   	input re,

   	output full,
   	output empty,
   	output last,

   	// -1: empty, 0: single element, 2**aw - 1: full
   	output [aw:0] count
   );

   localparam len = 1 << aw;

   reg [dw - 1: 0] mem[len - 1: 0];

   reg [dw - 1: 0] read = 0;
   reg [dw - 1: 0] last_write = 0;

   // read / write pointers (need an extra bit)
   reg [aw: 0] wr_addr = 0;
   reg [aw: 0] rd_addr = 0;

   // Else Vivado would not infer block ram, arrrgh
   wire [aw - 1: 0] wr_addr_ = wr_addr;
   wire [aw - 1: 0] rd_addr_ = rd_addr;
   wire [aw - 1: 0] rd_addr_next_ = rd_addr + 1;

   // Number of items in memory (up to len items)
   // Need 1 extra bit, else wouldn't be able to count len items
   wire [aw: 0] fill = wr_addr - rd_addr;
   assign count = fill - 1;

   // can only read when not empty
   wire re_ = re && !empty;

   // can only write when not full (except when also reading)
   wire we_ = we && (!full || re);

   assign empty = fill == 0;
   assign last = fill == 1;
   assign full = fill >= len;

   // Cannot use block-ram when there is only one element in the FIFO
   // as it has a 2 cycle latency (write and read). We need 1 cycle, so use the
   // bypass register `last_write` in this case instead.
   assign dout = last ? last_write : read;

   always @(posedge clk) begin
   	read <= mem[rd_addr_];

   	if (we_) begin
   		last_write <= din;
   		mem[wr_addr_] <= din;
   		wr_addr <= wr_addr + 1;
   	end

   	if (re_) begin
   		rd_addr <= rd_addr + 1;

   		// we need to look one cycle into the future to compensate the 2 cycle
   		// latency of the Xilinx block-ram
   		read <= mem[rd_addr_next_];
   	end
   end

   // ---------------------------

   `ifdef FORMAL
   // FIFO verification exercise from:
   // https://zipcpu.com/tutorial/lsn-10-fifo.pdf

   reg f_past_valid = 0;

   // 2 magic addresses we will follow up
   (* anyconst *) reg [aw: 0] f_first_addr;
   wire [aw:0] f_second_addr = f_first_addr + 1;

   // address pointers are circular. read_pointer is index0 of FIFO
   // If these are < fill the addresses are valid
   wire [aw: 0] f_first_dist = f_first_addr - rd_addr;
   wire [aw: 0] f_second_dist = f_second_addr - rd_addr;
   wire f_first_valid = !empty && (f_first_dist < fill);
   wire f_second_valid = !empty && (f_second_dist < fill);

   // with 2 corresponding magic values
   (* anyconst *) reg [dw - 1: 0] f_first_data, f_second_data;

   reg [1:0] f_state = 0;

   always @(posedge clk) begin
   	f_past_valid <= 1;

   	// FIFO sequence
   	// Follow up the FIFO state transitions as 2 values enter and leave it
   	// Need to do it for 2 values to verify the correct order
   	case (f_state)
   		0: begin  // IDLE state
   			// write first magic value into FIFO
   			if (we_ && (wr_addr == f_first_addr) && (din == f_first_data))
   				f_state <= 1;
   		end

   		1: begin  // 1 value is in
   			if (re_ && (rd_addr == f_first_addr))
   				f_state <= 0;  // first value was read prematurely, restart
   			else if(we_)
   				if (din == f_second_data)
   					f_state <= 2;  // write second value
   				else
   					f_state <= 0;  // wrote wrong second value, restart

   			// f_first_addr must be in the valid range of the FIFO
   			assert(f_first_valid);
   			assert(mem[f_first_addr] == f_first_data);
   			assert(wr_addr == f_second_addr);
   		end

   		2: begin  // 2 values are in, read out first value
   			if (re_ && (rd_addr == f_first_addr))
   				f_state <= 3;
   			else
   				f_state <= 0;

   			assert(f_first_valid);
   			assert(f_second_valid);
   			assert(mem[f_first_addr] == f_first_data);
   			assert(mem[f_second_addr] == f_second_data);

   			if (rd_addr == f_first_addr)
   				assert(dout == f_first_data);
   		end

   		3: begin  // read out second value
   			f_state <= 0;

   			assert(f_second_valid);
   			assert(mem[f_second_addr] == f_second_data);

   			assert(dout == f_second_data);
   		end
   	endcase

   	// Cannot go from full to empty and vice versa
   	if (f_past_valid && $past(full))
   		assert(!empty);
   	if (f_past_valid && $past(empty))
   		assert(!full);

   	// Read and write can happen at the same time!
   	if (f_past_valid && $past(we) && $past(re) && $past(fill > 0))
   		assert($stable(fill));

   	// cover mode: show 2 values entering and exiting the FIFO:
   	// cover(f_past_valid && $past(f_state) == 3 && f_state == 0);
   end

   // cover mode: Fill up the FIFO and empty it again
   reg f_was_full = 0;
   reg f_both = 0; // show what happens when both are high
   always @(posedge clk) begin
   	// assume(din == $past(din) + 8'h1);
   	if (full)
   		f_was_full <= 1;
   	if (we && re && !empty)
   		f_both <= 1;
   	cover(empty && f_was_full && f_both);
   end


   always @(*) begin
   	assert(fill == wr_addr - rd_addr);
   	assert(empty == (fill == 0));
   	assert(last == (fill == 1));
   	assert(full == (fill == len));

   	// Can't have more items than the memory holds
   	assert(fill <= len);

   	// Cant be full and empty at the same time
   	assert(!(full && empty));
   end
   `endif

   endmodule