The Correctness of Biphase Mark Protocol

When digital signals are exchanged between two independently clocked devices, the signal read is not exactly the signal written, depending on the phases and rates of the two clocks and the communications delay, among other things.

Communications protocols are designed to handle this. For example, the ``biphase mark protocol'' (also known as ``FM'' or ``single density format'') encodes a bit stream and a series of clock edges into a square wave to overcome the problem. The biphase mark protocol is widely used, e.g., it is the standard for single density magnetic floppy disk recording and a version of it, called the ``Manchester protocol'', is used in the Ethernet and is implemented in various hardware serial interfaces.

I became interested in formalizing and verifying such a protocol: it is a necessary step in trying to build a verified system containing several processors. I therefore developed a model of asynchronous communication. The model transforms the signal stream produced by one device into that consumed by an independently clocked one, given the phases and rates of the clocks, the communications delay and a nondeterministic ``oracle.''

Then, using this model I formalized and proved the following theorem with Nqthm.

Correctness of Biphase Mark Protocol: An 18-bit/cell biphase mark protocol reliably sends messages of arbitrary length between two independently clocked devices provided the ratio of the clock rates is within 5% of unity.

For details of the model and the biphase mark proof, see

A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol. In Formal Aspects of Computing, 6(1) 1994, pp. 60-91.

[Best Ideas] [Publications] [Research] [Home]