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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Augustsson, L., Schwarz, J., Nikhil, R.S.: Bluespec Language definition (2001)
Benton, N., Hur, C.-K., Kennedy, A., McBride, C.: Strongly Typed Term Representations in Coq. J. Autom. Reasoning 49(2), 141–159 (2012)
Berry, G.: The foundations of Esterel. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner. MIT Press (2000)
Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.J.: Putting it all together - Formal verification of the VAMP. STTT 8(4-5), 411–430 (2006)
Bjesse, P., Claessen, K., Sheeran, M., Singh, S.: Lava: Hardware Design in Haskell. In: Proc. ICFP, pp. 174–184. ACM Press (1998)
Bove, A., Coquand, T.: Formalising bitonic sort in type theory. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 82–97. Springer, Heidelberg (2006)
Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proc. ICFP, pp. 143–156. ACM (2008)
Chlipala, A.: A verified compiler for an impure functional language. In: Proc. POPL, pp. 93–106. ACM (2010)
Claessen, K., Sheeran, M., Singh, S.: The design and verification of a sorter core. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 355–369. Springer, Heidelberg (2001)
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. The MIT Press and McGraw-Hill Book Company (2001)
Coupet-Grimal, S., Jakubiec, L.: Certifying circuits in type theory. Formal Asp. Comput. 16(4), 352–373 (2004)
Dave, N., Arvind, Pellauer, M.: Scheduling as rule composition. In: Proc. MEMOCODE, pp. 51–60. IEEE (2007)
Gordon, M.: Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware (1985)
Gordon, M.J.C.: Relating Event and Trace Semantics of Hardware Description Languages. Comput. J. 45(1), 27–36 (2002)
Hanna, F.K., Daeche, N., Longley, M.: Veritas + : A Specification Language Based on Type Theory. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol. 408, pp. 358–379. Springer, Heidelberg (1990)
Hunt Jr., W.A., Brock, B.: The Verification of a Bit-slice ALU. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol. 408, pp. 282–306. Springer, Heidelberg (1990)
Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (2009)
Nikhil, R.S., Czeck, K.R.: BSV by Example (2010)
Pfenning, F., Elliott, C.: Higher-Order Abstract Syntax. In: Proc. PLDI, pp. 199–208. ACM (1988)
Richards, D., Lester, D.R.: A monadic approach to automated reasoning for Bluespec SystemVerilog. ISSE 7(2), 85–95 (2011)
Schneider, K.: Embedding Imperative Synchronous Languages in Interactive Theorem Provers. In: Proc. ACSD, pp. 143–154. IEEE Computer Society (2001)
Schneider, K.: The Synchronous Programming Language Quartz. Technical report, University of Kaiserslautern (2010)
Sheeran, M.: Hardware Design and Functional Programming: a Perfect Match. J. UCS 11(7), 1135–1158 (2005)
Slind, K., Owens, S., Iyoda, J., Gordon, M.: Proof producing synthesis of arithmetic and cryptographic hardware. Formal Asp. Comput. 19(3), 343–362 (2007)
Slobodová, A., Davis, J., Swords, S., Hunt Jr., W.A.: A flexible formal verification framework for industrial scale validation. In: Proc. MEMOCODE, pp. 89–97. IEEE (2011)
IEEE Standard System C Language Reference Manual (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Braibant, T., Chlipala, A. (2013). Formal Verification of Hardware Synthesis. In: Sharygina, N., Veith, H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, vol 8044. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39799-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-39799-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39798-1
Online ISBN: 978-3-642-39799-8
eBook Packages: Computer ScienceComputer Science (R0)