Formal Verification

Quelle est la différence entre la Formal Verification et la Functional Simulation ?

La Formal Verification est un style de vérification différent mais qui atteint le même objectif final : éliminer les bogues de la conception. L'une des grandes différences entre la vérification formelle et la vérification fonctionnelle est le rôle que joue l'outil. La vérification formelle utilise une analyse statique basée sur des transformations mathématiques pour déterminer l'exactitude du comportement du matériel ou du logiciel, contrairement aux techniques de vérification dynamique telles que la simulation.

Dans la simulation, les test cases (scénarios) sont créés manuellement ou par un testbench automatisé, puis exécutés sur la conception RTL ou gate-level. Étant donné le nombre considérable d'états dans une conception, même petite, il est impossible de simuler plus qu'un petit pourcentage du comportement de la conception. La simulation est probabiliste ; les chances d'exercer un scénario qui révèle un bogue de conception sont faibles. La vérification formelle n'exécute pas la conception, elle ne nécessite donc pas de tests ou de testbench. Au lieu de cela, elle analyse statiquement la conception pour toutes les séquences d'entrée possibles et toutes les valeurs d'état possibles, en vérifiant si des assertions peuvent être violées. D'un point de vue théorique, la vérification formelle est exhaustive à cent pour cent, prouvant que toutes les assertions sont "sûres" une fois que tous les bogues ont été trouvés et corrigés.