[FIRRTL] Add alternative constraint-based InferWidths pass #9173

wky17 · 2025-11-03T04:47:41Z

[WIP][FIRRTL] Add formally verified alternative InferWidths pass

🔍 Related Issue

Fixes #9140 (InferWidths failures on cyclic constraints)

📖 Background & Motivation

The current InferWidths implementation has critical limitations:
Correctness gaps: Fails on cyclic constraint cases like issue9140_0.mlir and issue9140_1.mlir

This PR introduces InferWidths_new - a drop-in alternative pass that:

Solves the correctness issues in InferWidths Pass Fails on Solvable Width Constraints with Circular Dependencies. #9140
Comes with formal verification guarantees

⚙️ Technical Approach

The new pass implements a constraint-based width inference engine with:

Graph propagation core: Using Boost's graph algorithms for: SCC decomposition (Tarjan)
Adapted Floyd-Warshall algorithm and **Adapted Branch-and-Bound algorithm **: Solving inside SCC
Formal verification: Core algorithm mechanically proven in Rocq
Incremental adoption: Preserves existing pass pipeline

Implementation note:
Boost is used for rapid prototyping of graph algorithms. We have prepped replacement stubs for:

Tarjan's algorithm (SCC decomposition)

Floyd-Warshall (computing the least path)

DFS (finding any existing path between two nodes)
These can be swapped in if necessary

🧪 Testing Strategy

Comprehensive verification across 2 test dimensions:

Test Category	Coverage	Verified Method
Legacy compliance	100% existing tests (`test/Dialect/FIRRTL/infer-widths.mlir`)	✅ Passes all 60 existing tests
Issue regression	`test_new_inferwidths/` • issue9140_0.mlir (example 1) • issue9140_1.mlir (example 2)	🐛 Fixes #9140 failures

🚀 Integration Plan

Following maintainer's phased adoption strategy:

[Current PR] Add alternative pass with firrtl-infer-widths-new opt-in
[Next] Enable in downstream CI with shadow testing
[Phase 3] Performance benchmarking (memory/runtime)
[Future] Switch default after bake period

darthscsi · 2025-11-06T17:25:00Z

test_new_inferwidths/issue9140_0.mlir

Please collect all the tests to a single file and put them in the appropriate tests folder with the normal LIT headers and directives and checks.

darthscsi · 2025-11-06T17:26:04Z

lib/Firtool/Firtool.cpp


  // Width inference creates canonicalization opportunities.
-  pm.nest<firrtl::CircuitOp>().addPass(firrtl::createInferWidths());
+  //pm.nest<firrtl::CircuitOp>().addPass(firrtl::createInferWidths());


Please either add a cmdline control over this or remove the old line. Don't leave commented out code in the file.

darthscsi · 2025-11-06T17:26:49Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+  auto cs_duration = std::chrono::duration_cast<std::chrono::microseconds>(cs_time - start);
+  auto solve_duration = std::chrono::duration_cast<std::chrono::microseconds>(update_time - solve_time);
+  auto update_duration = std::chrono::duration_cast<std::chrono::microseconds>(end - update_time);
+  // std::cout << "generate constraint time : " << cs_duration.count() / 1000.0 << " ms\n";


Please don't commit commented out code. I might suggest adding some performance counters from MLIR to track and report these.

darthscsi · 2025-11-06T17:27:23Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+  if (mapping.areAllModulesSkipped())
+    return markAllAnalysesPreserved();
+
+  auto solve_time = std::chrono::high_resolution_clock::now();


See if MLIR's timing mechanisms are sufficient.

darthscsi · 2025-11-06T17:28:45Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+
+    // 输出结果
+    if (solution.has_value()) {
+        // LLVM_DEBUG(llvm::dbgs() << "可行解找到:\n";


Please don't commit commented out code. It looks like the LLVM_DEBUG guard is sufficient to have the code in.

darthscsi · 2025-11-06T17:30:20Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+// bab
+//===----------------------------------------------------------------------===//
+
+using Bounds = std::unordered_map<FieldRef, std::pair<int, int>, FieldRef::Hash>;


I haven't checked, but unordered_map is a red flag for deterministic behavior. The code might be fine, but it needs to be carefully checked.

darthscsi · 2025-11-06T17:33:04Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+    return success();
+
+  bool mappingFailed = false;
+  TypeSwitch<Operation *>(op)


Consider using an OpVisitor.

darthscsi · 2025-11-06T17:42:21Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+#include "llvm/ADT/SetVector.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/ErrorHandling.h"
+#include <boost/graph/adjacency_list.hpp>


LLVM has a dim view of adding external dependencies. These would have to be very carefully considered.

darthscsi · 2025-11-06T17:42:55Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+#include "llvm/Support/ErrorHandling.h"
+#include <boost/graph/adjacency_list.hpp>
+#include <boost/graph/floyd_warshall_shortest.hpp>
+#include <boost/graph/strong_components.hpp>


There is a SCC implementation in MLIR which should likely be used.

darthscsi · 2025-11-06T17:43:29Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+#include <boost/graph/floyd_warshall_shortest.hpp>
+#include <boost/graph/strong_components.hpp>
+#include <iostream>
+#include <iomanip>


Please use MLIR/LLVM streams rather than the standard library.

darthscsi · 2025-11-06T17:45:19Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+//===----------------------------------------------------------------------===//
+
+// 节点类型
+using Node = std::variant<Zero, FieldRef>;


consider using a sentinel FieldRef. I think one already exists (value null).

wky17 · 2025-11-24T06:09:52Z

PR Update Summary

Hi maintainers, I've comprehensively updated this PR to address all previous feedback:

Formatting & Structure
- Fixed all clang-format issues
- Rebased onto latest upstream
- Added proper timing via MLIR's timing mechanisms
Implementation Improvements
- Added new -use-new-infer-widths option in firtool (instead of commenting-out)
- Replaced unordered_map with DenseMap for deterministic behavior and better performance
- Removed Boost dependency by using GraphTraits from LLVM
- Utilized MLIR/LLVM streams instead of standard library iostreams
Semantic Refinements
- Used LLVM_DEBUG for diagnostic output
- Used sentinel FieldRef instead of custom Zero variable
- Added width constraint: w_c <= 1 for condition handling

@llvm/circt-maintainers @seldridge @darthscsi Could you please re-run CI and review when convenient?

wky17 · 2025-12-11T03:04:20Z

@schulyer Hi! I have resolved the conflict in Firtool.cpp, please re-run again!

wky17 · 2025-12-11T03:12:52Z

@seldridge @darthscsi Hi! I have resolved the conflict in Firtool.cpp, please re-run again!

wky17 · 2025-12-11T13:33:28Z

@seldridge Hi! I have resolved the build error. I think the reason for the error is that my local environment is different from the Docker test environment. Please re-run again!

wky17 · 2025-12-12T06:55:40Z

@seldridge @darthscsi Dear reviewers,
All CI checks have passed after the recent fixes. Could you please review this PR when you have time?
Thank you for your time and consideration!

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

uenoku · 2025-11-05T10:43:00Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+    } 
+};
+
+#include <list>


nit: Please include header at the top of file

uenoku · 2025-12-15T07:54:57Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+  std::deque<Node> nodes;
+  DenseMap<FieldRef, Node *> nodeMap;
+


Isn't nodes reallocated when deque size is modified? If so I think nodeMap could refer to invalided node addresses. Certainly using bump allocator or unique_ptr is better here.

uenoku · 2025-12-15T07:57:31Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+  LLVM_DEBUG(llvm::dbgs() << "initial matrix:\n");
+  for (int i = 0; i < n; i++) {
+    for (int j = 0; j < n; j++) {
+      if (graph[i][j] == INF)
+        LLVM_DEBUG(llvm::dbgs() << "  INF  ");
+      else
+        LLVM_DEBUG(llvm::dbgs() << "  " << graph[i][j] << "  ");
+    }
+    LLVM_DEBUG(llvm::dbgs() << "\n");
+  }


nit: you can put entire for loops under LLVM_DEBUG

Suggested change

LLVM_DEBUG(llvm::dbgs() << "initial matrix:\n");

for (int i = 0; i < n; i++) {

for (int j = 0; j < n; j++) {

if (graph[i][j] == INF)

LLVM_DEBUG(llvm::dbgs() << " INF ");

else

LLVM_DEBUG(llvm::dbgs() << " " << graph[i][j] << " ");

}

LLVM_DEBUG(llvm::dbgs() << "\n");

}

LLVM_DEBUG({

lvm::dbgs() << "initial matrix:\n";

for (int i = 0; i < n; i++) {

for (int j = 0; j < n; j++) {

if (graph[i][j] == INF)

llvm::dbgs() << " INF ";

else

llvm::dbgs() << " " << graph[i][j] << " ";

}

llvm::dbgs() << "\n";

}

});

uenoku · 2025-12-15T08:08:22Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+//===- InferWidths_new.cpp - Infer width of types -------------------*- C++
+//-*-===//


Suggested change

//===- InferWidths_new.cpp - Infer width of types -------------------*- C++

//-*-===//

//===----------------------------------------------------------------------===//

uenoku · 2025-12-15T08:11:43Z

Could you add

circt-opt --pass-pipeline='builtin.module(firrtl.circuit(firrtl-infer-widths-new))' --verify-diagnostics %s | FileCheck %s

to

circt/test/Dialect/FIRRTL/infer-widths.mlir

Line 1 in 1e18df3

    
           // RUN: circt-opt --pass-pipeline='builtin.module(firrtl.circuit(firrtl-infer-widths))' --verify-diagnostics %s | FileCheck %s

and see if it passes?

uenoku · 2025-12-15T08:48:07Z

lib/Dialect/FIRRTL/Transforms/InferWidths_new.cpp

+  }
+};
+
+class Constraint1 {


Do you mind if you could add comments for Constraint1/2/Min? At the moment I need to guess from output "&operator<<(" ...

This commit introduces `InferWidths_new` as an alternative implementation to the existing `InferWidths` pass. The new pass utilizes a constraint-based approach [based on graph propagation and is formally verified in Rocq] which aims to: - Correctly handle cases like test_new_inferwidths/issue9140_0.mlir and test_new_inferwidths/issue9140_1.mlir where the current MFC implementation fails (issue llvm#9140). - Provide an option for the new inferwidths pass to benefit from the potential of formal verification. Key changes: 1. Added `InferWidths_new.cpp` implementing the core algorithm. 2. Added comprehensive tests in `test_new_inferwidths/…` covering: - All existing InferWidths test cases (from test/Dialect/FIRRTL/infer-widths.mlir). - Specific cases like example (1) and example (2) in llvm#9140. 3. Added a new command-line option `-infer-widths-new` to `circt-opt` to enable the new pass. 4. Updated CMake build files to include the new source. This is the first step (adding the alternative pass) as suggested by maintainers. It's worth noting that the current graph propagation algorithm utilizes the Boost library for rapid implementation. If needed in the future, the Boost dependency can be optimized away by implementing our own Tarjan's algorithm and Floyd-Warshall algorithm. Related to llvm#9140.

…s-new.mlir in /test/Dialect/FIRRTL

…ith same name as circuit

…t the top of file

wky17 requested review from darthscsi and seldridge as code owners November 3, 2025 04:47

darthscsi reviewed Nov 6, 2025

View reviewed changes

wky17 force-pushed the issue-9140-new-inferwidths branch from c9aaa58 to 2f3745a Compare November 24, 2025 03:04

wky17 requested a review from darthscsi November 24, 2025 05:46

wky17 force-pushed the issue-9140-new-inferwidths branch 4 times, most recently from 3c15856 to 221639e Compare December 8, 2025 02:04

wky17 force-pushed the issue-9140-new-inferwidths branch 2 times, most recently from 1fe9115 to b837c49 Compare December 11, 2025 03:03

wky17 force-pushed the issue-9140-new-inferwidths branch from b837c49 to 0f16622 Compare December 11, 2025 09:55

wky17 force-pushed the issue-9140-new-inferwidths branch from 0f16622 to d1856cc Compare December 12, 2025 01:59

uenoku reviewed Dec 15, 2025

View reviewed changes

wky17 force-pushed the issue-9140-new-inferwidths branch from 478d652 to cc26c73 Compare December 15, 2025 11:24

wky17 added 16 commits December 16, 2025 13:09

[format] Fix clang-format issues

74f2623

remove dependency on boost, using llvm/graphtraits

ff3c23e

add a cmdline control over new-inferwidths in firtool

1f11329

remove unordered_map, use DenseMap instead

7754b45

collect new tests in issue9140

ee9279b

remove /test_new_inferwidths folder, add a new file named infer-width…

57d6772

…s-new.mlir in /test/Dialect/FIRRTL

add Constraint2 for conditions, w_c <= 1

0b18f0c

follow clang-format

18c3fb8

[InferWidths] Add missing <stack> include for std::stack

fb33916

solve unexpected error: 'firrtl.circuit' op does not contain module w…

85735af

…ith same name as circuit

fixed clang-format

603f7fb

put entire debug info for loops under LLVM_DEBUG & including header a…

7d1f8d3

…t the top of file

working on add some comments for Constraint1/2/Min. TBD

081fc79

test new inferwidths pass

5b2da96

compilation error due to losing ';'s

a48e50b

wky17 force-pushed the issue-9140-new-inferwidths branch from cc26c73 to a48e50b Compare December 16, 2025 05:10

wky17 added 2 commits December 16, 2025 13:13

compilation error due to losing a 'l'

25da6f6

compilation error due to losing 'l's

42ace46

		//===- InferWidths_new.cpp - Infer width of types -------------------*- C++
		//-*-===//

	//===- InferWidths_new.cpp - Infer width of types -------------------*- C++
	//-*-===//
	//===----------------------------------------------------------------------===//

[FIRRTL] Add alternative constraint-based InferWidths pass #9173

Are you sure you want to change the base?

[FIRRTL] Add alternative constraint-based InferWidths pass #9173

Uh oh!

Conversation

wky17 commented Nov 3, 2025

[WIP][FIRRTL] Add formally verified alternative InferWidths pass

🔍 Related Issue

📖 Background & Motivation

⚙️ Technical Approach

🧪 Testing Strategy

🚀 Integration Plan

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wky17 commented Nov 24, 2025

Uh oh!

wky17 commented Dec 11, 2025

Uh oh!

wky17 commented Dec 11, 2025

Uh oh!

wky17 commented Dec 11, 2025

Uh oh!

wky17 commented Dec 12, 2025

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

uenoku commented Dec 15, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants