A FIFO control block can leave formal verification with every property proved and still deliver 34 uncovered bins in the simulation UCDB. That is not a contradiction. Formal has established the properties it was given, while simulation is reporting scenarios represented by its functional coverage model. The handoff between those two results is where coverage closure work begins.
This boundary appears whenever a team combines JasperGold or similar property-verification tools with simulation. Formal excels at exhaustive checking within a bounded state depth. It is not intended to exercise an entire functional coverage model across a large scenario space. Treating the boundary as workflow design, rather than as a contest between methodologies, makes the next step clearer.
What Formal Proves Well
Formal property verification is well suited to proving that an RTL design cannot enter an illegal state. Deadlock freedom, overflow protection, mutual exclusion, and protocol compliance over bounded transaction depths are useful examples. Proving that a FIFO cannot overflow for any input sequence, or that an arbiter cannot grant two requestors at once, gives assurance that simulation cannot match through sampling alone.
Formal cover properties add another useful result. A cover check can establish whether a design state is reachable before anyone spends time writing stimulus for it. When formal proves a coverage target unreachable, the appropriate action is generally a documented exclusion or waiver, not another constrained-random test.
The distinction is important in safety-critical work. A simulation run that exercises a property 10,000 times without a failure supplies evidence, not proof. A formal proof addresses every input sequence within the bounded model. Where the property and model are appropriate, that result should remain part of the sign-off record.
Where the Formal Boundary Appears
Formal verification usually meets its practical limit through state-space explosion. As the number of state elements grows, proving properties can degrade before exhaustive exploration becomes feasible. This follows from the computational cost of model checking large state spaces, not from a defect in one particular tool.
The handoff is common with large datapaths, especially blocks containing floating-point logic, and with interactions spanning more than two or three modules. Protocol sequences that require many clock cycles also press against bounded-depth limits. These are behavioral scenarios across a sizeable design, rather than isolated properties on a small state machine.
There is also a data-format problem. Formal tools do not naturally emit coverage results in the UCDb or UCIS forms used by simulation flows. A proof may establish that a behavior is impossible, while the simulation database still presents the related bin as open. Mapping formal evidence into exclusions therefore requires manual cross-reference or a bridge between the two result models.
Why Coverage Remains After Sign-Off
A block can pass formal sign-off for all specified properties and still show substantial simulation coverage gaps. That normally means the coverage model asks questions that were never encoded as formal properties: combinations of data patterns, ordering of protocol events, multi-master interactions, or error-recovery transitions.
Consider the FIFO example. Formal can prove overflow and underflow protection, pointer arithmetic, and gray-code conversion integrity. The simulation model may additionally contain bins for simultaneous reads and writes at selected fill levels, back-pressure thresholds, and recovery after invalid operations. Those are legitimate functional goals even when they are not natural formal properties.
For a small ASIC team using SystemVerilog coverage with Xcelium, VCS, or QuestaSim, the open targets are structured inputs rather than an undifferentiated test backlog. The UCDB identifies the uncovered bins, the coverage-group hierarchy identifies their scenario class, and the block interface defines the legal stimulus space. ChipAgents' Coverage Tracker can organize that evidence, while Test Writer can target bins that are reachable through constrained-random stimulus. Failure Explainer is useful when a new test reaches a related bin but fails elsewhere in the environment.
A Practical Formal to Simulation Handoff
Our preferred workflow has three stages after formal sign-off. First, record formal unreachability results as exclusions in the simulation coverage plan, including the proof reference. This is still a context-heavy step because someone must align formal names with coverage-group and bin names.
Second, triage the remaining UCDB gaps. Separate reachable targets from targets that need a different environment or a clarified model, then prioritize bins that can be addressed by targeted stimulus. In the FIFO case, simultaneous read and write at selected fill levels is a direct candidate for constrained-random bias.
Third, generate tests from the system context when the neighboring logic matters. The stimulus may need to drive upstream logic into back-pressure while also producing the FIFO fill level and input pattern required by a particular bin. A block-level test alone will not close a target whose cause lives in an AXI or other surrounding transaction sequence.
We are not saying that ChipAgents replaces formal verification, or that more generated tests can substitute for a proof of a safety property. We are saying that formal and agent-assisted simulation address different coverage classes. Formal supplies proof and reachability information where its model is tractable. The agents help continue closure for the functional scenarios that remain in the simulation plan.
What the Combined Flow Requires
A combined flow runs formal proofs first, records reachability and unreachability, applies justified exclusions to the simulation plan, and sends the remaining targets into agent-assisted test generation. Regression then evaluates the formal record alongside tests run through the team's existing simulator and coverage database.
The integration point is still the most manual part. JasperGold produces formal reports, but converting their meaning into UCDb exclusions requires an engineer who understands both the proof results and the simulation coverage model. That mapping is a practical area for future ChipAgents support, not a step to hide behind a general automation claim.
For teams already applying formal to control-intensive blocks, the incremental simulation work is narrower after the proof phase. The hardest safety and protocol properties have evidence behind them, while the remaining effort can focus on functional coverage closure. The useful handoff is therefore not "formal versus simulation"; it is a traceable decision about which open bins need a waiver, which need a better model, and which need targeted stimulus.