Méthode formelle (informatique)/Application: électronique

Méthode formelle (informatique)/Application: électronique

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

Nuvola apps important.svg Attention : En cours
Cette page a été créé pour pouvoir amener des notions propres à l'application des méthodes formelles au cas de la conception électronique.

Plusieurs notions développés ici pourront d'ailleurs être intégrées dans la page parente. Elles ont été intégrées ici avant toute demande d'intervention sur la page parente.

En effet celle-ci est parfois trop limitative et surtout n'indiquant pas le véritable état de l'art sur certains cas.

Fin de l’avertissement

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.

Sommaire

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.

A 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).

N.B. : Actuellement, les outils behavioural vs. xxx ne sont pas fonctionnels

Voir aussi

Articles connexes

Liens et documents externes

Ce document provient de « M%C3%A9thode formelle appliqu%C3%A9e %C3%A0 l%27%C3%A9lectronique ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Méthode formelle (informatique)/Application: électronique de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

  • Methode formelle (informatique) — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… …   Wikipédia en Français

  • Méthode formelle (informatique) — Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin …   Wikipédia en Français

  • Méthode formelle — (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels… …   Wikipédia en Français

  • Methode formelle appliquee a l'electronique — Méthode formelle appliquée à l électronique Attention : En cours Cette page a été créé pour pouvoir amener des notions propres à l application des méthodes formelles au cas de la conception électronique. Plusieurs notions développés ici… …   Wikipédia en Français

  • Méthode Formelle Appliquée À L'électronique — Attention : En cours Cette page a été créé pour pouvoir amener des notions propres à l application des méthodes formelles au cas de la conception électronique. Plusieurs notions développés ici pourront d ailleurs être intégrées dans la page… …   Wikipédia en Français

  • Informatique — Les moyens de calcul informatique peuvent établir une prévision météorologique à plusieurs jours grâce à la modélisation climatique. L informatique est le domaine d activité scientifique, technique et industriel concernant le traitement… …   Wikipédia en Français

  • L'informatique — Informatique L´informatique contraction d´information et automatique est le domaine d activité scientifique, technique et industriel en rapport avec le traitement automatique de l information par des machines telles que les ordinateurs, les… …   Wikipédia en Français

  • Problème informatique — Informatique L´informatique contraction d´information et automatique est le domaine d activité scientifique, technique et industriel en rapport avec le traitement automatique de l information par des machines telles que les ordinateurs, les… …   Wikipédia en Français

  • Système informatique — Informatique L´informatique contraction d´information et automatique est le domaine d activité scientifique, technique et industriel en rapport avec le traitement automatique de l information par des machines telles que les ordinateurs, les… …   Wikipédia en Français

  • Technologie informatique — Informatique L´informatique contraction d´information et automatique est le domaine d activité scientifique, technique et industriel en rapport avec le traitement automatique de l information par des machines telles que les ordinateurs, les… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”