Synthesizing complementary circuits automatically

One of the most difficult jobs in designing communication and multimedia chips, is to design and verify complex complementary circuit pair (E, E^-1), in which circuit E transforms information into a format that is suitable for transmission and storage, while E´s complementary circuit E^-1 recovers this information. In order to ease this job, we propose a novel two-step approach to synthesize complementary circuit E^-1 from E fully automatically. First, we assume that the circuit E satisfies parameterized complementary assumption, which means its input can be recovered from its output under some parameter setting. We check this assumption with SAT solver and find out proper values of these parameters. Second, with parameter values and the SAT instance obtained in the first step, we build the complementary circuit E^-1 with an efficient satisfying assignments enumeration technique that is specially designed for circuits with lots of XOR gates. To illustrate its usefulness and efficiency, we run our algorithm on several complex encoders from industrial projects, including PCIE and 10 G Ethernet, and successfully generate correct complementary circuits for them.