Superconductor electronics (SCE) is an emerging hardware technology that allows for highly power-efficient circuit designs. SCE circuits are based on inherently stateful gates that communicate via transient \textit{pulses}, in contrast to conventional CMOS technology that uses stateless gates that communicate via low vs high voltage levels (the traditional ‘zeroes’ and ‘ones’ of Boolean logic). These differences mean that decades of optimizations and techniques for reasoning about hardware designs are rendered obsolete for SCE designs. Advancing the state of SCE requires new techniques for formally reasoning about SCE designs and notions of equivalence and other relations between SCE circuits.

In this paper we describe Citrus, an embedded DSL in the dependently-typed language Agda for describing SCE circuits that allows for equational reasoning about SCE circuit equivalence. Citrus provides a formal description of SCE gates by embedding them into the theory of arrows and provides tools to reason about equivalence between circuits in the form of time-abstract bisimulation. We evaluate Citrus using a case study in which we prove that an SCE circuit optimization, previously proposed by people working on real SCE circuits but heretofore unproven to be correct, is indeed a semantics-preserving transformation.