ROM model not friendly for SymbiYosys K-Induction mode

[georgerennie]

Steps to reproduce the issue

I've noticed that recently a simple testbench I wrote to check a combinational circuit using SymbiYosys' prove mode has started to observe a failing inductive case. While this isnt super relevant for a purely combinational circuit (as there should be no sequential element so prove is unecessary), I think it is worth raising as an issue as this could affect similar cases. Below is a minimal SymbiYosys test case that exhibits the same behaviour.

[options]
mode prove
depth 1

[engines]
smtbmc

[script]
read_verilog -formal <<EOT
module top(
	input [3:0] in,
	output [7:0] out
);

always @* begin
	case (in)
		4'd0: out = 8'd0;
		4'd1: out = 8'd0;
		4'd2: out = 8'd0;
		4'd3: out = 8'd0;
		4'd4: out = 8'd0;
		4'd5: out = 8'd0;
		4'd6: out = 8'd0;
		4'd7: out = 8'd0;
		default: out = 'x;
	endcase
end

always @*
	if (in == 4'd0) assert(out == 8'd0);

endmodule
EOT

prep -top top

Expected behavior

As this is a basic combinational equivalence, I expect both the basecase and inductive case to prove easily for a depth of 1.

Actual behavior

The basecase proves easily, but the inductive case does not prove for any depth. This seems to be because out is being detected as a ROM (by proc_rom) in recent versions of Yosys, and thus being substituted for a $mem_v2 ROM cell. This seems to be inplemented by backends with a pattern like the following (this is adapted from write_verilog output but it seems write_smt2 is doing something similar).

	reg [7:0] _06_ [7:0];
	initial begin
		_06_[0] = 8'h00;
		_06_[1] = 8'h00;
		_06_[2] = 8'h00;
		_06_[3] = 8'h00;
		_06_[4] = 8'h00;
		_06_[5] = 8'h00;
		_06_[6] = 8'h00;
		_06_[7] = 8'h00;
	end
	assign _02_ = _06_[in[2:0]];

This is modelling a ROM inductively, by declaring its values in the initial state, and then by reg semantics the values in each new clock cycle are equal to those in the previous.

The inductive case in sby does not use the initial conditions, as it is considering traces from an arbitrary starting point that lead to a property violation. Thus using the above model, ROM values are left unconstrained for the inductive case which makes it hard for the inductive case to prove (k-induction needs a K sufficient to exclude all traces of valid states leading to a bad state).

Potential Solution

A potential solution is to replace the ROM model at least for formal focused backends (like write_smt2) with a continuous assignment model (like the original verilog code), so the values of the ROM values are clear on every timestep and present in the transition relation as well as the initial conditions. There is also an argument that could be made that the current implementation is fine as it reduces the number of clauses fed to the smt solver, particularly for a large ROM.

I've submitted this as an issue rather than a PR changing this as it is my understanding that a lot of this memory inference code is quite new and thus subject to change/improvements etc.

An aside about completeness

Not entirely relevant for the above, but in smtbmc's current implementation of K-Induction (at least as far as I am aware, I may be wrong) there is no K sufficiently large to prove the inductive case for the above example, because it does not implement a complete (in the logic sense) proof algorithm. This is because it cannot determine when it has checked all possible induction traces, as it admits infinite length induction traces. This can be remedied by applying a simple path/loop free constraint to the induction trace, as described in https://www.di.ens.fr/~pouzet/cours/mpri/bib/sheeran-FMCAD00.pdf to determine the required K. If this were done it would have been able to prove the above example correct, even with the inductive ROM model, although inefficiently.

[jix]

Thank you for this detailed bug report, I agree that this could be very relevant and quite hard to debug performance issue for some designs.

Regarding potential solutions, I can think of a few approaches:

• Work around this issue using existing passes
  • Prepend proc -norom to avoid inferring ROMs for this in the first place. Simplest workaround that should revert exactly to the previous behavior but requires changing the script in the sby file, so not really an overall solution.
  • Map ROMs to logic at the end of the script using memory_map r:WR_PORTS=0. This could also be added to the sby internal scripts or as a preparation step of write_smt2 and write_btor (like bmuxmap and demuxmap currently are). Depending on how much work the other alternatives are, this might be at least a good temporary fix.
    • This still generates FFs, which in principle have the same problem, but the optimization passes used for sbys formal flow are sufficient to remove them.
    • For calling it from within write_smt2, write_btor this would require changing memory_map to omit the FFs for a ROM.
    • Adding a memory_map -rom option instead of having to use a selection might be a nice UI improvement.
    • Already addressed in memory_map: Use const drivers instead of FFs for ROMs. #3380 and memory_map: Add -rom-only option. #3381
• Handle ROMs in write_smt2 and write_btor
  • Might be a good opportunity to also avoid bmuxmap and demuxmap in those passes if that can share code
  • There are multiple possible encodings, but my guess would be that for ROMs it does not make a big difference most of the time. Still some benchmarking of alternatives is a good idea.

Regarding simple path constraints, I don't think they are particularly useful as a workaround for this specific problem. In general, however, looking into simple path constraints for sby/smtbmc is already on my TODO list. Also, the btormc solver already does support K-induction with simple path constraints. Currently sby only has BMC support for btormc, though, but adding a btormc prove mode is already planned.

[mwkmwkmwk]

* This still generates FFs, which in principle have the same problem, but the optimization passes used for sbys formal flow are sufficient to remove them.

FYI, fixing this annoyance is on my TODO list

[georgerennie]

Thanks for sorting this so quickly. It's probably no great suprise that this affects a few other places as well, and I just noticed that it's causing similar cases to fail for equiv_induct/equiv_simple. I imagine they can be remedied in the same way but I can also add a manual call to memory_map -rom-only for now.

[jix]

This approach sadly does not work well in cases where the ROM content is not fully defined and breaks existing formal tests in worse ways than regressing provability. Therefore I'm going to revert the change that automatically calls this from write_smt2 and write_btor.

Trying to make it work better also uncovered some other issues in the formal flow that need to be resolved for this. I'm currently working on that. Even then, memory_map -rom-only -keepdc has to be called early, before async2sync or clk2fflogic.

There are also some use cases with large, completely uninitialized ROMs where memory_map -rom-only -keepdc may not be desirable from a performance perspective. Until I've done more testing and have a way that is robust enough to be enabled unconditionally, calling memory_map -rom-only -keepdc will have to be done manually.