Méthode formelle appliquée à l'électronique

Les méthodes formelles sont des techniques permettant d'assurer la bonne compréhension des fonctions attendues d'un système. Ces fonctions pouvant être temporels, déterministes,...

Elles permettent en outre de faciliter l'interconnexion de modules fonctionnels d'origines différentes (logiciel, matériel) en se basant sur des représentations mathématiques communes.

Aperçu historique

Les concepts liés à ces méthodes d'analyses ont été développé dans les années 1980 pour le codage informatique.

Dans les années 1990, ces concepts ont été étendus à la conception des circuits électroniques numériques. A ce jour, il n'est pas possible d'étendre ces techniques à l'intégralité des circuits analogiques. Cette limite est intrinsèque à l'approche des systèmes déterministes discrets.

Catégories d'outils

L'ensemble des outils dédiés aux circuits électroniques s'appuyant sur des méthodes formelles sont réparti en deux grandes familles : le model checking ou l'equivalent checking (on trouve aussi des méthodes vérifiant l'équivalence entre modèles pour les programmes informatique ainsi que des approches par composants).

Model Checking

Les outils de ce type utilisent une seule représentation du système. À partir de là, plusieurs approches sont possibles pour vérifier la réponse du système, son déterminisme, et donc son adéquation avec sa définition.

Voici une liste non exhaustive de ces techniques qui se basent toutes sur la présence d'une spécification appropriée des attendus fonctionnels du système :

1. Theorem Prooving : le système est défini sous forme d'un théorème mathématique.
2. Property Checking : le système est découpé sous forme de propriétés unitaires simples. La somme de ces propriétés devant définir l'ensemble des états valides du système.
3. Static Analysis : Cette technique commune à l'informatique peut s'apparenter au property checking, mais elle a le défaut de ne pas être en mesure de vérifier des comportements dynamiques du système.
4. Symbolic Model Cheking

Equivalent Checking

Les outils de ce type se basent sur le fait que la conception d'un circuit électronique implique plusieurs modèles, chacun ayant ses contraintes propres, et le fait que la complexité de ceux-ci fait que souvent l'ensemble consiste à intégrer des blocs fonctionnels d'origines diverses :

1. Description fonctionnelle (Behavioural)
2. Description des transferts entre registres (RTL)
3. Description sous forme d'un réseau d'interrupteurs électriques (netlist)
4. Allocation spatiale du réseau d'interrupteurs sur le composant (P&R, Layout)

Les outils de ce type comparent donc le modèle en cours avec un modèle, dit de référence (Golden Model), qui a été vérifié comme correspondant aux attentes unitaires, ou d'interface.

Il y a comparaison entre deux modèles de même niveau (behavioural vs. behavioural, rtl vs. rtl, netlist vs. netlist), ou de niveaux successifs (behavioural vs. rtl, behavioural vs. netlist, rtl vs. netlist).

Notes et références

Voir aussi

Articles connexes

• Méthode formelle (informatique)

Liens et documents externes

• Improve-HDL
• Rulebase
• Model Checking

• Portail de l’informatique
• Portail de l’électricité et de l’électronique