Stage 3 moves from what one design does to whether two designs agree. The pipeline lesson pins latency and the reset rule on the reference. The miter lesson proves the retimed twin equal, finds the planted twin fault, and measures the induction window with and without a helper. The last lesson scopes one intended change and proves everything outside it untouched. Causes are in the Solutions topic after stage 4.
Lesson | After it you can... |
|---|---|
Prove the latency-3 result, find the smallest induction window, and write your own mutants. | |
Prove miter equivalence, find the twin fault, and compare the windows with and without the helper. | |
Exhibit an intended difference and prove equivalence outside it. |
Suggested order: top to bottom. Latency first, because the miter says the twins agree, not that either is right; the twin next; the ECO last, because it reuses the miter idea with a changed revision.
Equal outputs prove the implementations agree, not that either is right: two copies of the same fault agree perfectly. The latency proof is the correctness half; the miter is the agreement half.