Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.
Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.
Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.
Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Ben non. Cela ne marche pas que comme ça.
Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.
Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.
Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.
Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)
J'ai dû oublier d'autres types de vérification.
"La première sécurité est la liberté"