Initialement cette étude constituait un simple exercice de style ayant pour objectif d’évaluer la modélisation de circuits numériques simples à l’aide de la méthode B. Cette expérimentation était essentiellement motivée par la perception d’une analogie forte entre le domaine cible et les principes de la méthode B. Les circuits numériques sont de plus en plus complexes tant du point de vue de l’intégration que du point de vue des fonctions traitées. Actuellement, la principale activité de validation des circuits numériques consiste à réaliser une campagne de test. Il ne nous semble pas évident de faire front à cette complexité uniquement au travers d’activités de test. Le but de cet article est de présenter une approche méthodologique basée sur le couplage d’une conception VHDL et sur une vérification par preuve formelle basée sur la méthode B.

Mots-clés : circuits numériques, modélisation, méthode formelle, méthode B, preuve, raffinement, VHDL.