Quelle méthode confirme mathématiquement, sans simulation, que la logique du circuit est inchangée avant et après la synthèse logique ?

Réponse : A. Vérification formelle d'équivalence

La vérification formelle d'équivalence établit de façon exhaustive, par des méthodes mathématiques, si deux circuits réalisent la même fonction logique. Sans vecteurs de test, elle garantit l'équivalence pour toutes les combinaisons d'entrées ; elle sert à vérifier avant et après la synthèse logique, le placement-routage ou un ECO. Essayer toutes les combinaisons par simulation est irréaliste dès que les entrées comptent quelques dizaines de bits. Le DRC contrôle les règles géométriques.