Routability checking for three-dimensional architectures

We present a novel symbolic routability checking approach for three-dimensional interconnect layout. The model considered is a general architecture that can fit into different applications, such as ASIC, multichip modules, field-programmable gate arrays, and reconfigurable computing architectures. The method can incrementally incorporate additional constraints driven by timing, performance, and design. We used the latest satisfiability solver to validate the effectiveness of our approach. The experimental results demonstrate the encouraging performance on difficult routing benchmarks.