L'américain Jasper Design Automation, éditeur d'outils de vérification par la méthode des preuves formelles, vient d'ajouter à son catalogue un ensemble d'extensions de modélisation pour une vérification rapide et exhaustive des conceptions de chemins de données difficiles à gérer. Il s'agit de ''Formal Scoreboard Proof Accelerator'', un tableau de résultats optimisé pour la méthode formelle, de ''Clock Domain Crossing Proof Accelerator'', qui permet une vérification formelle des blocs contenant plusieurs domaines d'horloge asynchrones, et de ''Cache and FIFO Proof Accelerator'', qui assure une manière formelle sûre de modéliser des mémoires caches et des Fifo complexes.