|
Stephen Longfield and Rajit Manohar
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.
|
|