Synthesizing Complementary Circuits Automatically
Shengyu Shen, Ying Qin, Ke-fei Wang, Liquan Xiao, Jianmin Zhang, Sikun Li · IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems · 2010
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 circuitE-1recovers this information. In order to facilitate this job, we proposed a novel two-step approach to synthesize the complementary circuitE-1fromEautomatically. First, a SAT solver was used to check whether the input sequence ofEcan be uniquely determined by its output sequence. Second, the complementary circuitE-1was 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.