Formal proves control properties for every reachable state when the proof is unbounded, and up to the bound otherwise; simulation exercises long system flows. Neither covers the chip alone. The failure mode is not choosing wrongly but choosing vaguely: an obligation assumed covered by both methods and verified by neither, or counted twice to inflate confidence. One ledger with one owner per obligation removes both.
Each obligation names its method and its gap. Formal rows carry the proof status, the bound or the induction argument; simulation rows carry the tests and the coverage that shows the scenario ran. Double-counting is forbidden: an obligation proven formally is not also claimed as simulation coverage, and a simulation-tested flow is not quoted as a formal result. Each method's gap is stated plainly: bounded formal misses past its bound, simulation samples rather than exhausts.
The table assigns each design's key obligations, with the formal evidence status the formal runs of this course give. Control properties with small state go to formal; long data flows and system sequences go to simulation with named tests. The bridge's data path is the illustrative split: conservation and integrity proven formally with a tracked word, sustained throughput measured in simulation.
Design | Formal owns | Formal evidence | Simulation owns | Gap each side states |
|---|---|---|---|---|
Four-entry FIFO | Overflow, underflow, flags, ordering. | Proven at k equal to 2 with the tracked-slot helper. | Sustained throughput and back-to-back stress. | Formal: data proof is one tracked slot; simulation: sampled traffic only. |
Four-way arbiter | One-hot grant, no phantom grant, work conservation, bounded wait (a request waits at most 3 cycles). | Proven at k equal to 1 with helpers, k equal to 4 without. | Fairness under realistic request patterns. | Formal: no request-holding rule assumed; simulation: no exhaustion. |
Skid-buffer bridge | Conservation, hold of valid and data under stall, tracked-word integrity. | Proven at k equal to 2 with three helper invariants; no k up to 12 closes it without them. | Throughput and long stall sequences. | Formal: tracked-word proof, one word at a time; simulation: sampled. |
Register block | Reset values, read-write, write-1-to-clear, read-only, isolation. | Proven at k equal to 2. | Driver sequences and access timing. | Formal: single-cycle interface; simulation: system interleavings. |
Pipelined arithmetic | Latency property and retimed equivalence. | Latency proven at k equal to 3; equivalence proven at k equal to 3, or 2 with the cut invariant. | Corner data values at speed. | Formal: 4-bit operands; simulation: no proof. |
Decade counter | Range invariant and step behaviour. | Proven at k equal to 2 with the range invariant. | Terminal-pulse integration in the system. | Formal: block level only; simulation: sampled. |
Read each row as a contract: the formal evidence column is what the formal side may claim, the gap column is what it may not. The methods meet in the combination lessons linked below; this lesson only fixes who owns which row.
# illustrative: every obligation has exactly one owning method
owners = {"fifo-overflow": ["formal"], "fifo-throughput": ["simulation"],
"bridge-integrity": ["formal"], "bridge-stall-sequences": ["simulation"]}
required = ["fifo-overflow", "fifo-throughput", "bridge-integrity", "bridge-stall-sequences"]
def audit(owners, required):
faults = []
for o in required:
n = len(owners.get(o, []))
if n == 0:
faults.append(o + ": verified by neither")
elif n > 1:
faults.append(o + ": claimed by both")
return faults
assert audit(owners, required) == []
assert audit(dict(owners, **{"fifo-overflow": ["formal", "simulation"]}), required) == ["fifo-overflow: claimed by both"]
assert audit({k: v for k, v in owners.items() if k != "bridge-integrity"}, required) == ["bridge-integrity: verified by neither"]
print("PASS: complete allocation accepted; double-counted and unowned obligations rejected")Every obligation has exactly one owning method; no row is claimed by both, none by neither.
Formal rows carry status and bounds with justifications; simulation rows carry tests with coverage.
Each side states its gap in one sentence, and the other side either covers it or it is a waived risk with an owner.
Audit the ledger by obligation, not by method: list every requirement from the specification and find its row. Requirements with no row are the gaps, and they cluster at the boundary, such as reset sequencing across blocks or error responses under backpressure. When a bug escapes, the first question is which row owned it; the second is whether the row's stated gap already predicted the escape.
Once, under simulation with the measured numbers, with formal owning only the losslessness underneath. The block proof supports the measurement; it does not replace it.