Document Open Access Logo

Pi-Ware: Hardware Description and Verification in Agda

Authors João Paulo Pizani Flor, Wouter Swierstra, Yorick Sijsling

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2015.9.pdf
  • Filesize: 0.67 MB
  • 27 pages

Document Identifiers

Subject Classification

Keywords
  • dependently typed programming
  • Agda
  • EDSL
  • hardware description languages
  • functional programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

There is a long tradition of modelling digital circuits using functional programming languages. This paper demonstrates that by employing dependently typed programming languages, it becomes possible to define circuit descriptions that may be simulated, tested, verified and synthesized using a single language. The resulting domain specific embedded language, Pi-Ware, makes it possible to define and verify entire families of circuits at once. We demonstrate this by defining an algebra of parallel prefix circuits, proving their correctness and further algebraic properties.

Cite As Get BibTex

João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling. Pi-Ware: Hardware Description and Verification in Agda. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 9:1-9:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2015.9

Author Details

João Paulo Pizani Flor
Wouter Swierstra
Yorick Sijsling

References

  1. Emil Axelsson, Koen Claessen, and Mary Sheeran. Wired: Wire-aware circuit design. In Dominique Borrione and Wolfgang J. Paul, editors, Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings, volume 3725 of Lecture Notes in Computer Science, pages 5-19. Springer, 2005. URL: http://dx.doi.org/10.1007/11560548_4.
  2. Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. Lava: Hardware design in Haskell. In Matthias Felleisen, Paul Hudak, and Christian Queinnec, editors, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), Baltimore, Maryland, USA, September 27-29, 1998., pages 174-184. ACM, 1998. URL: http://dx.doi.org/10.1145/289423.289440.
  3. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - A functional language with dependent types. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 73-78. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03359-9_6.
  4. E. Brady, J. McKinna, and K. Hammond. Constructing correct circuits: Verification of functional aspects of hardware specifications with dependent types. In M. T. Morazán, editor, Trends in Functional Programming 8, pages 159-176. Intellect, 2007. Google Scholar
  5. Thomas Braibant. Coquet: A Coq library for verifying hardware. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 330-345. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-25379-9_24.
  6. Thomas Braibant and Adam Chlipala. Formal verification of hardware synthesis. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 213-228. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39799-8_14.
  7. A. Camilleri, M. Gordon, and T. F. Melham. Hardware verification using higher-order logic. Technical Report 91, University of Cambridge Computer Laboratory, 1986. URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-91.pdf.
  8. Koen Claessen and David Sands. Observable sharing for functional circuit description. In P. S. Thiagarajan and Roland H. C. Yap, editors, Advances in Computing Science - ASIAN'99, 5th Asian Computing Science Conference, Phuket, Thailand, December 10-12, 1999, Proceedings, volume 1742 of Lecture Notes in Computer Science, pages 62-73. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-46674-6_7.
  9. Hadi Esmaeilzadeh, Emily R. Blem, Renée St. Amant, Karthikeyan Sankaralingam, and Doug Burger. Dark silicon and the end of multicore scaling. In Ravi Iyer, Qing Yang, and Antonio González, editors, 38th International Symposium on Computer Architecture (ISCA 2011), June 4-8, 2011, San Jose, CA, USA, pages 365-376. ACM, 2011. URL: http://dx.doi.org/10.1145/2000064.2000108.
  10. Morteza Fayyazi and Laurent Kirsch. Efficient simulation of oscillatory combinational loops. In Sachin S. Sapatnekar, editor, Proceedings of the 47th Design Automation Conference, DAC 2010, Anaheim, California, USA, July 13-18, 2010, pages 777-780. ACM, 2010. URL: http://dx.doi.org/10.1145/1837274.1837470.
  11. F. K. Hanna and N. Daeche. Dependent types and formal synthesis. Philos. Trans. Phys. Sci. Eng., 339(1652):121-135, 1992. URL: http://www.jstor.org/stable/54016.
  12. Ralf Hinze. An algebra of scans. In Dexter Kozen and Carron Shankland, editors, Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings, volume 3125 of Lecture Notes in Computer Science, pages 186-210. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-27764-4_11.
  13. IEEE standard VHDL language reference manual: IEEE standard 1076-1987, 1988. URL: http://dx.doi.org/10.1109/ieeestd.1988.122645.
  14. Warren A. Hunt Jr. FM8501: A Verified Microprocessor, volume 795 of Lecture Notes in Computer Science. Springer, 1994. URL: http://dx.doi.org/10.1007/3-540-57960-5.
  15. Pepijn Kokke and Wouter Swierstra. Auto in Agda - programming proof search using reflection. In Ralf Hinze and Janis Voigtländer, editors, Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings, volume 9129 of Lecture Notes in Computer Science, pages 276-301. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-19797-5_14.
  16. John Launchbury, Jeffrey R. Lewis, and Byron Cook. On embedding a microarchitectural design language within Haskell. In Didier Rémy and Peter Lee, editors, Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France, September 27-29, 1999., pages 60-69. ACM, 1999. URL: http://dx.doi.org/10.1145/317636.317784.
  17. U. Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology, 2007. URL: http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf.
  18. Nicolas Oury and Wouter Swierstra. The power of pi. In James Hook and Peter Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 39-50. ACM, 2008. URL: http://dx.doi.org/10.1145/1411204.1411213.
  19. I. Sander and A Jantsch. System modeling and transformational design refinement in ForSyDe. IEEE Trans. Comput. Aided Des. Integ. Circ. Syst., 23(1):17-32, 2004. URL: http://dx.doi.org/10.1109/tcad.2003.819898.
  20. M. Sheeran. muFP, a language for VLSI design. In Proc. 1984 ACM Symp. on LISP and Functional Programming, LFP '84, pages 104-112. ACM, 1984. URL: http://dx.doi.org/10.1145/800055.802026.
  21. Mary Sheeran. Hardware design and functional programming: a perfect match. J. UCS, 11(7):1135-1158, 2005. URL: http://dx.doi.org/10.3217/jucs-011-07-1135.
  22. Atze van der Ploeg and Oleg Kiselyov. Reflection without remorse: revealing a hidden sequence to speed up monadic reflection. In Wouter Swierstra, editor, Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014, pages 133-144. ACM, 2014. URL: http://dx.doi.org/10.1145/2633357.2633360.
  23. Paul van der Walt and Wouter Swierstra. Engineering proof by reflection in Agda. In Ralf Hinze, editor, Implementation and Application of Functional Languages - 24th International Symposium, IFL 2012, Oxford, UK, August 30 - September 1, 2012, Revised Selected Papers, volume 8241 of Lecture Notes in Computer Science, pages 157-173. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-41582-1_10.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact