[circt-bmc] Support seq.firreg with sync reset
#8698
Conversation
| @@ -150,6 +150,69 @@ void ExternalizeRegistersPass::runOnOperation() { | |||
| ++numRegs; | |||
| return; | |||
| } | |||
| if (auto regOp = dyn_cast<seq::FirRegOp>(op)) { | |||
There was a problem hiding this comment.
This whole statement is a lot of code duplication that it's probably better to avoid. I believe all the differences between the two cases are just having to call different getters to fetch similar information about the respective registers right (e.g. getInitial vs getPreset)? It would probably be neater to have some generic register lowering function that takes the input, initial value, reset etc. as arguments - then, you just need to have a case for each kind of register where you extract these values and call the method.
| // expected-error @below {{seq.firreg with async reset not yet supported}} | ||
| %1 = seq.firreg %in clock %clk reset async %rst, %c0_i32 : i32 | ||
| hw.output %1 : i32 | ||
| } |
There was a problem hiding this comment.
nit: this file is missing a newline at the end
| // CHECK: [[ADD:%.+]] = comb.add [[IN0]], [[IN1]] | ||
| // CHECK: hw.output [[OLD_REG1]], [[ADD]], [[OLD_REG0]] | ||
| // CHECK: } | ||
| hw.module @combreg_and_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) { |
There was a problem hiding this comment.
| hw.module @combreg_and_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) { | |
| hw.module @compreg_and_firreg(in %clk: !seq.clock, in %in0: i32, in %in1: i32, out out: i32) { |
(same change necessary in CHECK comment too)
|
Thanks for the advice! |
| return failure(); | ||
| } | ||
| // Sync reset | ||
| result.replaceAllUsesWith(newInput); |
There was a problem hiding this comment.
nit: we have this in both branches of the if, could it be moved outside?
Co-authored-by: Bea Healy <[email protected]>
Co-authored-by: Bea Healy <[email protected]>
This adds support for
seq.firregwith synchronous reset inExternalizeRegistersPass.Asynchronous resets are not supported because currently there isn't a way to update a register on the negedge.
When the async reset signal becomes true before the negedge and turns false before the posedge, register should be reset and store the reset value. This needs to specify and update the register on the negedge in
VerifToSMT.How to implement this need further discussion, maybe pass more information to
VerifToSMT, or first simplify the clock and circuit into a transition-system-like form.