Verifying TTP/C

Carnegie Mellon: The Rare Glitch Project E. Clarke and D. Kroenig

Abstraction Hierarchy

Formalizing TTP/C

TDMA round

MSG
slot

macro-
ticks

….

includes MFM

micro-
ticks

….

   macro-tick synchronization
   DPRAM access timing
   each SRU has own time base


	On top of this hierarchy one might want to consider the “cluster cycle”, which consists of multiple TDMA rounds of equal length.

	MFM=modified frequency modulation, also known as Miller code
	The Miller Code allows encoding a clock and a data signal on a single signal.
	E.g., also used in older harddisks etc.
	There are much better codes available now (in particular with respect to error detection).