Double indirection not supported for memories?

[whitequark]

I am writing a formal specification for a CPU instruction that performs double indirection. I.e. it does reg = mem[mem[op]];

I am trying to write an assertion like this:

assert (fi_w_data == mem[mem[a_regY] + i_imm5]);

This fails, indicating a logic loop. I have worked around this by rewriting it as:

assert (fi_w_data == mem[$past(mem[a_regY]) + i_imm5]);

As I understand, this effectively adds a register, but without the need to explicitly declare variables, expand processes, etc. So this register breaks the logic loop.

As I also understand, the only case where the mem[mem[r]] construct would be absolutely necessary is if you had a dual read port asynchronous memory where the data of the first port is chained to the address of the second port. In all other cases, there is at least one cycle between reads, and so the $past trick will work (although it might get messy with intervening writes..?).

Can you please explain the nature of this limitation? Is this a real logic loop according to Verilog semantics or is this an artifact of the way Yosys lowers Verilog features? Is my workaround 'correct'?

What would I have to do if I had the dual read port asynchronous memory as described above and wanted to verify it? Yes, probably not a very good idea, but I think it is synthesizable with LUTRAM and enough duplication, so this can in principle be encountered in a real world design.

[daveshah1]

I understand this is due to the nature of the $mem cell, it appears as a logic loop - feedback from the output of the $mem to an input - at the word level, even though no loop exists at the bit level. This is vaguely similar to https://stackoverflow.com/questions/44828776/yosys-logic-loop-falsely-detected.

Running the memory command to explode the RAM to registers and logic removes the logic loop error, but will increase the cost of verification for larger designs.

[daveshah1]

It would seem like a possible solution would be splitting the single $mem cell with two read ports to two $mem cells each with one read port. But I don't think this exists as a Yosys command at the moment.

[whitequark]

Ah, I understand the solution now. I can probably implement such a command.