DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2015.9

Pi-Ware: Hardware Description and Verification in Agda

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

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

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

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)

Copy BibTex To Clipboard

@InProceedings{pizaniflor_et_al:LIPIcs.TYPES.2015.9,
  author =	{Pizani Flor, Jo\~{a}o Paulo and Swierstra, Wouter and Sijsling, Yorick},
  title =	{{Pi-Ware: Hardware Description and Verification in Agda}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{9:1--9:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.9},
  URN =		{urn:nbn:de:0030-drops-84791},
  doi =		{10.4230/LIPIcs.TYPES.2015.9},
  annote =	{Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming}
}

Search Results

Documents authored by Sijsling, Yorick

Pi-Ware: Hardware Description and Verification in Agda

Abstract

Cite as

Thanks for your feedback!

Could not send message