Structural analysis asks “is there a synchroniser?” Formal protocol checking asks “does the logic around it behave?” — does the handshake never lose data, does the FIFO never overflow from clock drift, does the request always see a stable bus? The two methods meet at the crossing and together cover what neither covers alone.
Structural analysis shows | Formal checking adds | Example property |
|---|---|---|
A handshake synchroniser exists | The handshake cannot deadlock or drop data | Every request is eventually acknowledged exactly once |
FIFO pointers are Gray-coded | Full and empty are never wrong in their own domains | Empty is never asserted when data is present (read domain); full is never asserted when space remains (write domain) |
A pulse synchroniser exists | No pulse is lost or duplicated under the spacing rule | Every source pulse yields exactly one destination pulse |
Quasi-static qualification exists | The qualifier really covers every sample | The destination samples only while the qualifier is steady |
Formal proofs rest on environment assumptions: the clock relationship modelled, the minimum spacing between events, the stability windows the protocol relies on. Each assumption is a claim that must be reviewed like a waiver — an unreviewed assumption proves the design correct in a world that may not exist. The standard discipline is to list every assumption with the property it supports and review the list at the gate.
State space bounds the size of what can be proven: block-level protocols prove well, full-chip behaviour usually does not.
The synchroniser itself is modelled, not proven: formal assumes the flop settles within its window and checks everything around that assumption.
A proven property covers the modelled conditions only; an uncovered mode (test, debug, low power) needs its own run or its own argument.
The protocol circuits these properties target are taught in CDC handshakes and async FIFO; the verification mindset overlaps with CDC verification.
That the four-cycle spacing actually holds: the mechanism enforcing it, its owner, and evidence it operates — otherwise the proof assumes a world the design does not provide.
Behavioural guarantees around the structure: that full and empty can never be wrong, that pointers cannot lap under the depth argument, and that reset brings both sides to agreement.