An Embedded Hardware Description Language using Dependent Types.

This repository contains the source code and documentation of the Π-Ware project, developed as doctoral research by João Paulo Pizani Flor at Utrecht University.

Π-Ware is an Embedded Domain-Specific Language (EDSL) for hardware design, packaged as a library for the *dependently-typed* Agda programming language. It leverages dependent types in order to *ban* certain classes of design mistakes **by construction**, as well as to prove circuit correctness according to a high-level functional specification.

Circuits modeled in Π-Ware can be **simulated** (run over bit vectors) and can be **synthesized** to VHDL netlists. Properties over circuit behaviour can be proven using PiWare, even for (possibly infinite) **families of circuits**. Also, circuits can be compared for behavioural equivalence and, in this framework, semantics-preserving circuit optimizations can be established.

In contrast to other approaches to formal verification using automated solvers, Π-Ware is designed from the ground up to facilitate *compositional* and modular proofs. Several features are in place to help build proofs for a certain circuit *given proofs about its subparts*.

The project proposal, motivation, literature review, and high-level technical descriptions behind the design choices taken are documented in the project wiki.

The "root" Π-Ware repository has the following organization:

- The
`agda`

subdirectory contains all source code and auxiliary scripts to build/run PiWare - Under
`docs`

lie "manual-like" pages describing the design of the library and how to use it - In
`thesis`

you can find the M.Sc thesis report which started it all (with accompanying figures, etc.) - Under
`slides`

are sets of slides from presentations given about Π-Ware

For those wishing to obtain solely the Agda code of Π-Ware, there is a repository with only the library.

A first paper containing a general introduction to Π-Ware and a case study involving Parallel-Prefix Circuits (PPCs) was submitted to post-proceedings of the TYPES2015 workshop and a draft can be found at the address below: