To formally verify a hardware design, a formal behavioural specification of the design and of the 43 modules in it is needed. Ideally the formal specification would be written first and the device implemented from it. The switching element had been designed and implemented without any form of formal behavioural specification being created. There was also only sketchy informal documentation. Therefore the formal specification was reverse engineered from the HDL description. This was a very time-consuming process taking between one and two man-months. The early versions of the specification contained many errors. To a large extent the formal verification process was used to aid the reverse engineering. As the proof progressed the specification was gradually corrected as the implementation was analysed and a better understanding of the design was obtained.
The formal behavioural specification of the switching element effectively describes a timing diagram for its inputs and outputs. It is given by a predicate over the input, output and state sequences. The predicate is true for sequences which are possible behaviours of the element. The functional behaviour of the element at a given time is dependent on the arbitration process. We specified this process as a function on the cell headers. Given a set of headers, the function describes the arbitration decision that will be made.