LIP6 2000/003
- Thesis
Abstraction Fonctionnelle des Circuits Numériques VLSI Avec une méthode formelle basée sur une extraction de réseau de portes - A. Lester
- 181 pages - 12/21/1999- document en - http://www.lip6.fr/lip6/reports/2000/lip6.2000.003.pdf - 725 Ko
- Contact : Anthony.Lester (at) nullavertec.com
- Ancien Thème : ASIM
- Keywords : Functional Abstraction, Circuit Disassembly, VLSI Verification, Integrated Circuit Design, Formal Methods, Boolean Partial Derivative, Pattern Recognition
- Publisher : Francois.Dromard (at) nulllip6.fr
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.