ABSTRACT. Modelling digital circuits has been a fertile ground for functional programming and theorem proving. There have been numerous fruitful efforts to describe, simulate, and verify circuit in using functional languages, and such languages have also often been used as the host of hardware embedded DSLs.

When dependently-typed languages are used as host, we can have the hardware models simulated (with an executable specification) and verified in the same language, and properties can be proven not only of specific circuits, but of circuit generators describing entire (infinite) families of circuits.

In this paper we describe a deep embedding of a typed DSL for hardware description and verification, called λπ-Ware, using the dependently-typed language Agda as host. We define several common recursion schemes with the primitives of this DSL, in both combinational and sequential versions, and show how known circuits can be expressed in terms of these recursion patterns.

Finally, we make clear a notion of equivalence between circuits with different levels of parallelism, and prove the core equivalence property between the parallel and sequential versions of our vector iteration primitive. Circuits defined using the common recursion schemes can then easily be implemented in more or less parallel architectures with the guarantee that their behaviour will be equivalent up to timing.