An Investigation of Boolean Approaches to Physical Design Problems

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

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.