A halting algorithm to determine the existence of decoder

Complementary synthesis automatically synthesizes the decoder circuit E^-1 of an encoder E. It determines the existence of E^-1 by checking the parameterized complementary condition (P C). However, this algorithm will not halt if E^-1 does not exist. To solve this problem, we propose a novel halting algorithm to check P C in two steps. First, we over-approximate P C with the linear path unique condition (LP), and then falsify LP by searching for a loop-like path. If such a loop is found, then E^-1 does not exist; otherwise, LP can eventually be proved within E´s recurrence diameter. Second, with LP proved above, we construct a list of approximations that forms an onion-ring between PC and LP. The existence of E^-1 can be proved by showing that E belongs to all these rings. To illustrate its usefulness, we have run our algorithm on several complex encoder circuits, including PCIE and 10G Ethernet. Experimental results show that our new algorithm always distinguishes correct Es from incorrect ones and halts properly.