check: Skip detailed edge modeling if costly

[povik]

What are the reasons/motivation for this change?

On real world designs like the Black Parrot, check can get stuck on some cells because of the edge data explosion. See e.g. this shift cell

attribute \src "../black-parrot/external/HardFloat/source/HardFloat_primitives.v:103.10-103.17"
  cell $shr $auto$slang_frontend.cc:657:operator()$20570
    parameter \Y_WIDTH 4097
    parameter \B_WIDTH 12
    parameter \B_SIGNED 0
    parameter \A_WIDTH 4097
    parameter \A_SIGNED 1
    connect \Y $auto$slang_frontend.cc:665:operator()$20571
    connect \B $auto$slang_frontend.cc:604:operator()$20569
    connect \A 4097'10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
  end

Explain how this is achieved.

For those cells for which the edge data is available and can exhibit a quadratic explosion, we check for the product of the input and output port widths, and if the product is over a threshold, we fall back to coarse connectivity modeling (we assume all output port bits are connected to all input port bits, like we do for cells for which the edge data is unavailable today).

At the same time, we introduce a new option to force the detailed modeling:

    -force-detailed-loop-check
        for the detection of combinatorial loops, use a detailed connectivity
        model for all internal cells for which it is available. This disables
        falling back to a simpler overapproximating model for those cells for
        which the detailed model is expected costly.

If applicable, please suggest to reviewers how they can test the change.

See this session on this somewhat synthetic example:

module top(input wire [15:0] i, output wire [31:0] y);
	assign y = {16'hbf39, ~y[31:15]} >> i; 
endmodule

yosys> read_verilog loop.v
...
yosys> check

2. Executing CHECK pass (checking for obvious problems).
Checking module top...
Warning: found logic loop in module top:
    cell $shr$loop.v:2$2 ($shr) source: loop.v:2.13-2.39
      (cell's internal connectivity overapproximated; loop may be a false positive)
    cell $not$loop.v:2$1 ($not) source: loop.v:2.24-2.33
      A[0] --> Y[0]
Warning: found logic loop in module top:
    cell $shr$loop.v:2$2 ($shr) source: loop.v:2.13-2.39
      (cell's internal connectivity overapproximated; loop may be a false positive)
    cell $not$loop.v:2$1 ($not) source: loop.v:2.24-2.33
      A[1] --> Y[1]

...

Warning: found logic loop in module top:
    cell $shr$loop.v:2$2 ($shr) source: loop.v:2.13-2.39
      (cell's internal connectivity overapproximated; loop may be a false positive)
    cell $not$loop.v:2$1 ($not) source: loop.v:2.24-2.33
      A[16] --> Y[16]
Found and reported 17 problems.
Consider re-running with '-force-detailed-loop-check' to rule out false positives.

yosys> check -force-detailed-loop-check

3. Executing CHECK pass (checking for obvious problems).
Checking module top...
Found and reported 0 problems.

[rowanG077]

I would like an option that will automatically fall back to detailed loop checking when a course loop is found. I expect that a loop is mostly isolated to a relatively tiny subset of the netlist so detailed checking should be cheap.

This will also make sure this optimization has the same external behaviour as before. As it stands designs which yosys now reports as fine will be wrongly flagged as having logic loops with this PR as it is.

Sorry for this drive by comment 😅. If this is infeasible or just a lot of work ignore me.

[povik]

I expect that a loop is mostly isolated to a relatively tiny subset of the netlist so detailed checking should be cheap.

Where the new behavior matters the most is in cases where a single cell can explode to a prohibitive number of edges (like in the Black Parrot). In such cases it's a bit misleading to suggest -force-detailed-loop-check as it will get stuck, so we may want to adjust the wording or remove the suggestion.

As it stands designs which yosys now reports as fine will be wrongly flagged as having logic loops with this PR as it is.

We could adjust the threshold to make sure the change doesn't affect realistic designs which were checkable before. So that the only designs affected are those on which check was stuck or close-to-stuck before.

Sorry for this drive by comment 😅. If this is infeasible or just a lot of work ignore me.

Not at all. It's not infeasible though I am a bit worried about the code complexity for a little gain.