Quartz: a framework for correct and efficient reconfigurable design

We present Quartz, the first language supporting advanced features such as polymorphism, overloading, formal reasoning and generic VHDL library compilation, for correct and efficient reconfigurable design. Quartz is designed to support formal reasoning for design verification and generic optimisation strategies can be captured as algebraic transformations; the correctness of such transformations has been established using the Isabelle theorem prover. The parameterisation supported by Quartz higher-order combinators makes the expression of regular designs with a parameterised level of pipelining much easier than the equivalent in VHDL. The language also supports reconfiguration through the use of virtual multiplexer blocks. We have used Quartz to describe a range of designs with parameterised pipelining, and investigated the different tradeoffs in speed, size and power consumption. For designs where pipeline registers can reduce glitch propagation, increasing the level of pipelining can reduce power consumption by as much as 90%