Formal Verification of Hardware Synthesis

Thomas Braibant 1, * Adam Chlipala 2, *
* Auteur correspondant
2 PLV
CSAIL - Computer Science and Artificial Intelligence Laboratory [Cambridge]
Abstract : We report on the implementation of a certified compiler for a high-level hardware description language (HDL) called Fe-Si (FEatherweight SynthesIs). Fe-Si is a simplified version of Bluespec, an HDL based on a notion of guarded atomic actions. Fe-Si is defined as a dependently typed deep embedding in Coq. The target language of the compiler corresponds to a synthesisable subset of Verilog or VHDL. A key aspect of our approach is that input programs to the compiler can be defined and proved correct inside Coq. Then, we use extraction and a Verilog back-end (written in OCaml) to get a certified version of a hardware design.
Type de document :
Communication dans un congrès
Natasha Sharygina and Helmut Veith. Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. Springer, 8044, pp.213-228, 2013, Lecture notes in computer science. <10.1007/978-3-642-39799-8_14>
Liste complète des métadonnées


https://hal.archives-ouvertes.fr/hal-00776876
Contributeur : Thomas Braibant <>
Soumis le : dimanche 20 janvier 2013 - 21:42:36
Dernière modification le : mercredi 29 juillet 2015 - 01:25:24
Document(s) archivé(s) le : dimanche 21 avril 2013 - 02:20:09

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Thomas Braibant, Adam Chlipala. Formal Verification of Hardware Synthesis. Natasha Sharygina and Helmut Veith. Computer Aided Verification - 25th International Conference, Jul 2013, Saint Petersburg, Russia. Springer, 8044, pp.213-228, 2013, Lecture notes in computer science. <10.1007/978-3-642-39799-8_14>. <hal-00776876>

Partager

Métriques

Consultations de
la notice

237

Téléchargements du document

198