generic_fifo_proof.sv

module generic_fifo_proof
	#(parameter WIDTH=8, DEPTH=3, TEST_DATA_LENGTH=7) (
	input wire clock,
	//input wire [WIDTH-1:0] anything,
	input wire             in_valid,
	input wire             out_ack);
	
	(* anyconst *) reg [(WIDTH*TEST_DATA_LENGTH)-1:0] data;
	
	wire [WIDTH-1:0] fifo_in;
	wire             fifo_in_valid;
	wire             fifo_in_ack;
	wire [WIDTH-1:0] fifo_out;
	wire             fifo_out_valid;
	wire             fifo_out_ack;
	
	assign fifo_in_valid = in_valid;
	assign fifo_out_ack = out_ack;
	
	fifo_pointers #(.WIDTH(WIDTH), .DEPTH(DEPTH)) fut (
	    .clock(clock),
	    .in(fifo_in),   .in_valid(fifo_in_valid),   .in_ack(fifo_in_ack),
	    .out(fifo_out), .out_valid(fifo_out_valid), .out_ack(fifo_out_ack)
	);
	
	reg [$clog2(TEST_DATA_LENGTH)-1:0] in_pointer = 0;
	
	assign fifo_in = data[(in_pointer+1)*WIDTH-1:in_pointer*WIDTH];
	
	reg [$clog2(TEST_DATA_LENGTH)-1:0] out_pointer = 0;
	
	wire [WIDTH-1:0] expected_out;
	assign expected_out = data[(out_pointer+1)*WIDTH-1:out_pointer*WIDTH];
	
	wire in_consumes;
	assign in_consumes = in_valid && fifo_in_ack;
	
	wire out_consumes;
	assign out_consumes = out_ack && fifo_out_valid;
	
	wire done;
	assign done = (out_pointer >= (TEST_DATA_LENGTH - 1));
	
	// Count total cycles for timeout.
	reg [15:0] cycles = 0;
	
	// Count cycles without outside input/output to ensure fair conditions for FIFO.
	reg in_pause = 0;
	reg out_pause = 0;

	reg was_full = 0;
	
	always @ (posedge clock) begin
		was_full <= was_full || (!fifo_in_ack && fifo_in_valid);
		// Random but constant data.
		assume ($stable(data));
		
		// Once set, valid input remains stable until read.
		assume ((cycles == 0) || !$past(fifo_in_valid && !fifo_in_ack) || fifo_in_valid);
		
		// Once set, output ack remains stable until read.
		assume ((cycles == 0) || !$past(fifo_out_ack && !fifo_out_valid) || fifo_out_ack);
		
		// Selftest.
		stable_input_data: assert ((cycles == 0) || !$past(fifo_in_valid && !fifo_in_ack) || (fifo_in == $past(fifo_in)));
		
		// Make sure we have at least some reads and writes.
		assume (in_pause < 4);
		assume (out_pause < 8);
		
		// Make sure interesting configurations are possible:
		full_once: cover (!fifo_in_ack); // FIFO may be full.
		transported_all_data: cover (done); // All data may run through FIFO.
		recover_from_full: cover (was_full && in_consumes); // Combination of both.
		finish_after_full: cover (was_full && done && fifo_out_valid); // Combination of both.
		
		if (!done) begin
			cycles <= cycles + 1;
			// Known wrong condition to test toolchain.
			// assert(cycles < 8);
		
			// Our FIFO needs to output after having received input.
			has_any_output_after_input_cycle: assert ((cycles == 0) || !$past(fifo_in_valid) || fifo_out_valid);
			
			// Correct output.
			has_correct_output: assert (!fifo_out_valid || (fifo_out == expected_out));
			
			if (in_valid) begin
				in_pause <= 0;
			end else begin
				in_pause <= in_pause + 1;
			end
			
			if (out_ack) begin
				out_pause <= 0;
			end else begin
				out_pause <= out_pause + 1;
			end
			
			in_pointer <= in_pointer + in_consumes;
			out_pointer <= out_pointer + out_consumes;
		end
	end
endmodule