[FIRRTL] Add alternative constraint-based InferWidths pass by wky17 · Pull Request #9173 · llvm/circt

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

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


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

+  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

+  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

+
+    // 输出结果
+    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

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

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


Consider using an OpVisitor.

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

+#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

+#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

+#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

+//===----------------------------------------------------------------------===//
+
+// 节点类型
+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!

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

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


nit: Please include header at the top of file

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

+  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

+  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

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

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 <schuyler.eldridge@sifive.com>

Sort the types for the "no-op" case when visiting operations in FIRRTL's `InferWidths` pass. Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>

Cleanup trailing whitespace in an `InferWidths` test. Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>

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 · 2026-01-12T03:21:17Z

Hi @uenoku @seldridge 👋, I have now resolved the upstream conflicts and can merge cleanly. Please help me review the code again.

seldridge · 2026-01-20T16:46:11Z

I gave this a spin on an internal design that is 1.7GiB of FIRRTL. There's a pretty major performance regression vs. the old infer widths:

Old:

Total Execution Time: 377.2114 seconds
----User Time----  ----Wall Time----  ----Name----
5.4665 (  0.7%)    5.4665 (  1.9%)    InferWidths

New:

Total Execution Time: 377.2114 seconds
----User Time----  ----Wall Time----  ----Name----
42.6200 (  4.3%)   42.6200 ( 11.3%)    InferWidths_new

I haven't dug into this more to see what is going on.

wky17 · 2026-01-28T14:58:57Z

Hi @uenoku @seldridge 👋,

Thank you for catching the performance regression in the earlier version and sharing those critical metrics! 🙏 I've taken this feedback seriously and conducted optimization on the width inference algorithm.

Performance Improvements

Using the largest available FIRRTL design I could access (309MB), here are the optimized results:

Version	`solver.solve()` Time	Speed vs Old
Old (original)	49.337 ms	1.0x
Initial PR	204.366 ms	4.14x slower
Optimized (the latest commitment)	11.123 ms	4.44x faster

Key optimizations:

Eliminated Heavy Copy Operations
Avoided copying large intermediate results (e.g., maps with hundreds of thousands of entries) during variable declarations and function result passing by using move semantics and pointers.
Constraint Map Pruning
Proactively removed solved variables from the constraint map after resolution, reducing the search space for subsequent operations. This is safe due to our topological sorting approach and improves performance as the algorithm progresses.

Could you please re-run your 1.7GiB test case with this optimized implementation? I'm confident you'll see significant improvements.

seldridge · 2026-01-28T16:44:57Z

Yes, this looks way better now. I reran this and am seeing:

Old:

  Total Execution Time: 311.8410 seconds 
  ----User Time----  ----Wall Time----  ----Name----
    6.3407 (  0.6%)    6.3407 (  2.0%)    InferWidths

New:

  Total Execution Time: 350.9843 seconds
  ----User Time----  ----Wall Time----  ----Name----
   12.7613 (  1.2%)   12.7613 (  3.6%)    InferWidths_new

wky17 · 2026-02-23T09:57:03Z

Hi @uenoku @seldridge 👋,

First, thank you for your last feedback - I'm really glad to hear the optimizations are heading in the right direction! 🚀

Since it's been about a month since your last review, would you be available for another look when convenient?

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

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

Comment thread test/Dialect/FIRRTL/infer-widths.mlir

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 <schuyler.eldridge@sifive.com>

[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 <schuyler.eldridge@sifive.com>

[FIRRTL] Whitespace cleanup, NFC

705c142

Cleanup trailing whitespace in an `InferWidths` test. Signed-off-by: Schuyler Eldridge <schuyler.eldridge@sifive.com>

[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

Merge branch 'main' into issue-9140-new-inferwidths

6ac3196

wky17 added 2 commits January 26, 2026 22:52

worked on efficiency problem

0e02047

clang-format

0a0822b

Merge branch 'main' into issue-9140-new-inferwidths

2247f33

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

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

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!

wky17 commented Jan 12, 2026

Uh oh!

seldridge commented Jan 20, 2026

Uh oh!

wky17 commented Jan 28, 2026

Performance Improvements

Uh oh!

seldridge commented Jan 28, 2026

Uh oh!

wky17 commented Feb 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone