Structural analysis proves every crossing has a recognised structure — but not that the protocol around the structure behaves, nor that the structure survives synthesis. This topic covers the three dynamic and mathematical complements: formal protocol checking, metastability injection in simulation, and gate-level re-verification — plus how all four methods share regression without stepping on each other.
Lesson | After it you can... |
|---|---|
Say what formal protocol checking adds, what it assumes, and where it stops. | |
Explain what injection proves about the protocol and what it cannot prove. | |
List what synthesis and ECOs can break and what must be re-checked. | |
Combine structural, formal, and dynamic methods in regression with ownership. |
It confirms structure, not behaviour: protocols, settling assumptions, implementation damage, and runtime interaction all lie outside what structure can show. Each needs its own method.