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:

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: