[circt-bmc] Add multi-clock BMC support#9729
[circt-bmc] Add multi-clock BMC support#9729robert-at-pretension-io wants to merge 5 commits intollvm:mainfrom
Conversation
Remove the single-clock restriction from ExternalizeRegisters and LowerToBMC. The ExternalizeRegisters pass already handles each register independently via regOp.getClk(), so the foundClk guard that rejected multiple clock ports was unnecessary. LowerToBMC now counts all top-level clock inputs (numClocks) and generates one init/loop entry per clock: each clock is initialized to 0 (false) and toggled every step via seq.from_clock → comb.xor → seq.to_clock. Struct-embedded clocks are still rejected with a clear diagnostic. Tests: - Remove the two-clock error case from externalize-registers-errors.mlir - Update lower-to-bmc-errors.mlir: update struct-clock error message - Add two_clk_regs positive case to externalize-registers.mlir - Add multi-clock-bmc.mlir: end-to-end pipeline test for a two-clock design verifying init yields 2 clocks and loop toggles each independently
TaoBi22
left a comment
TaoBi22
left a comment
There was a problem hiding this comment.
Hi @robert-at-pretension-io, thanks for taking a look at this! I'm not certain this is exactly the right approach to tackle this though. The commenting in this PR claims that by toggling each clock in the loop region, we expore all possible interleavings. I don't agree with this - this means that we toggle every clock at the same time, which could potentially be a desired behaviour but certainly should not be the default (as it only explores one, fairly unlikely interleaving). If this is a behaviour you have a use-case for, then it's obviously worth supporting, but I'd suggest we probably want to have that be enabled by a flag.
Probably worth noting that a remaining challenge for multiple clock support when the clocks are toggled separately is that we currently don't have a way to identify which externalized registers are clocked by which values. Previous discussions on this came to the conclusion that we might want some kind of clocked_by verif operation to annotate outputs with their corresponding clock value (since we can't refer to an SSA value in an attribute)
…erif.clocked_by - Replaced fragile integer attribute tracking with verif.clocked_by SSA values. - Replaced synchronous clock toggling with independent verif.symbolic_value toggling in LowerToBMC to explore asynchronous CDC interleavings. - Added --sync-clocks flag for legacy synchronous behavior. - Added multi-clock integration tests.
|
@TaoBi22 Thanks for the feedback. I'm very excited to be a part of this project :) Please let me know if this implementation is better suited, always willing to make changes! |
|
Thanks for taking another pass @robert-at-pretension-io - it looks like there are a few separate things happening here now, so it might make sense to split them across PRs so we don't have multiple unrelated changes at once (makes reviewing a bit easier for me!). Might be easiest to stick to the flag to toggle all clocks together in this PR (if this is something you have a use case for), then add the additional ops/lowerings/changes in later PRs? |
|
2 participants
Implement robust multi-clock BMC support to enable formal verification of Clock Domain
Crossing (CDC) logic and asynchronous clock drift.
Core Changes:
verif.symbolic_value, allowing Z3 to mathematically explore all asynchronous
interleavings.
clocks, replacing fragile port-index tracking and ensuring stability during IR
passes.
legacy lockstep behavior.
Validation:
cdc-gray-counter.mlir: Proves the async model catches a subtle Gray counterprotocol failure (multi-bit jumps) that is "invisible" to the synchronous model.
multi-clock-bmc.mlir: Verifies end-to-end pipeline support for multiple clockinputs.
externalize-registers.mlir: Confirms correct hoisting and mapping of registers inmulti-clock designs.
This PR removes the single-clock restriction from ExternalizeRegisters and LowerToBMC
and updates VerifToSMT to handle the resulting SMT lowering.