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:

- Paul Curzon
- Mike Gordon
- Ian Leslie

- The Fairisle Switch
- Hardware Verification using the HOL System
- Verifying the 4 by 4 Fabric
- Tracking Design Changes
- The 4 by 4 Switching Fabric as a Case Study
- A Comparison of HOL and MDG
- Verifying the 16 by 16 Fabric
- Design for Verifiability
- Proof Re-Engineering and Theory Management
- List of Publications
- Details of Publications

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 Formal Verification of the Fairisle ATM Switching Element: an Overview,
- Paul Curzon. Technical Report 328, University of Cambridge, Computer Laboratory, 1994.

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:

- Experiences Formally Verifying a Network Component
- Paul Curzon. In
*Proceedings of the 9th Annual IEEE Conference on Computer Assurance*, pp 183-193, IEEE Press, 1994. (Time taken, problems encountered, errors found for the 4 by 4 fabric verification) - The Formal Verification of the Fairisle ATM Switching Element: an Overview,
- Paul Curzon. Technical Report 328, University of Cambridge, Computer
Laboratory, 1994.
**(An earlier, longer version of the above.)** - The Formal Verification of the Fairisle ATM Switching Element
- Paul Curzon. Technical Report 329, University of Cambridge Computer
Laboratory, 1994.
**(The full HOL specifications of the 4 by 4 fabric modules)**

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:

- Tracking Design Changes with Formal Machine-checked Proof
- Paul Curzon.
*The Computer Journal*, 38 (2), pp 91-100, 1995. - Tracking Design Changes with Formal Verification
- Paul Curzon. In
*Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop*, edited by Thomas F. Melham and Juanito Camilleri,*Lecture Notes in Computer Science*, Volume 859, pages 177-192, Springer-Verlag, September 1994.**(An earlier version of the above paper)**

- Solange Coupet-Grimal and Line Jakubiec, Laboratoire d'Informatique de Marseilles.
- Have reworked the specifications in Coq, and are working on a verification of the 4 by 4 fabric in Coq.
- MDG Verification Group, University of Montreal, Canada
- Has reverified the 4 by 4 fabric using a verification system based on multiway decision graphs.
- Tom Gebhardt, Oxford University
- Used the Handel system to compile high level (essentially Occam) descriptions of the system into Xilinx hardware.
- Hardware Verification Group , University of Karlsruhe, Germany
- Used the Mephisto II System to reverify the 4 by 4 design using a combination of model checking and formal proof. Bit level specifications were used.
- Edelweis Helena Ache Garcez , University of Tuebingen
- Has verified some properties of the 4x4 fabric using the HSIS model checking tool.
- M. Fairtlough (University of Sheffield) and M. Mendler (University of Passau)
- Considering using it as a case study for the Propositional Lax Logic .
- S. Tahar, Concordia University
- has reverified aspects of the fabric using VIS

For more information see:

- Problems Encountered in the Machine-Assisted Proof of Hardware
- Paul Curzon. In
*Correct Hardware Design and Verification Methods*, LNCS 987, pp 56-70, Springer-Verlag, 1995.

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:

- Improving Hardware Designs whilst Simplifying their Proof
- Paul Curzon and Ian Leslie. In
*Designing Correct Circuits*, Workshops in Computing, Springer-Verlag, 1996.**(The implementation and verification of the redesigned 16 by 16 fabric)** - A Case Study on Design for Provability
- Paul Curzon and Ian Leslie. In
*the Proceedings of the First International Conference on Engineering of Complex Computer Systems*, pp 59-62, IEEE Press, 1995.**(Initial ideas on how the 16 by 16 fabric could be redesigned)**

For more information see:

- Virtual Theories
- Paul Curzon. Higher Order Logic Theorem Proving and Its Applications: 8th
International Workshop, Lecture Notes in Computer Science 971, pp 138-153,
Springer-Verlag 1995.
**(A prototype theory manager for HOL which allows multiple-active theories)** - The Importance of Proof Maintenance and Re-engineering
- Paul Curzon.
*International Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track: Short Presentations*, editor Jim Alves-Foss, pp 17-32, 1995.**(Discussion of why support for proof modification is at least as important as proof creation)**

- Improving Hardware Designs whilst Simplifying their Proof
- Paul Curzon and Ian Leslie. In
*Designing Correct Circuits*, Workshops in Computing, Springer-Verlag, 1996. - A Comparison of MDG and HOL for Hardware Verification
- Sofiene Tahar and Paul Curzon. In
*Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96*, Joakim von Wright, Jim Grundy, and John Harrison (Eds.) LNCS 1125, Springer-Verlag, 1996. - Hierarchical Formal Verification of Communication Networks
- Paul Curzon. Poster presented at EPSRC ITeC'96, Leeds, April 1996. (This looks best when blown up to A0 size!)
- Problems Encountered in the Machine-Assisted Proof of Hardware
- Paul Curzon. In
*Correct Hardware Design and Verification Methods*, LNCS 987, pp 56-70, Springer-Verlag, 1995. - A Case Study on Design for Provability
- Paul Curzon and Ian Leslie. In
*the Proceedings of the First International Conference on Engineering of Complex Computer Systems*, pp 59-62, IEEE Press, 1995. - Tracking Design Changes with Formal Machine-checked Proof
- Paul Curzon.
*The Computer Journal*, 38 (2), pp 91-100, 1995. - Virtual Theories
- Paul Curzon. Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, Lecture Notes in Computer Science 971, pp 138-153, Springer-Verlag 1995.
- The Importance of Proof Maintenance and Reengineering
- Paul Curzon.
*International Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track: Short Presentations*, editor Jim Alves-Foss, pp 17-32, 1995. - Conclusions from a Study to Verify a Real Network Component
- Paul Curzon, Ian Leslie and Mike Gordon. In
*Proceedings of the Second Workshop on Automated Reasoning: Bridging the Gap Between Theory and Practice*, April 1995. - The Formal Verification of an ATM Network
- Paul Curzon. In
*Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing*, page 392, ACM Press, August 1994. - Experiences Formally Verifying a Network Component
- Paul Curzon. In
*Proceedings of the 9th Annual IEEE Conference on Computer Assurance*, pp 183-193, IEEE Press, 1994. - Tracking Design Changes with Formal Verification
- Paul Curzon. In
*Higher Order Logic Theorem Proving and Its Applications: 7th International Workshop*, edited by Thomas F. Melham and Juanito Camilleri,*Lecture Notes in Computer Science*, Volume 859, pages 177-192, Springer-Verlag, September 1994. - The Formal Verification of the Fairisle Switch: The 4x4 Switching Fabric.
- Paul Curzon. Chapter 37 of
*ATM Document Collection 3 (The Blue Book)*, ed. Richard Black, University of Cambridge Computer Laboratory, 1994. - The Formal Verification of the Fairisle ATM Switching Element: an Overview,
- Paul Curzon. Technical Report 328, University of Cambridge, Computer Laboratory, 1994.
- The Formal Verification of the Fairisle ATM Switching Element
- Paul Curzon. Technical Report 329, University of Cambridge Computer Laboratory, 1994.

- Experiences Formally Verifying the Fairisle Switching Elements
- Paul Curzon. Presented at the University of Cambridge Computer Laboratory, in the Wednesday Seminar series on 9th November 1994. This seminar was broadcast live over MBONE.
- Hardware Verification and ATM Switches
- Paul Curzon. Invited Talk at the Colloquium on Formal Methods and Security, Isaac Newton Institute, Cambridge, April 1996.

- EPSRC final report for feasibility study.
- Summary of EPSRC final report for feasibility study.
- The proposal for the second phase of the project.

@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" }