The work has been funded by the EPSRC. The project builds upon the existing expertise of the Automated Reasoning Group and the Systems Research Group at the University of Cambridge Computer Laboratory, UK.
The following people were involved with the project:
The Fairisle switch consists of port controllers and a switching fabric. The fabric forms the heart of the switch, routing ATM cells from input ports to output ports. It also arbitrates cell clashes and sends acknowledgements back to the input ports. It is self routing; making routing and arbitration decisions based on routing tags appended to the front of the cells by the port controllers. The tags are stripped off by the fabric. Fabrics come in various sizes. The smallest is the 4 by 4 fabric which connects 4 input ports to 4 output ports. The larger 16 by 16 fabric is constructed from 4 by 4 elements that are based on the 4 by 4 fabric design. They are connected in two rows of 4 elements in a delta network. Different element designs are used in the two rows. The port controllers are more complex. They deal with the queueing of cells, the addition of headers to control routing and other management tasks.
A more complete overview of the fabric designs is here.
|- Assumptions ==> (Implementation ==> Specification)
This states that the description of the implementation implies the specification under certain assumptions on the environment. Implementation gives a hierarchical structural description of the implementation down to the logic gate level: the components used, how they are wired together and which wires are inputs, outputs and local to the module. Specification gives the more abstract behavioural description consisting of the timing and functional behaviour of the module, mainly in the form of interval temporal style operators. Assumptions give the conditions on the environment (i.e.~inputs) under which the module will satisfy the specification. The implementation, behavioural specification and assumptions are given in the form of higher-order logic relations on the inputs and outputs (as appropriate). Once the separate modules have been independently verified, their correctness theorems are hierarchically combined to give a correctness theorem for the whole device. In general, the proofs involve expanding definitions, performing case splits over different time intervals, and appealing to previously proved lemmas about the functional behaviour over the given intervals. All lemmas used were proved within HOL.
For more information see:
The first task in verifying the 4 by 4 fabric was to provide formal structural and behavioural specifications of the implementation and all its component modules. As the fabric had not been designed with verification in mind these did not initially exist. The former was relatively simple as HDL descriptions did exist. It was straightforward to translate these to higher-order logic descriptions, to which formal verification could be applied. The resulting descriptions were very similar, up to surface syntax, to the originals. Some changes were made, however. In particular, extra features of HOL such as words of words were used and additional levels of hierarchy were added. This made the proof more tractable. It was not intended to change the design, just the description of it. The underlying netlists should have been identical. In fact some translation errors were made. These were discovered and corrected during the proof process. Whilst demonstrating that formal verification can detect errors and give an indication of their locations, this also highlights a reason for integrating formal methods into the design process rather than tagging it on as an afterthought. If the original designs had been written in a HDL suitable for formal verification, such mistakes could have been avoided.
Producing formal behavioural specifications was much harder than producing structural ones. The designs had only minimal documentation, so the formal specifications were largely reverse-engineered from the HDL descriptions. This was very time consuming; taking approximately 2 person-months. The resulting specifications contained many errors that were uncovered by the proof process. The number of such errors would have been reduced if the specification had been produced as an integrated part of the design process. The specifications of all modules were written before any proof was performed. In retrospect it would have been better to verify each module as it was specified. This would have prevented errors propagating throughout the hierarchy, as the modules' specifications were used to determine the behaviour of those which called them.
The proof of the 4 by 4 fabric took a total of approximately 2 person-months to complete. 3 weeks of this were taken up by the verification of 2 out of the 43 distinct modules of the design. The main reason these modules took so much longer was that the specifications contained many errors. Correcting the errors was time consuming. The interaction of different errors also hindered the proof process. The verifier got bogged down in the details of the proof. It is clear that formal proof should be used in conjunction with other techniques such as animation. Formal proof is a good way of finding small numbers of obscure errors, but it is better if more obvious errors are found by other methods prior to the proof attempt.
The designer estimated that had the 4 by 4 fabric been designed from scratch it would have required several months work. The formal proof thus took a roughly similar amount of time. If the verification had been integrated with the design it is likely that the specification and proof times would have been reduced for the reasons discussed. Thus formal proof could be a viable validation technique.
For more information see:
The 16 by 16 fabric is constructed from 4 by 4 elements connected in a regular array of two rows. In an ideal world, these 4 by 4 elements would just be 4 by 4 fabrics. However, in practice changes needed to be made. In fact two different designs resulted: one for the front row elements and one for the back row elements. We modified the original proof of the 4 by 4 fabric to verify these two new designs, both of which had been fabricated prior to the verification project. We also verified five other designs of which one had been fabricated.
The new designs were verified by first editing the structural and behavioural specifications to take account of the changes. The proofs were then modified by interactively rerunning the original proofs, fixing problems as they arose. Because the designs were modular, only modules whose specifications had been modified needed to be reverified. The changes to the implementations were all relatively small so it would be hoped that the reverification could be performed very quickly. This was indeed so. All seven new designs were verified in a matter of hours or days. Some speed up was expected because only modules that had been changed needed to be reverified. However, the speedup was much greater than would be expected from that alone. This is clearly demonstrated by the fact that the total time taken to specify and verify all seven new designs was less than seven days compared with the 4 months required to specify and verify the original. This was despite a similar number of modules being reverified as were in the original design. The rate at which modules were reverified, including those that were originally the slowest, was as fast as the original verification of the most trivial modules. The upper level modules which were originally slowest needed to be reverified for each new design because the specification of the whole device changed for each. Thus these slowest modules were actually verified most often.
There were several reasons for the increased speed-up. The most obvious was that the new specifications were largely error free. The rate of verification was noticeable slowed down in the presence of errors. The design which took the longest to reverify did so because it violated an assumption of the original specification. The modules in the original verification that took longest were the ones with most errors. The verification process helped locate errors, but it was not always immediately clear to the verifier what remedy was required. For example fixing the error might involve changing the behavioural specification, the implementation or the specification of a submodule. Thus much time was spent inspecting the design and proof when a problem was encountered. This time would almost certainly have been reduced if the verification was more closely coupled with the design.
There were fewer errors in the specifications for several reasons. Firstly, modifications were being made to a correct specification, thus there were less opportunities for errors to arise. Also, the verifier understood the designs very well after the original verification -- it is highly unlikely that the verification could be completed without this occurring. Thus for the reverification, the changes made were less likely to introduce errors.
A further reason for the speed up was that the proofs of individual modules was divided into a series of lemmas. Only some of the lemmas and thus proofs needed to be modified to account for the changes. Also, modifying a proof script is much quicker than creating one from scratch. This was highlighted by the verification of one of the designs which required completely new proofs for several modules. These proofs were far simpler than the originals but this design took longer than the other designs to verify. Most proofs in the other designs were largely still suitable, with Changes being required at just a few points. The task of reverification is in finding those points and then correcting the proof. The points are found relatively quickly by running the proof and seeing where it breaks (though the point where a proof breaks is rarely exactly the point where the change must be made).
The study highlighted a problem with the combination of reengineering specifications from the implementation and modifying old proofs. Some of the non-fabricated designs resulted from changes being made to the structural description which did not correspond to the changes made to the actual implementation. Since the behavioural specifications were reverse-engineered from these incorrect structural descriptions, the designs were successfully verified. The mistakes were only discovered when a 16 by 16 fabric constructed from these incorrect elements was attempted to be verified. Had the verification been incorporated into the design process (for example, by the designers using higher-order logic as the HDL) errors of this kind would be much less likely. This also emphasizes the advantages as the hierarchical proof methodology since the errors in the specification of one level were discovered when the next level was attempted to be verified.
For more information see:
For more information see:
Our approach was to attempt to verify existing, real hardware (notably the 16 by 16 fabric), identifying factors in the implementation which slowed the proof. On the basis of the identified bottlenecks, design changes were suggested by the verifier which it was believed would remove the problems. These were evaluated for acceptability by the original designer. A new design was specified incorporating many of these changes and a detailed implementation performed. Finally the new implementation was formally verified to determine whether the expected advantages were realized. We built on our preliminary work conducted as part of the EPSRC funded feasibility study (``Formal Verification of an Asynchronous Transfer Mode Network''). There we identified some areas where the design of the 4 by 4 elements might be altered, though no detailed implementation or verification was performed.
A range of possible design changes were identified: most totally acceptable to the designer. The new implementation was successfully formally verified. The problematic parts of the proof were removed. The specifications of each module in the new design and of the whole design itself are much simpler and clearer than in the original design. The assumptions made about the environment have been simplified dramatically and the more problematic ones removed completely. In particular, the troublesome environment assumption that had prevented the completion of the proof for the fabricated 16 by 16 fabric was removed. Various lemmas which previously needed to be proven about the environment assumptions were no longer needed. No significant extra proof work appears to have resulted. The new version of some of the lower level modules required longer proofs. However, as these units occur low in the hierarchy, and are thus relatively simple, the extra work was small.
Several general lessons arose with respect to the way a designer can make the verifier's task easier from the outset:
Keep the interfaces between modules simple. A common feature of the acceptable design changes is that they involve simplifying the environment assumptions of modules. This reduces the verification cost by removing or simplifying proof obligations, reducing the possibility of mistakes being made in those assumptions.
Push complexity down to the lowest levels. The biggest savings in verification time are made where modules deep in the hierarchy depend on assumptions that are discharged by modules much higher up. The result of removing such assumptions is often that extra proof complexity is pushed down to the simplest modules at the base of the hierarchy where it is most easily managed.
Start with a clean specification and stick to it. The specification of the modified design is very clean. If a designer were to write down a specification of the exact intended behaviour of the design before the implementation stage, it is likely that something similar would be produced. Many of the verification problems arose because specific implementation decisions introduced minor deviations from the clean specification.
Keep related designs as similar as possible. Clearly proof effort can be reduced if the number and degree of modifications made when a design is re-engineered is kept to a minimum. Designs should be made generic from the outset where possible. It is also important that the verification team are aware of possible future changes so that genericity can be built in.
We have shown that implementation changes can be made to a design that ease the verification task but that do not impeach on other design considerations. Indeed several of the design changes suggested improve the design with respect to other such considerations. Further research is required to investigate the practicality of incorporating design for verifiability into the design process.
Perhaps most importantly, designing with verifiability in mind encourages design simplicity. The designer may have to work a little harder to ease the verifier's task. However, the result is a much cleaner design. This is vitally important in itself for safety-critical systems where formal proof techniques are most likely to be used.
For more information see:
For more information see:
@InProceedings{CurzonLeslie96DCC,
author = {Paul Curzon and Ian Leslie},
title = {Improving Hardware Designs Whilst Simplifying their Proof},
booktitle = {Designing Correct Circuits},
series = {Workshops in Computing},
year = {1996},
publisher = {Springer-Verlag}
}
@InProceedings{TaharCurzon96,
author = {Sofi{\`{e}}ne Tahar and Paul Curzon},
title = {A Comparison of {MDG} and {HOL} for Hardware Verification},
booktitle = {Theorem Proving in Higher Order Logics: 9th International Conference},
editor = {Joakim von Wright and Jim Grundy and John Harrison},
number = {1125},
series = {Lecture Notes in Computer Science},
year = {1996},
publisher = {Springer-Verlag},
OPTpages = {415-430},
}
@InProceedings{Curzon95CHARME,
author = "Paul Curzon",
title = "Problems Encountered with the Machine-assisted Proof of
Hardware",
editor = "Paolo E. Camurati and Hans Eveking",
volume = "987",
series = "Lecture Notes in Computer Science",
pages = "56-70",
booktitle = "Correct Hardware Design and Verification
Methods",
year = "1995",
publisher = "Springer-Verlag",
}
@InProceedings{CurzonLeslie95ICECCS,
author = "Paul Curzon and Ian Leslie",
title = "A Case Study on Design for Provability ",
pages = "59-62",
booktitle = "The Proceedings of the First International Conference on
Engineering of Complex Computer Systems",
year = "1995",
publisher = "{IEEE} Computer Society Press",
month = nov,
}
@Article{Curzon95CJ,
author = "Paul Curzon",
title = "Tracking Design Changes with Formal Machine-Checked Proof",
journal = "The Computer Journal",
year = "1995",
volume = "38",
number = "2",
pages = "91-100"
}
@InProceedings{Curzon95WAR,
author = "Paul Curzon and Ian Leslie and Mike Gordon",
title = "Conclusions from a Study to Verify a Real Network Component",
booktitle = "Proceedings of the Second Workshop on Automated Reasoning:
Bridging the Gap Between Theory and Practice",
year = "1995",
month = apr,
}
@InProceedings{Curzon94PODC,
author = "Paul Curzon",
title = "The Formal Verification of an ATM Network",
pages = "392",
booktitle = "Proceedings of the 13th Annual ACM Symposium on Principles
of Distributed Computing",
year = "1994",
publisher = "{ACM} Press",
month = aug,
}
@InProceedings{Curzon94COMP,
author = "Paul Curzon",
title = "Experiences formally verifying a network component",
pages = "183-193",
booktitle = "Proceedings of the 9th Annual IEEE Conference on Computer Assurance",
year = "1994",
publisher = "{IEEE} Press",
}
@InProceedings{Curzon94HUG,
author = "Paul Curzon",
title = "Tracking Design Changes with Formal Verification",
pages = "177-192",
booktitle = "Higher Order Logic Theorem Proving and Its Applications: 7th
International Workshop",
year = "1994",
publisher = "Springer-Verlag",
editor = "Thomas F. Melham and Juanito Camilleri",
volume = "859",
series = "Lecture Notes in Computer Science",
month = sep,
}
@InCollection{Curzon94BLUE,
author = "Paul Curzon",
title = "The Formal Verification of the Fairisle Switch: The 4x4 Switching Fabric.",
booktitle = "{ATM} Document Collection 3 (The Blue Book)",
publisher = "University of Cambridge Computer Laboratory",
year = 1994"",
editor = "Richard Black",
chapter = "37",
address = "University of Cambridge Computer Laboratory, New Museums
Site, Pembroke Street, Cambridge CB2 3QG. England",
month = mar,
}
A hard copy can be ordered via ...
Email: tech_reports@cl.cam.ac.uk
Phone: +44 1223 334648
@TechReport{Curzon94ElementTR1,
author = "Paul Curzon",
title = "The Formal Verification of the {F}airisle {ATM} Switching
Element: an Overview",
institution = "University of Cambridge Computer Laboratory",
year = "1994",
number = "328",
month = mar,
}
A hard copy can be ordered via ...
Email: tech_reports@cl.cam.ac.uk
Phone: +44 1223 334648
@TechReport{Curzon94ElementTR2,
author = "Paul Curzon",
title = "The Formal Verification of the {F}airisle {ATM} Switching Element",
institution = "University of Cambridge Computer Laboratory",
year = "1994",
number = "329",
month = mar,
}
@InProceedings{Curzon95HUGV,
author = "Paul Curzon",
title = "Virtual Theories",
editor = "E. Thomas Schubert and Phillip J. Windley and James Alves-Foss",
volume = "971",
series = "Lecture Notes in Computer Science",
pages = "138-153",
booktitle = "Higher Order Logic Theorem Proving
and Its Applications: 8th International Workshop",
year = "1995",
publisher = "Springer-Verlag"
}
@InProceedings{Curzon95HUGM,
author = "Paul Curzon",
title = "The Importance of Proof Maintenance and Reengineering",
editor = "Jim Alves-Foss",
pages = "17-32",
booktitle = "International Workshop on Higher Order Logic Theorem Proving
and Its Applications: B-Track: Short Presentations",
year = "1995"
}