| Issue |
163906
|
| Summary |
Request Commit Access For wky17
|
| Labels |
infra:commit-access-request
|
| Assignees |
|
| Reporter |
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
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**:
```Terminal
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
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).
![]()
_______________________________________________
llvm-bugs mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-bugs
