A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware

We develop formal arguments about a bit clock synchronization mechanism for time-triggered hardware. The architecture is inspired by the FlexRay standard and described at the gate-level. The synchronization algorithm relies on a specific value of a counter. We prove or disprove values proposed in the literature. Our framework is based on a general and precise model of clock domain crossing, which considers metastability and clock imperfections. Our approach combines this model with the state transition representation of hardware. The result is a clear separation of analog and digital behaviors. Analog considerations are formalized in the logic of the Isabelle/HOL theorem prover. Digital arguments are discharged using the NuSMV model checker. To the best of our knowledge, this is the first verification effort tackling asynchronous transmissions at the gate-level.