- Middlesex University,
- Concordia University Hardware Verification Group and
- the University of Provence.

The following people have been involved with the work:

- Paul Curzon, Queen Mary, University of London, UK
- Sofiene Tahar, Concordia University
- J. Lu, Concordia University
- Solange Coupet-Grimal, University of Provence
- Line Jakubiec, University of Provence
- Mike Gordon, Cambridge University

- Fairisle as a Verification Case Study
- A Comparison of HOL and MDG
- A Comparison of HOL, MDG and VIS
- A Comparison of HOL and Coq
- List of Publications
- Details of Publications

- Solange Coupet-Grimal and Line Jakubiec, Laboratoire d'Informatique de Marseilles, University of Provence.
- The Marseilles group reworked the specifications of the 4 by 4 fabric, and have verified a significant proportion of it in Coq.
- MDG Verification Group, University of Montreal and Concordia University, Canada
- The MDG Group reverified the 4 by 4 fabric using a verification system based on multiway decision graphs. They have also verified aspects of a port controller based on Fairisle and are using the 16 by 16 fabric as a case study in work combining the MDG and HOL systems. The group at Concordia also reverified the 4 by 4 fabric using the VIS system.
- Hardware Verification Group , University of Karlsruhe, Germany
- The MEPHISTO Group at Karlsruhe 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.
- Tom Gebhardt, Oxford University
- Used the Handel system to compile high level (essentially Occam) descriptions of the system into Xilinx hardware.
- M. Fairtlough (University of Sheffield) and M. Mendler (University of Passau)
- Considering using it as a case study for the Propositional Lax Logic .

Each system has distinct advantages and disadvantages. The specification styles used are totally different: timing diagrams versus state transition diagrams. Which is preferred is perhaps a matter of taste. The MDG style of specification could potentially be used in the HOL approach, though not vice versa. The MDG verification was faster, involving weeks rather than a few months of effort. Much of the slow down is actually due to the modular approach adopted with HOL. With MDG the whole design is specified and verified in one go. With HOL each module is specified and verified separately. This is more time consuming as each module must be individually understood, specified and verified. However, it pays off for the verification of subsequent related designs which then take only days. Furthermore, because of this comprehensive inspection of all modules, design changes can be suggested that improve or simplify the design. It also means that the HOL approach is potentially scalable to larger designs whereas the MDG approach is not. MDG provides a relatively straightforward way to check specific properties of a design. It also provides counter-examples when errors are encountered. With HOL, the problem of finding the cause of errors is eased because of the thorough understanding of the design that is obtained. This does not occur with MDG because of its black-box approach. A final advantage of the HOL approach is the extra confidence its results are afforded because of its LCF-style design.

For more information see:

- A Comparison of MDG and HOL for Hardware Verification
- Sofiene Tahar and Paul Curzon. In
*the 1996 International Conference on Theorem Proving in Higher Order Logics*, LNCS, Springer-Verlag, 1996. - Comparing HOL and MDG: A Case Study on the Verification of an ATM Switch Fabric.
- Paul Curzon and Sofične Tahar, Accepted by the
*Nordic Journal of Computing*, October 1998.

For more information see:

- Three Approaches to Hardware Verification: HOL, MDG and VIS compared.
- Sofiene Tahar, Paul Curzon and Jianping Lu. In
*Formal Methods in Computer Aided Design 98*, 1998.

For more information see:

- A Comparison of the Coq and HOL Proof Systems for Specifying Hardware.
- Line Jakubiec, Solange Coupet-Grimal and Paul Curzon. In
*the Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics*, edited by Elsa L. Gunter and Amy Felty, pages 63-78, August 1997.

- Comparing HOL and MDG: A Case Study on the Verification of an ATM Switch Fabric.
- Paul Curzon and Sofične Tahar, Accepted by the
*Nordic Journal of Computing*, October 1998. - Three Approaches to Hardware Verification: HOL, MDG and VIS compared.
- Sofiene Tahar, Paul Curzon and Jianping Lu. In
*Formal Methods in Computer Aided Design 98*, 1998. - A Comparison of the Coq and HOL Proof Systems for Specifying Hardware.
- Line Jakubiec, Solange Coupet-Grimal and Paul Curzon. In
*the Supplementary Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics*, edited by Elsa L. Gunter and Amy Felty, pages 63-78, August 1997. - 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. - The Formal Verification of the Fairisle ATM Switching Element
- Paul Curzon. Technical Report 329, University of Cambridge Computer Laboratory, 1994.