An Investigation of Boolean Approaches to Physical Design Problems

布尔可满足性问题（SAT）是设计自动化领域中许多计算任务的核心。虽然SAT是NP完全类的第一个成员，但最近在搜索修剪算法方面的进展已经产生了一系列强大的SAT求解器，能够处理涉及数万个变量和数百万个约束的问题。该项目正在探索特别有效的GRASP SAT引擎的应用，以精确建模和解决一类传统上一直受到攻击的物理设计问题。具体而言，利用该赠款开展的研究活动包括：1）现场可编程门阵列（FPGA）的布局优化，包括建模信号路径布线模式、建模和施加时序要求以及在不可布线的情况下快速确定和提取有用的诊断信息的方法，以及2）通过在晶体管微布局期间更好地估计布线面积来定制质量的晶体管级单元合成，布局和布线的灵活性，以及在布局和布线中更多自由度的探索。本项目开发的详细FPGA布线工具正在广泛分发。

The Boolean Satisfiability problem (SAT) lies at the core of manycomputational tasks in the field of design automation. While SAT has thedistinction of being the first member of the NP-complete class, recentadvances in search pruning algorithms have yielded a crop of powerful SATsolvers capable of tackling problems involving tens of thousands ofvariables and millions of constraints. This project is exploring theapplication of the particularly effective GRASP SAT engine to exactly modeland solve a class of physical design problems that have traditionally beenattacked heuristically. Specifically, research activities being carried outunder this grant include: 1) layout optimization of field-programmable gatearrays (FPGAs) including ways for modeling signal path route patterns,modeling and imposition of timing requirements, and quick determination anddistillation of useful diagnostic information in cases of unroutability,and 2) custom-quality transistor-level cell synthesis through betterestimation of routing area during transistor micro-placement, simultaneousplacement and routing, and exploration of more degrees of freedom in bothplacement and routing. A detailed FPGA routing tool developed in thisproject is being widely distributed.