Each module in the design was formally verified against its behavioural specification separately. The separate proofs were then combined to give a result about the whole element. If the modules are used in other designs their proofs can be reused. Thus the proofs can track design changes relatively quickly. We verified all modules down to the gate level.
Figure 1: Time taken to verify the switching element
Approximately two man-months were spent performing the verification. The breakdown of the time is given in Figure 1. It shows the cumulative time taken as each module was verified. The time (one week) spent proving general word theorems is not included. On the whole, the simpler modules were verified first. The verifier had not previously performed a hardware verification though was a competent HOL user.
Much of the effort was expended in understanding informally why the implementation was correct. This was hampered to some extent by the delay between writing the specifications for a module and doing the proof. Errors in the specifications slowed progress. When the presence of an error was discovered, it had to be located. The manner in which the proofs failed usually gave a strong indication as to the location of the error. However, it was not always immediately clear whether the error was in the behavioural or structural specification of the module, or because a component module's specification was too weak. Determining which was so involved examining the specifications of other modules as well as the faulty one. The specification then needed to be corrected and the proof completed. The main errors were in the modules where there are plateaus in the graph. No errors were discovered in the actual implementation of the switching element.
Some errors were introduced in the structural specification in the translation from Qudos HDL to HOL-HDL. The most serious such error was that the connections of two wires were swapped. Errors also occured in the behavioural specifications because the specifier was not originally familiar with the designs being specified and because very little informal documentation was available. The specifications would probably have contained fewer errors if written by the designers during the design process, or if there had been informal documentation for each module, rather than just for the top levels of the design. All errors found during the course of the verification were corrected and the proofs completed successfully.
No detailed record of the original time spent designing and testing the element was recorded. The design evolved from earlier designs, and several different designs were produced at the same time, making it difficult to accurately estimate the time scale involved. However, it has been estimated that had it been designed from scratch the initial design time would have been in the order of several months. The time spent testing would have been in the order of several weeks. However, errors were discovered after the testing process had been completed when the fabric was installed and in use. These errors would have been uncovered by formal verification had it been conducted before the element was installed rather than afterwards. Thus the time spent to formally specify and verify the design was not unreasonable. Furthermore, it is likely that it would have been much quicker if done as the element was designed since much of the time was spent attempting to understand the design. Had formal verification been applied to the ancestors of the design, the formal verification could have tracked the changes made, with a minimal amount of time spent adapting the proof for the new generation.
The final correctness statement contains an assumption about the environment in which the element operates. It states that the cell header does not arrive at an inopportune moment relative to the frame start signal. The fabric has no control over when these signals arrive as they are determined by the external environment. The design of the port controllers must ensure that the assumption is upheld. The condition was known about by the designers, though did not appear in the informal documentation. It was not originally known of by the verifier but was discovered during the verification.
The proof has been adapted to one of the other versions of the element that was designed at the same time. Due to the modular nature of the design and proof, only the modules which were affected needed to be reverified. It took months to complete the original verification. It took only a few days to modify the specifications and redo the verification for the new design.