We describe work in progress to formally verify the Fairisle switch. To date we have formally verified the Fairisle 4x4 switching fabric using the HOL 90 theorem prover [1][2]. We formalised both the implementation and its behaviour. We then used formal logic to rigorously prove that the behaviour suggested by the description of the implementation satisfies the specified behaviour. In contrast to validation using inexhaustive testing, the results hold for all valid sets of inputs, not just for some small subset. Formal verification corresponds in this sense to exhaustive testing. However, the latter is infeasible for all but very small designs due to the number of cases to consider. Formal verification is feasible because of the use of mathematics (such as induction) to consider the results of many cases at once. It should be noted that formal verification deals with formal descriptions of real world objects and ideas. Theorems obtained are only as good as the descriptions used. The results are only as valid as the formal descriptions.
The time taken was comparable to the time originally spent designing, implementing and informally testing the element. No errors were found in the fabricated implementation. This was unsurprising as the element had been in service for some time prior to the formal verification work commencing. Undocumented ``features'' were found however and many errors were discovered in the initial versions of the formal specifications. This was also unsurprising since documentation of the design and its implementation was sparse.