-
Notifications
You must be signed in to change notification settings - Fork 309
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[HW][circt-synth] Implement AggregateToComb pass and add to circt-synth pipeline #8068
base: main
Are you sure you want to change the base?
Conversation
Would it make sense to have aggregate to comb lowering in a separate pass? To me, it seems like it could also be useful outside of the AIG lowering path. |
Generally yes, I agree. One concern is that the lowering pattern for |
592f785
to
b43e6f8
Compare
b43e6f8
to
abb9d77
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
include/circt/Dialect/HW/Passes.td
Outdated
let description = [{ | ||
This pass lowers aggregate *operations* to comb operations within modules. | ||
This pass does not lower ports, as ports are handled by FlattenIO. This pass | ||
will also change the behavior of out-of-bounds access of arrays. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we mention here how it changes the behavior? If I understand correctly it's just a refinement, so we're all good and wouldn't even need to mention it here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can we mention here how it changes the behavior?
Yes. I'll do.
If I understand correctly it's just a refinement
Yes, it's refinement so it should be fine from the semantics perspective but i would at least mention in the doc. Maybe in the future we might want to run post-synthesis simulation on arcilator but only pre-synthesis IR can catch out-of-bounds access in this case.
%c3_i2 = hw.constant 3 : i2 | ||
// NOTE: If the index is out of bounds, the result value is undefined. | ||
// In LEC such value is lowered into unbounded SMT variable and cause | ||
// the LEC to fail. So just asssume that the index is in bounds. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, for these kind of things, a translation validation tool would be quite nice 🙂
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah without circt-lec it has been almost impossible to implement lowering pattern with confidence for the correctness. Thank you @maerhart @frog-in-the-well @TaoBi22 for outstanding work!
This PR adds a new pass
HWAggregateToComb
that lowers array operations to comb operations. The pass converts:hw.array_get
to a mux tree using comb operationshw.array_create
andhw.array_concat
tocomb.concat
hw.aggregate_constant
tocomb.concat
of individual constantsThe PR also moves two utility functions from CombToAIG to the Comb dialect:
extractBits
: Extracts individual bits from a valueconstructMuxTree
: Builds a multiplexer tree from selectors and leaf nodesThe pass is required to run before CombToAIG to ensure array operations are
properly lowered to AIG. Strictly speaking other than array_get operations can be preserved
but array values prevent optimizations at AIG level. So for the simplicity, I think it's reasonable
to lower array operations within circt-synth pipeline.
I currently added the pass under
HW/Transforms
consideringFlattenIO
is very similar but the pass might better belong to Conversion.