cache state at reset leads to first 0x2000 addresses returning invalid data

[mattvenn]

I'm working on a formal proof of the qpi cache, and though I'm not finished I've found a potential issue.

The cache doesn't have valid lines, instead, if there is a tag in the tag memory that matches the incoming address, the cache line is assumed valid.

The initial fill for the tag_data memory is all 0s for first way, and all 1s for the second. So (with default settings), the first 0x2000 addresses will return invalid data. (note the found_tag line is high for first 0x2000 addresses).

If the cache is used so that those addresses are always written to at boot, then this wouldn't be a problem, but we should probably put at least a warning in the description at the top of the file.

For the formal proof I am just making the solver choose addresses above 0x2000 to validate, but thought I'd post this for discussion.

[Spritetm]

Actually, this is intended and the data is not invalid on the FPGA itself. In the FPGA implementation, the first half of the data cache contains the boot code, with the cache lines marked as 'valid' so the cache implementation will write it back to the RAM when it needs those cache lines for something else. As I can pre-load the BRAMs on the FPGA without any cost, this effectively is a 'free' way to get me the boot code without having to implement a separate boot ROM.

Perhaps I should have made that more clear, although I'm 100% sure I left a note to this extent somewhere.

[mattvenn]

Ah, ok. I didn't find a note.. The cache gets initialised with this when not run with verilator.

.INITIAL_HEX("rom_random_seeds0x123456.hex")

But I can see in the Makefile

%_out.config: %_out_synth.config rom.hex ecpbram -i $< -o $@ -f rom_random_seeds0x123456.hex -t rom.hex

So maybe a few notes and some renaming would make this more understandable. I can make a pull request if you like. If so, can you try to find the note that describes the behaviour first, in case I missed it.