Inverting Martin Synthesis for Verification

Quasi Delay-Insensitive (QDI) circuits can be created through the procedure of Martin Synthesis, a series of transformations that begin with an executable specification and end in a transistor network. If these transformations are properly applied the circuits will be correct by construction, however if they are improperly applied, finding design errors can be quite difficult. We show that the forward transformations of Martin Synthesis are reversible, and that the inversion of these steps recreates the specification when applied to correctly synthesized circuits. We have created a tool to apply these inversions, and show that it can also be used to verify other compilation methods for QDI circuits. This procedure presents an alternative approach to typical VLSI verification by requiring little designer effort and by reconstructing specifications through transformations.