Cet article présente Proof2Silicon, un nouveau framework de synthèse de bout en bout permettant de générer du matériel formellement vérifié à partir de spécifications en langage naturel. Proof2Silicon s'appuie sur PREFACE, un framework existant indépendant du modèle, pour améliorer le taux de réussite de la vérification du code Dafny généré par LLM basé sur l'apprentissage par renforcement. Il convertit ensuite le code Dafny vérifié en code C et génère une implémentation RTL à l'aide de Vivado HLS. Des évaluations comparatives sur 100 tâches montrent que PREFACE améliore le taux de réussite de la vérification du code Dafny jusqu'à 21 %, tandis que Proof2Silicon atteint un taux de réussite de la synthèse RTL jusqu'à 72 %. Cela démontre un pipeline automatisé robuste et évolutif, des spécifications en langage naturel à l'implémentation sur silicium.
