[circt-bmc] Add multi-clock BMC support via independent toggling#9803
Draft
robert-at-pretension-io wants to merge 3 commits intollvm:mainfrom
Draft
[circt-bmc] Add multi-clock BMC support via independent toggling#9803robert-at-pretension-io wants to merge 3 commits intollvm:mainfrom
robert-at-pretension-io wants to merge 3 commits intollvm:mainfrom
Conversation
Remove the single-clock restriction from ExternalizeRegisters and add support for verifying designs with multiple independent clock domains. - Add verif.clocked_by op to associate externalized registers with their clock, preserving clock-register relationships through the pipeline. - LowerToBMC generates per-clock init/loop regions; each clock toggles independently via verif.symbolic_value, allowing the SMT solver to explore all asynchronous interleavings. - Update VerifToSMT to use per-register posedge detection based on the clock mapping from verif.clocked_by, replacing the single-clock assumption.
Add detailed inline documentation explaining: 1. Why symbolic values are used to non-deterministically toggle clocks in LowerToBMC. 2. Why the auxiliary verif.clocked_by ops must be erased before SMT conversion. 3. How the If-Then-Else (ITE) logic enforces strict per-register posedge gating based on clock domain mapping.
robert-at-pretension-io
force-pushed
the
robert/bmc-multi-clock
branch
from
767e8d3 to
fe62f39
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR removes the single-clock restriction from
circt-bmcto enable the formal verification of Clock Domain Crossing (CDC) logic.Per feedback on previous PR #9729, this implements a mathematically rigorous asynchronous model:
verif.clocked_byduringExternalizeRegistersto associateexternalized registers with their specific driving clocks, preventing the loss of clock relationships in
the SSA graph.
LowerToBMCto XOR the clocks with averif.symbolic_valueateach step. This forces the SMT solver to explore all possible asynchronous clock drift interleavings
rather than assuming lockstep behavior.
VerifToSMTto parse the metadata and generate strict If-Then-Elselogic, ensuring registers only update state when their specific clock domain experiences a posedge.