La simulation et les méthodes de vérification formelle

La conjonction de l'evolution des technologies de fabrication des circuits integres et de la nature du marche des systemes electroniques fait que l'on est amene a concevoir des circuits de plus en plus complexes (plusieurs millions) de transistors en un temps de plus en plus court (quelques mois). Ce phenomene a entraine une metamorphose du processus de conceptiuon. Si le principe de la conception reste le meme (il s'agit de generer une realisation physique sous forme d'une puce en partant d'une specification systeme), les outils mis en œuvre et l'organisation du travail durant le processus de conception ont, en revanche, beaucoup evolue. Ainsi, on est passe de la conception ou l'on dessinait les masques du circuit sur du papier special, a une conception quasi automatique qui part d'une description du comportement du circuit sous forme d'un programme dans un langage de haut niveau. Cet ouvrage a pour but de decrire les methodes et les outils d'aide a la conception de haut niveau des systemes electroniques digitaux integres. Apres une presentation des elements de base necessaires a l'etude des langages, des methodes et des outils de conception (chapitre 2), le lecteur trouvera une description des concepts et des techniques utilises pour la conception comportementale (chapitre 3). Il s'agit de raffiner un modele de haut niveau decrivant les operations de calcul, de controle et de communication d'une application donnee, en un ou les fonctions sont decoupees en calculs elementaires pouvant etre realises en un seul cycle d'horloge (conception logique). Le chapitre 4 est consacre aux concepts et aux techniques utilises pour la conception systeme. Elle consiste a realiser le decoupage logiciel/materiel pour transposer une specification fonctionnelle en langage de haut niveau, sur une architecture composee de circuits specialises et de processeurs genereaux (ou specialises interconnectes). Pour controler la qualite de la conception il faut s'assurer que les specifications initiales decrivent bien la fonctionnalite souhaitee, puis il faut verifier que les differentes etapes de raffinement preservent cette fonctionnalite. Dans le chapitre 5, la verification d'equivalence, la verification de proprietes, la simulation symbolique et la demonstration de theoremes sont donc abordees. Le chapitre 6 de l'ouvrage traite du domaine emergeant qui a rendu possible l'integration de systemes complexes sur une puce : la conception des systemes heterogenes. Il s'agit de systemes pouvant comporter des parties provenant de plusieurs equipes utilisant des methodes de conception differentes.