InferWidths Pass Fails on Solvable Width Constraints with Circular Dependencies.

[wky17]

The current InferWidths pass in firtool(1.109.0) exhibits two critical flaws:

1. Incorrect handling of circular dependencies:

The pass erroneously throws uninferrable exceptions for solvable constraints with circular dependencies, despite the existence of a least solution.
Demonstrative Example:

FIRRTL version 3.0.0
circuit A:
  module A:
    input in : UInt<4>
    input clock : Clock
    output out : UInt
    reg x : UInt, clock
    connect x, add(tail(x,1), in)  // Constraint: wₓ ≥ max(wₓ-1, 4) + 1
    connect out, x

Expected Solution: wₓ = 5
Observed Failure:

error: 'firrtl.reg' op is constrained to be wider than itself
    reg x : UInt, clock
    ^
7:5: note: see current operation: %0 = "firrtl.reg"(%arg1) <{annotations = [], name = "x", nameKind = #firrtl<name_kind droppable_name>}> : (!firrtl.clock) -> !firrtl.uint
8:14: note: constrained width W >= W+1 here:
    x <= add(tail(x,1), in)
             ^
8:7: note: constrained width W >= W+1 here:
    x <= add(tail(x,1), in)
      ^

2. Completeness Deficiencies in Constraint Resolution:

Source code analysis reveals fundamental incompleteness. The implementation fails to identify valid least solutions for constraint systems where such solutions provably exist and even throws unexpected reports.

Demonstrative Example:

FIRRTL version 3.0.0
circuit Foo:
  module Foo:
    input in : UInt<4>
    input clock : Clock
    output out : UInt

    reg x1 : UInt, clock
    wire x2 : UInt
    wire x3 : UInt

    connect x1, mul(mul(x2, in), x2)  // Constraint: wₓ₁ ≥ 2wₓ₂ + 4
    connect x3, shr(x1,2)             // Constraint: wₓ₃ ≥ max(wₓ₁ - 2, 0)
    connect x2, tail(x3,2)            // Constraint: wₓ₂ ≥ wₓ₃ - 2
    connect out, x1

Expected Solution: wₓ₁ = 4, wₓ₂ = 0, wₓ₃ = 2
Observed Failure (seems nonsense):

error: 'firrtl.reg' op is constrained to be wider than itself
    reg x1 : UInt, clock
    ^
...
12:21: note: constrained width W >= 2W+4 here:
    connect x1, mul(mul(x2, in), x2)
                ^
14:17: note: constrained width W >= 2W here:
    connect x2, tail(x3,2)
                ^

The erroneous "constrained to be wider than itself" diagnostic indicates failure to recognize satisfiable constraint chains. This exemplifies the algorithm's inability to systematically explore the solution space.

Request Rationale

We seek commit access to integrate a formally verified alternative implementation that:

1. Resolves circular dependencies through topological sorting and scc decomposion.

2. Guarantees completeness via branch-and-bound solution search.

Our solution has been validated in the Rocq theorem prover (6.9k LOC proof).

[seldridge]

I thought we ported the current FIRRTL InferWidths algorithm directly from the SFC, however, the SFC algorithm works for example (1). The MFC algorithm fails for example (1). Both fail for example (2).

I'm happy for any better algorithms to be used here. I would also be enthusiastic with any changes to the InferWidths pass that are substantially more performant. The current implementation builds up almost an entirely complete shadow IR of constraints. It uses too much memory and is too slow given the fact that most widths are already known.

We seek commit access to integrate a formally verified alternative implementation...

While it is fine to pursue commit access, you don't need it to make a contribution. For that, just a fork and one or more PRs will do. (Also, LLVM upstream is likely going to bounce you without 3 outstanding PRs, per their policy here: https://llvm.org/docs/DeveloperPolicy.html#obtaining-commit-access).

Also, with this, I'll need to do a fair amount of internal testing of any new algorithm, both that it doesn't cause changes in behavior or (more worrying) performance regressions.

Also, please structure this as an "alternative Infer Widths". Any change like this should be done in several steps:

1. Add the alternative pass w/ tests. If this is a pure superset of the old algorithm, then it should reuse the existing tests.
2. An opt-in switch to firtool to use the new pass.
3. A waiting period while testing of the new pass is done.
4. Change the polarity of the switch where the new algorithm is the default, but the old is still available.
5. Delete the old pass, rename the new pass to the old pass.

(You'll see this pattern play out with other thinks like the changes done for FIRRTL's "layer sink" pass.)

All that said, I've very excited for any improvements here! Looking forward to the PRs.