Comparing Hardware Verification Systems

Comparing Hardware Verification Systems

As part of the Fairisle Verification project at Cambridge University, a 4 by 4 switch fabric that formed part of the Farisle ATM Networkwas verified. Fairisle is a working network that was not designed with formal verification in mind. As such it provides a realistic formal verification case study. The original verification funded by the EPSRC used the HOL Theorem Proving System. It has subsequently been taken up by several groups as a verification case study by several groups investigating a range of verification techniques and tools. We have since carried out several comparative studies of verification systems based on the 4 by 4 verication work. The work has involved collaboration between researchers at

The following people have been involved with the work:

Contents

Fairisle as a Verification Case Study

The 4 by 4 Switching Fabric has been used, or is being considered, as a case study by several other verification groups.
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 .
Other groups are encouraged to reverify the 4 by 4 fabric using their favourite verification (or synthesis) system. . The HOL specifications are publicly available.

A Comparison of HOL and MDG

In conjunction with the MDG group based at Montreal University, we have compared the HOL and MDG systems. MDG is based on a decision graph approach extended with a new technique called abstract implicit enumeration in which decision graphs are used to represent sets of states as well as the transition and output relations.

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.

A Comparison of HOL, MDG and VIS

The Concordia Verification Group reverified the 4 by 4 fabric using VIS. A three way comparison was then made between these systems.

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.

A Comparison of Coq and HOL

The Marseilles group respecified the 4 by 4 fabric using the Coq interactive proof system. This is based on constructive higher order logic which provides facilities for coinductive definitions and dependant types. A comparison of the differing specification approaches was made.

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.

Publications

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.

Details of Papers

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.

Abstract

Interactive formal proof and automated verification based on decision graphs are two contrasting formal hardware verification techniques. In this paper, we compare these two approaches. In particular we consider HOL and MDG. The former is an interactive theorem proving system based on higher-order logic, while the latter is an automatic system based on Multiway Decision Graphs. As the basis for our comparison we have used both systems to independently verify a fabricated ATM communications chip: the Fairisle 4 by 4 switch fabric.

Obtaining the paper

An online version of this paper is available as compressed postscript.