The assertion above will fail.

This is not the way to describe a write through block RAM.

Frankly, I’m not sure I’ve seen a good way to describe a write through block RAM. I’ve seen several. For example, one might write:

always @(posedge i_clk)
begin
	o_data <= mem[i_addr];
	if (i_write)
		mem[i_addr] <= i_data;
end

This, of course, fails because o_data is set before mem ever gets updated.

You might also write,

always @(posedge i_clk)
begin
	if (i_write)
		mem[i_addr] <= i_data;
	o_data <= mem[i_addr];
end

While this looks closer to what you want, it also fails for the same reason: The assignment to mem[i_addr] is deferred until the clock edge, and so o_data is set to what used to be in the memory–not what is going into the memory.

The obvious alternative to this problem would be to use blocking assignments, and instead write,

always @(posedge i_clk)
begin
	if (i_write)
		mem[i_addr] = i_data;
	o_data = mem[i_addr];	// This could also be non-blocking
end

But now you’ll have a race condition within your design regarding when you actually evaluate this logic. Specifically, any processes reading o_data may (or may not) read the value from before the memory was updated.

Sure, you could make o_data non-blocking, o_data <= mem[i_addr], but now you have a race condition on mem[i_addr].

The solution I’ve come across isn’t great, but it appears to work. That is to register the incoming data, and to combinatorially select from between the registered incoming and the read outgoing data.

always @(posedge i_clk)
begin
	if (i_write)
		mem[i_addr] <= i_data;
	rd_data <= mem[i_addr];

	write_flag <= i_write;
	wr_data    <= i_data;
end

assign	o_data = (write_flag) ? wr_data : rd_data;

While this works, it doesn’t necessarily use any special write–through RAM hardware that the chip might have. The fact that this design will work in both simulation and in hardware, however, makes the difference worthwhile.

I’ve also added a variant of this technique to my synchronous FIFO implementation, allowing the FIFO to be written and then read on the same cycle. Hence, you can now successfully read and write from an empty FIFO, as well as writing to and reading from a full FIFO.