Two teams verify the same block. The formal team proves its properties and reports "100% proven". The simulation team closes coverage and reports "100% covered". At the review nobody can say, for a given rule, which team's evidence covers it, whether any rule was covered by neither, or whether both spent weeks on the same arbiter. Two kinds of evidence with no shared ledger are two half-plans.
How do you split a verification plan between formal and simulation?
The obvious split is by block: formal owns the arbiter, simulation owns the rest. It is simple and it leaves gaps at every boundary: the arbiter's interaction with the credit logic, the fairness rule nobody wrote as a property, the deep counter formal could not reach. The unit of planning should be the rule (lesson 2.6), and each rule should get the method that gives the strongest evidence for it, with one ledger recording which.
DCRouter rule | Primary evidence | Secondary | Why |
|---|---|---|---|
R1, R2 FIFO occupancy | Formal proof (lesson 7.9) | Scoreboard | Small control state; induction proves it for all depths |
R3 routing, R6 arbitration | Formal proof | Arbitration checker (lesson 5.10) | Every combination of requests; a proof beats any traffic pattern |
R7 credits | Formal proof | Credit audit | A conservation invariant |
R4, R5, R8 framing, lengths, CRC | Scoreboard | Formal if cheap | Data over whole packets; the reference model is simple |
R9, R10 counters | Simulation read-backs | Formal with a small counter configuration | Deep state (255 errors) |
R11, R12 registers | Formal register app (lesson 7.7) | Directed register tests | Mechanical comparison with the register table |
R13 sleep and wake | Assertions in simulation | Formal with induction | Timing rules over idle periods |
Performance and fairness bounds | Simulation monitors | Formal bounded-wait properties | Statistics need long runs |
Shared assertions: one property, checked in simulation every cycle and proved by formal (lesson 5.3).
Formal for coverage holes: a hole simulation cannot hit goes to formal, which reaches it or proves it unreachable (lesson 6.6).
Simulation traces as formal seeds: start a proof from a deep state reached in simulation, to look further than a bound from reset allows.
Formal counterexamples as directed tests: a counterexample replayed in simulation becomes a regression test.
One evidence ledger: each rule's column shows proof, test, coverage and waiver, whichever produced it (Part 14).
Practice | Purpose |
|---|---|
Verification plans with a method per requirement | Every rule has an owner and a kind of evidence |
Formal and simulation results merged into one coverage and status database | One view at reviews |
Formal engineers embedded with block teams | Properties written early, alongside the RTL |
A team (illustrative) assigned its coherence controller to formal and its data path to simulation. Formal proved the protocol properties, all within an abstraction that modelled the data path as always responding in one cycle. Simulation verified the data path with a protocol model that never issued back-to-back snoops. The bug lived in a back-to-back snoop with a slow data response: each team's assumption was the other team's untested case. A rule-based ledger would have shown "snoop with slow response" assumed by both and verified by neither.
Rules that cross the boundary (arbitration with credits, fairness over time) and each side's assumptions about the other fall between the two, with nobody owning them.
R6 arbitration: formal proves the winner choice for every request combination; the simulation arbitration checker confirms fairness under real traffic and catches anything outside the property set.
Plan by rule: each rule gets the method with the strongest evidence for it, and important rules get both.
Connect the methods: shared assertions, formal for holes, counterexamples as tests.
Keep one ledger, including every assumption one method leaves for the other.