Normal view MARC view ISBD view

Vérification formelle de descriptions VHDL comportementales / Félix Nicoli ; sous la direction de Jean-Luc Paillet

Auteur principal : Nicoli, Felix, AuteurAuteur secondaire : Paillet, Jean-Luc, Directeur de thèseAuteur secondaire collectivité : Université Aix-Marseille 1, Etablissement de soutenanceType de document : ThèseLangue : français.Pays : France.Éditeur : [S.l.] : [s.n.], 1999Description : 1 vol. (209 p.) ; 30 cmBibliographie : Bibliogr. p. [159]-168.Sujet MSC : 68V15, Computer science support for mathematical research and practice, Theorem proving
68N15, Theory of software, Theory of programming languages
68W35, Algorithms in computer science, Hardware implementations of nonnumerical algorithms (VLSI algorithms, etc.)
94Cxx, Information and communication theory, circuits - Circuits, networks
97-02, Research exposition (monographs, survey articles) pertaining to mathematics education
Note de thèse: Thèse de doctorat, informatique, 1999, université Aix-Marseille I
Tags from this library: No tags from this library for this title. Log in to add tags.
Current location Call number Status Date due Barcode
CMI
Salle S
Thèses NIC (Browse shelf) Available 00256-01

Bibliogr. p. [159]-168

Thèse de doctorat informatique 1999 université Aix-Marseille I

CETTE THESE S'INSCRIT DANS LE CADRE DE LA VERIFICATION FORMELLE DE CIRCUITS DIGITAUX ET TRAITE PLUS PARTICULIEREMENT DE LA CERTIFICATION DE DESCRIPTIONS VHDL COMPORTEMENTALES EN VUE DE LA SYNTHESE DE HAUT NIVEAU DE COMPOSANTS ELECTRONIQUES. NOTRE APPROCHE CONSISTE A MODELISER UNE PARTIE DU LANGAGE VHDL DANS LE DEMONSTRATEUR DE THEOREMES NQTHM. POUR CE FAIRE, NOUS DISTINGUONS UN SOUS-ENSEMBLE COMPORTEMENTAL DE VHDL QUI INCLUT LES PROCESS, TOUTES LES INSTRUCTIONS SEQUENTIELLES DE BASE ET LES FONCTIONS UTILISATEUR (EN PARTICULIER LES FONCTIONS DE RESOLUTION). NOUS DEFINISSONS ENSUITE LA SEMANTIQUE DENOTATIONNELLE DE CE SOUS-ENSEMBLE, CE QUI PERMET DE DONNER UN ENONCE EXTREMEMENT RIGOUREUX ET PRECIS DE LA SIMULATION DES DESCRIPTIONS QUI EN SONT ISSUES EN TERME DE CYCLE DELTA. LE COMPORTEMENT DES SIGNAUX EST MODELISE PAR DES PILOTES ET DES HISTORIQUES. NOUS DEDUISONS DE CETTE FORMALISATION, DES REGLES DE TRADUCTION SYSTEMATIQUE DE VHDL VERS LE DEMONSTRATEUR NQTHM. NOUS OBTENONS UN ENSEMBLE DE FONCTIONS RECURSIVES QUI MODELISENT UNE DESCRIPTION VHDL ET SA SIMULATION. LA VERIFICATION D'UNE DESCRIPTION REPOSE SUR CES DEFINITIONS AINSI QUE SUR DES BIBLIOTHEQUES GENERALES DE THEOREMES EN PARTICULIER SUR LE MODELE DU TEMPS DE VHDL, LES PILOTES, LES HISTORIQUES, ET LES PRIMITIVES VHDL. NOUS PROPOSONS UNE METHODE REUTILISABLE DE PREUVE POUR UNE CLASSE SPECIFIQUE DE DESCRIPTIONS : UNE SEULE INSTRUCTION DE TEMPORISATION PAR PROCESS ET DES AFFECTATIONS DE SIGNAL A DELAI NUL. CETTE STRATEGIE REPOSE SUR LA PREUVE DE PROPRIETES QUI DOIVENT ETRE VERIFIEES PAR LA SIMULATION D'UNE DESCRIPTION.

There are no comments for this item.

Log in to your account to post a comment.