We define a DSL for hardware description, called λπ -Ware, embedded in the dependently-typed language Agda, which makes the DSL well-scoped and well-typed by construction. Other advantages of dependent types are that circuit models can be simulated and verified in the same language, and properties can be proven not only of specific circuits, but of circuit generators describing (infinite) families of circuits. This paper focuses on the relations between circuits computing the same values, but with difierent levels of statefulness. We define common recursion schemes, in combinational and sequential versions, and express known circuits using these recursion patterns. Finally, we define a notion of convertibility between circuits with difierent levels of statefulness, and prove the core convertibility property between the combinational and se-quential versions of our vector iteration primitive. Circuits defined using the recursion schemes can thus have diferent architectures with a guarantee of functional equivalence up to timing.