Synthesizing Complementary Circuits Automatically

One of the most difficult jobs in designing communication and multimedia chips is to design and verify the complex complementary circuit pair (E, E^-1), in which circuit E transforms information into a format suitable for transmission and storage, and its complementary circuit E^-1 recovers this information. In order to facilitate this job, we proposed a novel two-step approach to synthesize the complementary circuit E^-1 from E automatically. First, a SAT solver was used to check whether the input sequence of E can be uniquely determined by its output sequence. Second, the complementary circuit E^-1 was built by characterizing its Boolean function, with an efficient all-solution SAT solver based on discovering XOR gates and extracting unsatisfiable cores. To illustrate its usefulness and efficiency, we ran our algorithm on several complex encoders from industrial projects, including PCIE and 10 G Ethernet, and successfully built correct complementary circuits for them.