[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?

…ith same name as circuit

…t the top of file

test/Dialect/FIRRTL/infer-widths.mlir

wky17 · 2025-12-19T15:30:48Z

Hi @uenoku @seldridge 👋,
Thanks for your thorough review! I've addressed all your suggestions in the latest push. Below is a breakdown of the changes:

✅ Implemented Suggestions:

Include Statements
- Moved #include <list> and #include <stack> to the top of the file for better organization.
Memory Safety Improvement
- Replaced unsafe deque usage with a bump allocator as suggested.
Debugging Optimization
- Wrapped entire loops in LLVM_DEBUG blocks.

Test Pipeline Enhancement

Added explicit verification command to infer-widths.mlir:

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

Verification: All tests pass successfully ✅

Code Documentation
- Added detailed comments for:
  - Constraint1/Constraint2/Min classes
  - Key function behaviors throughout the file
- (Let me know if any section needs further clarification!)

➡️ Next Steps:

Happy to refine any remaining points
Will address additional feedback
Appreciate your expertise! 🙌

…idth inference, but I don't find 'firrtl.domain.define %B, %A' in infer-widths.mlir:468:5. Don't know the reason about this error

wky17 · 2025-12-23T01:45:07Z

Hi @uenoku @seldridge 👋,

Thank you for your feedback on the PR. I've addressed the memory safety concerns by implementing the suggested BumpPtrAllocator approach. However, I'm encountering an unexpected CI failure that needs your help.

CI Failure Analysis

The Windows CI test is failing with this error:

RUN: at line 2

d:\a\circt\circt\build\bin\circt-opt.exe --pass-pipeline='builtin.module(firrtl.circuit(firrtl-infer-widths-new))' --verify-diagnostics D:\a\circt\circt\test\Dialect\FIRRTL\infer-widths.mlir | d:\a\circt\circt\build\bin\filecheck.exe D:\a\circt\circt\test\Dialect\FIRRTL\infer-widths.mlir

executed command: 'd:\a\circt\circt\build\bin\circt-opt.exe' '--pass-pipeline=builtin.module(firrtl.circuit(firrtl-infer-widths-new))' --verify-diagnostics 'D:\a\circt\circt\test\Dialect\FIRRTL\infer-widths.mlir'

.---command stderr------------
D:\a\circt\circt\test\Dialect\FIRRTL\infer-widths.mlir:468:5: error: unexpected error: 'firrtl.domain.define' op not supported in width inference
    firrtl.domain.define %B, %A
    ^

Investigation Done

I've thoroughly investigated this issue:

File content verification:
- The referenced line (468) in infer-widths.mlir does not contain firrtl.domain.define %B, %A
- The entire file infer-widths.mlir has zero occurrence of firrtl.domain.define
Reproduction attempts:
- ✅ Ubuntu 22.04: ninja -C build check-circt passes all tests
- ✅ macOS (Sequoia 15.5): ninja -C build check-circt passes all tests
- ❌ Docker environment (using ./utils/run-docker.sh): cannot reproduce this error

Request for Assistance

Since I can't reproduce this locally, could you please help with:

Confirming if this is a known Windows CI issue
Suggesting additional debugging steps
Recommending Windows-specific test commands I could try

I'm happy to investigate further with your guidance. The complete test file and changes can be seen in the PR.

seldridge · 2025-12-23T01:47:39Z

It should be more than just Windows. See this commit: 1be4b77

Domain information can show up and it should ignored.

Add the `DomainDefineOp` to the list of operations which are ignored by FIRRTL's `InferWidths` pass as they have no effect. Signed-off-by: Schuyler Eldridge <[email protected]>

Sort the types for the "no-op" case when visiting operations in FIRRTL's `InferWidths` pass. Signed-off-by: Schuyler Eldridge <[email protected]>

Cleanup trailing whitespace in an `InferWidths` test. Signed-off-by: Schuyler Eldridge <[email protected]>

Gets rid of a Slang warning.

Programs are essentially just modules. There are a few subtle semantic differences, but we aren't far enough down the simulation path to have those show up. For the time being, just treat programs as modules. We will add the necessary exit blocking mechanisms later on when we have sufficient simulation support in Arcilator.

Add support for lowering the `moore.builtin.time` op to a new `llhd.current_time` op that simply materializes the current simulation time as an SSA value. Error diff on circt-tests: ```diff -37 error: failed to legalize operation 'moore.builtin.time' +22 error: failed to legalize operation 'moore.time_to_logic' +15 error: failed to legalize operation 'moore.fmt.time' 0 total change ```

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 added 10 commits December 19, 2025 11:44

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

3e38c6e

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

dad21bc

…ith same name as circuit

fixed clang-format

2c1ce1c

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

871de46

…t the top of file

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

d70580b

test new inferwidths pass

f06423f

compilation error due to losing ';'s

b139a3f

compilation error due to losing a 'l'

916be11

compilation error due to losing 'l's

9b17309

using bump allocator instead of unsecure deque

db8244b

wky17 force-pushed the issue-9140-new-inferwidths branch from 42ace46 to db8244b Compare December 19, 2025 03:44

seldridge reviewed Dec 19, 2025

View reviewed changes

test/Dialect/FIRRTL/infer-widths.mlir Show resolved Hide resolved

wky17 added 2 commits December 19, 2025 14:14

fix clang-format

ea14574

add some comments for the code

c2ca057

clang-format for comments

5ab37d7

wky17 requested review from seldridge and uenoku December 21, 2025 14:53

error: unexpected error: 'firrtl.domain.define' op not supported in w…

e197140

…idth inference, but I don't find 'firrtl.domain.define %B, %A' in infer-widths.mlir:468:5. Don't know the reason about this error

seldridge and others added 7 commits December 23, 2025 10:43

[FIRRTL] Ignore domain.define in InferWidths

a57ef92

Add the `DomainDefineOp` to the list of operations which are ignored by FIRRTL's `InferWidths` pass as they have no effect. Signed-off-by: Schuyler Eldridge <[email protected]>

[FIRRTL] Alpha-sort InferWidths no-ops, NFC

8575a2e

Sort the types for the "no-op" case when visiting operations in FIRRTL's `InferWidths` pass. Signed-off-by: Schuyler Eldridge <[email protected]>

[FIRRTL] Whitespace cleanup, NFC

705c142

Cleanup trailing whitespace in an `InferWidths` test. Signed-off-by: Schuyler Eldridge <[email protected]>

[ImportVerilog] Add missing automatic keyword to test

2fa5598

Gets rid of a Slang warning.

add support for DomainDefineOp

6e4db92

wky17 requested review from fabianschuiki and maerhart as code owners December 23, 2025 02:50

		//===- 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

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!

Uh oh!

wky17 commented Dec 19, 2025

✅ Implemented Suggestions:

➡️ Next Steps:

Uh oh!

wky17 commented Dec 23, 2025

CI Failure Analysis

Investigation Done

Request for Assistance

Uh oh!

seldridge commented Dec 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants