Theory of safe replacements for sequential circuits

We address the problem of developing suitable criteria for design replaceme nt in the context of sequential logic synthesis. There have been previous e fforts to characterize replacements for such designs. However, all previous attempts either make implicit or explicit assumptions about the design or the environment of the design. For example, it is widespread practice to as sume the existence of a hardware reset line and, consequently, a fixed powe r-up state; in the absence of the same, a common premise is that the design 's environment will apply an initializing sequence. We present the notion o f safe replaceability, which does away with these assumptions, and prove a number of properties that hold of it, Most importantly, we show that the no tion is sound, i.e., if design D-1 is a safe replacement for design D-o, th en no environment can determine if D-1 is used in place of D-o and that the notion is complete, i,e., if D-1 is not a safe replacement for D-o then th ere exists an environment that can detect if D-1 is used in place of D-o, C ompleteness is important for logic synthesis and verification because it sp ecifies the maximum allowable flexibility for replacement. When the design' s output is not used for a certain number of cycles after power up, then sa fe replaceability can be relaxed to obtain what we refer to as delay safe r eplaceability; we analyze properties of this notion too. Since our work, ma ny papers have used this notion effectively for sequential optimization.