[FIRRTL] Add alternative constraint-based InferWidths pass #9173
Conversation
There was a problem hiding this comment.
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.
lib/Firtool/Firtool.cpp
Outdated
|
|
||
| // Width inference creates canonicalization opportunities. | ||
| pm.nest<firrtl::CircuitOp>().addPass(firrtl::createInferWidths()); | ||
| //pm.nest<firrtl::CircuitOp>().addPass(firrtl::createInferWidths()); |
There was a problem hiding this comment.
Please either add a cmdline control over this or remove the old line. Don't leave commented out code in the file.
| 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"; |
There was a problem hiding this comment.
Please don't commit commented out code. I might suggest adding some performance counters from MLIR to track and report these.
| if (mapping.areAllModulesSkipped()) | ||
| return markAllAnalysesPreserved(); | ||
|
|
||
| auto solve_time = std::chrono::high_resolution_clock::now(); |
There was a problem hiding this comment.
See if MLIR's timing mechanisms are sufficient.
|
|
||
| // 输出结果 | ||
| if (solution.has_value()) { | ||
| // LLVM_DEBUG(llvm::dbgs() << "可行解找到:\n"; |
There was a problem hiding this comment.
Please don't commit commented out code. It looks like the LLVM_DEBUG guard is sufficient to have the code in.
| // bab | ||
| //===----------------------------------------------------------------------===// | ||
|
|
||
| using Bounds = std::unordered_map<FieldRef, std::pair<int, int>, FieldRef::Hash>; |
There was a problem hiding this comment.
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.
| return success(); | ||
|
|
||
| bool mappingFailed = false; | ||
| TypeSwitch<Operation *>(op) |
There was a problem hiding this comment.
Consider using an OpVisitor.
| #include "llvm/ADT/SetVector.h" | ||
| #include "llvm/Support/Debug.h" | ||
| #include "llvm/Support/ErrorHandling.h" | ||
| #include <boost/graph/adjacency_list.hpp> |
There was a problem hiding this comment.
LLVM has a dim view of adding external dependencies. These would have to be very carefully considered.
| #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 was a problem hiding this comment.
There is a SCC implementation in MLIR which should likely be used.
| #include <boost/graph/floyd_warshall_shortest.hpp> | ||
| #include <boost/graph/strong_components.hpp> | ||
| #include <iostream> | ||
| #include <iomanip> |
There was a problem hiding this comment.
Please use MLIR/LLVM streams rather than the standard library.
| //===----------------------------------------------------------------------===// | ||
|
|
||
| // 节点类型 | ||
| using Node = std::variant<Zero, FieldRef>; |
There was a problem hiding this comment.
consider using a sentinel FieldRef. I think one already exists (value null).
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
wky17
force-pushed
the
issue-9140-new-inferwidths
branch
from
c9aaa58 to
2f3745a
Compare
|
PR Update Summary Hi maintainers, I've comprehensively updated this PR to address all previous feedback:
@llvm/circt-maintainers @seldridge @darthscsi Could you please re-run CI and review when convenient? |
2 participants
[WIP][FIRRTL] Add formally verified alternative InferWidths pass
🔍 Related Issue
Fixes #9140 (InferWidths failures on cyclic constraints)
📖 Background & Motivation
The current
InferWidthsimplementation 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:⚙️ Technical Approach
The new pass implements a constraint-based width inference engine with:
🧪 Testing Strategy
Comprehensive verification across 2 test dimensions:
(
test/Dialect/FIRRTL/infer-widths.mlir)test_new_inferwidths/• issue9140_0.mlir (example 1)
• issue9140_1.mlir (example 2)
🚀 Integration Plan
Following maintainer's phased adoption strategy:
firrtl-infer-widths-newopt-in