Abstraction Fonctionnelle des Circuits Numériques VLSI Avec une méthode formelle basée sur une extraction de réseau de portes

A. Lester

LIP6 2000/003: THÈSE de DOCTORAT de l'UNIVERSITÉ PARIS 6 LIP6 / LIP6 research reports
181 pages - Décembre/December 1999 - French document.

Get it : 708 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Architecture des Systèmes Intégrés et Micro-Électronique

Titre français : Abstraction Fonctionnelle des Circuits Numériques VLSI Avec une méthode formelle basée sur une extraction de réseau de portes
Titre anglais : A Formal Method for the Functional Abstraction of Digital VLSI Circuits based upon the Extraction of a Gate Netlist

Résumé : Cette thèse s'inscrit dans le cadre de la vérification des circuits numériques de haute complexité. Elle porte sur le désassemblage et sur l'abstraction fonctionnelle. Le problème abordé concerne l'identification des portes et la génération automatique d'une description au niveau RTL à partir d'un réseau de transistors. L'obtention de ce réseau de portes facilite, par la suite, les vérifications temporelles et l'analyse de la consommation. Surtout, la description RTL permet une vérification fonctionnelle d'un circuit VLSI quelle que soit la méthode de conception. Elle permet aussi de réaliser la migration technologique par le biais d'une resynthèse de cette description comportementale vers une nouvelle technologie cible. Une méthode formelle (sans recourir à une bibliothèque de cellules prédéfinies) est proposée qui exploite les corrélations au sein d'un circuit pour extraire uniquement la fonctionnalité utile. Cela permet d'obtenir un réseau de portes avec une caractérisation fonctionnelle optimale. Le problème de la reconnaissance et la modélisation des éléments séquentiels est adressé par l'élaboration d'un algorithme original. Cet algorithme s'appuie sur la dérivée partielle booléenne pour analyser la stabilité et la capacité de mémorisation des boucles. La méthode permet de générer automatiquement un modèle comportemental pour tous les latchs statiques dans un circuit. Dans une dernière partie, la faisabilité d'une approche hybride est démontrée. Avec cette approche, une méthode par reconnaissance de formes hiérarchique vient compléter la méthode formelle. Cette approche apporte deux avantages principaux : premièrement il devient possible de traiter en entier des circuits contenant des parties analogiques, deuxièmement cette méthode permet un traitement plus efficace et une modélisation plus optimale des structures répétitives comme les RAMs.

Abstract : This doctoral thesis concerns the verification of highly complex digital integrated circuits. More precisely, circuit disassembly and functional abstraction. The problem considered is that of the automatic extraction of a gate netlist from a transistor netlist, together with the generation of a register-transfer level description. Not only does this gate netlist simplify subsequent timing and power consumption analysis, but also, more importantly, the RTL description allows functional verification of a VLSI circuit regardless of the design flow. In addition, it provides a method for technology migration through the resynthesis of the behavioural description onto a modern target technology. A formal method (not requiring a user-defined library) is proposed, which uses the correlation within a circuit to extract only the useful functionality. This results in the generation of a gate netlist that is optimum in terms of gate functional characterisation. The problem of the identification and the modelling of sequential elements is handled by an original algorithm. This algorithm uses the Boolean partial derivative to help in the analysis of the stability and the capacity to memorise of any combinatorial loops. The result is the automatic generation of a behavioural description for any kind of static latch. The final section demonstrates the feasibility of a hybrid method, in which a pattern recognition method complements the formal method. This kind of approach brings two advantages: firstly, it becomes possible to process circuits containing analog components, secondly it allows for a more efficient handling and more optimum modelling of repetitive circuit structures, such as RAMs.

Mots-clés : Abstraction Fonctionnelle, Désassemblage, Vérification VLSI, Conception des Circuits Intégrés, Méthodes Formelles, Dérivée Partielle Booléenne, Reconnaissance de Formes

Key-words : Functional Abstraction, Circuit Disassembly, VLSI Verification, Integrated Circuit Design, Formal Methods, Boolean Partial Derivative, Pattern Recognition

Publications internes LIP6 2000 / LIP6 research reports 2000

Responsable Éditorial / Editor :Francois.Dromard@lip6.fr