Pi-Ware: An Embedded Hardware Description Language using Dependent Types
Summary
Recently, the incentives for hardware acceleration of algorithms are growing, as Moore's law continues to hold but optimizations in traditional processors show diminishing returns. This growing need for hardware implementation pushes programmers towards hardware design, an activity with stricter correctness and performance requirements than software development.
A long-standing line of research is concerned with the application of functional programming techniques to hardware design, and the relatively recent dependently-typed programming paradigm has been claimed by many researchers to be the "successor" of functional programming. This thesis aims, therefore, to investigate what are the improvements that Dependently-Typed Programming (DTP) can bring to hardware design.
We developed a domain-specific language for hardware, called Π-Ware, embedded as a library in the Agda programming language. Π-Ware allows the specification of circuits, their simulation, synthesis and verification. Compared to similar approaches in the literature, Π-Ware provides high type safety and robust proofs of correctness for whole families of circuits, however it still needs significant improvements in terms of ease-of-use.