Du B-événementiel pour du VHDL synthétisable

Partenaires Forcoment

Présentation du projet Forcoment

Le projet Forcoment (FORmal COdevelopMENT) est un projet focalisé PACA, financé par la région PACA, regroupant dans ses dernières étapes STMicroelectronics et ClearSy (4ème et 5ème conventions du Conseil Régional PACA), avec pour objectif de montrer qu’un modèle B événementiel d’une fonctionnalité peut être transformé en une description hardware qui s’intègre directement dans un cycle de développement classique de circuit électronique tel que celui des microcontrôleurs de STMicroelectronics.

Les travaux réalisés ont consisté en :

  • L’étude et la détermination d’abstractions utilisables pour la modélisation de circuits microélectroniques
  • La spécification de schémas de traduction de B-événementiel vers le sous-ensemble de VHDL utilisé par STMicroelectronics, et le développement du générateur de code associé
  • L’application en vraie grandeur sur une fonctionnalité de contrôle d’accès mémoire enfoui, Memory Protection Unit (MPU)

Un cycle de développement formel

Le processus actuel de développement de circuits (voir figure n°1) de type microcontrôleur chez STMicroelectronics fait appel au test de façon intensive pour les étapes de vérification qui précèdent l’élaboration physique du circuit (fonderie). Ces étapes représentent une part prépondérante du temps nécessaire à cette partie du développement. L’élaboration des plans de test repose sur le savoir-faire des ingénieurs en charge de la vérification et de la validation.

Cycle de développement Forcoment
Figure n°1 : premières étapes du cycle de développement d’une fonctionnalité d’un microcircuit

Dans le cadre de ce projet, nous avons voulu adapter l’utilisation du développement formel par étapes successives promu par le langage B, dont le développement de logiciels pour les systèmes ferroviaires est un succès manifeste, au domaine de la microélectronique. En effet ce domaine n’utilise les méthodes formelles qu’après coup, pour réaliser plusieurs activités de vérification, à la fois sur le code source et sur ses transformations en réseaux de portes logiques, ultime représentation avant l’entrée dans la chaîne de fabrication. Or les erreurs fonctionnelles les plus coûteuses sont souvent introduites dans les phases amont de ce cycle, bien avant l’écriture du code source, notamment dans les spécifications fonctionnelles, dans les spécifications de conception générale et de conception détaillée, dites spécifications d’implantation. Les outils de vérification sont pratiquement inexistants pour toutes ces représentations “papier” et seule la vigilance des relecteurs permet de trouver ces “graines d’erreur” qui deviennent des “forêts de dysfonctionnements” une fois enfouies dans le silicium.

Le projet Forcoment a permis de construire un cycle de développement alternatif (voir figure n°2) qui intègre la vérification formelle, donc exhaustive, du code VHDL par rapport aux spécifications fonctionnelles et d’interface, tout en restant compatible avec le reste du flot de développement. Ce cycle de développement repose sur la modélisation formelle en B événementiel de la fonctionnalité, avec pour objectif la construction correcte de fonctions digitales, les fonctions analogiques, hors portée des techniques utilisées, étant simplement intégrées dans le développement via leurs interfaces digitales.

Ce nouveau cycle commence avec l’écriture d’un modèle B-événementiel très simple contenant quelques évènements représentant une abstraction de la fonctionnalité. Les détails de fonctionnement liés à son enfouissement dans un microcircuit sont introduits peu à peu. On dit que le modèle enrichi de ces détails est raffiné. Le processus qui permet de passer d’un modèle à un autre, enrichi de détails, en explicitant les conditions qui le rendent conforme au premier s’appelle le raffinement. Le raffinement et la vérification des conditions de conformité sont effectués, à chaque pas de développement, en utilisant des mathématiques de base telles que les ensembles et leurs opérations, ou la logique des prédicats, ou encore les relations et les fonctions. Ces concepts se révèlent beaucoup plus proches de la logique binaire d’un circuit qu’il n’y paraît.

Le modèle B-événementiel le plus détaillé est finalement transformé en un module VHDL, grâce à l’utilisation du générateur de code développé ex-professo, nommé B4SYN pour B for Synthesis (B pour la synthèse). Le module VHDL produit par B4SYN est alors injecté dans la suite du flot traditionnel. La campagne de test menée sur le module VHDL issu du flot traditionnel a été menée avec succès sur celui produit par B4SYN, ce qui a permis de valider le nouveau flot.

Ce nouveau flot, bien qu’expérimental, est déjà capable de couvrir un grand nombre d’erreurs avec une assurance totale. Il devra toutefois intégrer les solutions ébauchées, et explorées au cours de ce projet, avant d’être étendu pour permettre la composition de fonctionnalités, et d’être déployé de façon industrielle.

Cycle de développement alternatif Forcoment
Figure n°2 : cycle de développement alternatif élaboré et expérimenté au cours du projet

 

Cas d’étude

Le cycle de développement décrit ci-dessus a été mis en œuvre sur un cas d’étude, un contrôleur d’accès mémoire enfoui, Memory Protection Unit (MPU), voir figure n°3.

Cas de figure Forcoment
Figure n°3 : position de la MPU dans le microcontrôleur sécurisé

Les quelques métriques recueillies lors des développements de ce module, à la fois dans le flot traditionnel et dans le nouveau flot expérimental permettent de réaliser une première comparaison (voir figure n°4). Bien que celle-ci ne soit en aucune manière étalonnée, on peut remarquer que les modules VHDL issus des deux flots représentent un effort de développement équivalent. Plus intéressant encore, ces modules donnent lieu, après synthèse, à un nombre de portes quasiment identique. Ce fait nous autorise à penser que la preuve formelle ainsi développée n’empiète absolument pas sur la liberté de conception nécessaire aux optimisations des microcircuits parmi les plus exigeants en termes de surface et qui font traditionnellement appel à des techniques de développement de type “cousu main”. De plus, le “cousu main” obtenu par ce nouveau flot est garanti complètement conforme à sa spécification et à sa conception par une preuve mathématique informatisée qui peut faire l’objet d’un audit.

Tableau comparatif développement formel
Figure n°4 : effort comparatif entre le développement traditionnel et le développement formel

Références

M. Benveniste – A « Correct by Construction » Realistic Digital Circuit – RIAB Workshop – FMWeek 2009 – Eindhoven