Request Commit Access For wky17

[wky17]

Why Are you requesting commit access ?

InferWidths Pass Fails on Solvable Width Constraints with Circular Dependencies.

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).

[github-actions]

@wky17 thank you for applying for commit access. Please review the project's code review policy.

[github-actions]

Activity Summary:

• 0 Pull Requests
• 0 Merged Pull Requests
• Top 3 Committers:
• Top 3 Reviewers:

[llvmbot]

@llvm/issue-subscribers-infra-commit-access-request

Author: None (wky17)

### Why Are you requesting commit access ?

InferWidths Pass Fails on Solvable Width Constraints with Circular Dependencies.

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).