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 temporelles, déterministes,...

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

Aperçu historique[modifier | modifier le code]

Les concepts liés à ces méthodes d'analyses ont été développés 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. À 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[modifier | modifier le code]

L'ensemble des outils dédiés aux circuits électroniques s'appuyant sur des méthodes formelles sont répartis 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 informatiques ainsi que des approches par composants).

Model Checking[modifier | modifier le code]

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 fondent toutes sur la présence d'une spécification appropriée des attendus fonctionnels du système :

Theorem Prooving : le système est défini sous forme d'un théorème mathématique.
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.
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.
Symbolic Model Cheking

Equivalent Checking[modifier | modifier le code]

Les outils de ce type se fondent 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 :

Description fonctionnelle (Behavioural)
Description des transferts entre registres (RTL)
Description sous forme d'un réseau d'interrupteurs électriques (netlist)
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).