How to prove the completeness of a set of register level design transformations

The VLSI design transformations used in the kernel of any interactive design exploration tool should be correct and should, preferably, form a complete set. Completeness guarantees that any correct design for the given specification can be produced using the tool. A method of proving completeness of register level design transformations is discussed. Using this method, it is shown that a set of transformations is complete for a class of register level designs, called the single architectural register transfer (SART) designs