Cette thèse concerne l'utilisation de modèles fonctionnels dans le test de circuits intégrés complexes. Dans la première partie, des vecteurs de test sont générés pour les automates d'états finis a partir de leurs spécifications de synthèse. Un premier ensemble de vecteurs de test est calcule en parcourant tous les arcs du graphe de contrôle. Les valeurs d'entrées non spécifiées sur les transitions sont fixées afin d'accroitre la couverture. Il est montre que ce test a une excellente couverture par rapport a sa longueur. Les fautes résiduelles sont détectées par une methode de distinction sur les modèles machine juste machine fausse. La deuxième partie est consacrée au test hiérarchisé de circuits complexes. Les vecteurs de test locaux aux blocs sont justifies vers les entrées primaires et propages en avant vers les sorties primaires en utilisant des variables symboliques et des modèles fonctionnels pour les blocs traverses. Des techniques originale de propagation retardée permettent de restreindre le nombre d'échecs des propagations. Un prototype en prolog a été expérimenté