Titre:
Using the Coq system for the formal verification of the Fairisle ATM 4x4 Switch Fabric
Conférencier:
Line Jakubiec ,
Laboratoire d'Informatique de Marseille
Université de Provence - UFR MIM
39, Rue Joliot Curie
13453 MARSEILLE Cédex 1
Lieu:
CONCORDIA UNIVERSITY, Dept. of Electrical and Computer Engineering ,
Room S-H961-14
Date et heure:
vendredi le 28 août 1998 de
15:00 à 00:00
Résumé:
We are concerned with the formal verification of sequential circuits.
After a short presentation of the Coq proof assistant and of its underlying theory, we will show how we deal with some special features of the Coq system in hardware verification. In particular, we use dependent types and co-induction to specify circuits and their behaviour. Then, the correctness of these circuits is established using a co-inductive reasoning.
Hardware specifications with dependent types give a precise and so reliable representation of circuits. Examples from the 4x4 Swith Fabric will illustrate this aspect, showing the interest of dependent types in our work, but also the drawbacks they can raise.
The other aspect developed in the talk, is the notion of co-inductive definitions in hardware. These greatest fixpoint definitions are used to describe infinite sequences of values (streams). In our study, these sequences represent the history of the values carried on wires or, in other words, input and output signals of circuits. Then, we specified circuits and their behaviours as functions on streams. As examples, some units of the Fabric are studied.
The proofs establish equivalences between the output stream of the considered circuit and the stream constructed from the behavioural description.
Reasoning by co-induction for verifying circuits allows to preserve the elegant way of representing the time in the specifications. Moreover, we obtain proofs in which the combinational results are clearly separated from temporal results.