High speed layout synthesis for minimum-width CMOS logic cells via Boolean satisfiability

We propose a cell layout synthesis method via Boolean satisfiability (SAT). Cell layout synthesis problems are first transformed into SAT problems by our formulations. Our method realizes the high-speed layout synthesis for CMOS logic cells and guarantees to generate the minimum width cells with routability under our layout styles. It considers complementary P-/N-MOSFETs individually during transistor placement, and can generate smaller width layout compared with pairing the complementary P-/N-MOSFETs case. To demonstrate the effectiveness of our SAT-based cell synthesis, we present experimental results which compare it with the 0-1 ILP-based transistor placement method and the commercial cell generation tool. The experimental results show that our SAT-based method can generate minimum width placements in much shorter run time than the 0-1 ILP-based transistor placement method, and can generate the cell layouts of 32 static dual CMOS logic circuits in 54 % run time with only 3 % area increase compared with the commercial tool.