Sign-off is not a meeting; it is a package. One ledger of results, one register of assumptions, one coverage report, one waiver file, all tied to one source hash. This topic assembles that package for the four-entry FIFO end to end, then shows where formal evidence meets simulation evidence in a single ledger. Every line of the checklist points at the lesson that teaches it, so a reviewer can drill from any claim to its evidence in one step.
Lesson | After it you can... |
|---|---|
Walk the complete checklist and cite the evidence behind each line. | |
Assemble a real package: proofs, covers, assumption register, mutation score, bound and ledger gate. | |
Assign each obligation to a method with no gaps and no double-counting. |
Suggested order: top to bottom. The checklist first, because it names everything; the worked FIFO package next, because it fills every line with real runs; the joint ledger last, because it places the formal package inside the wider verification sign-off.
The discharge story: which environment rules each proof relied on, where each is proved elsewhere, and what input classes were excluded. Without it the proofs are conditional on undocumented terms.