SAT-based synthesis of clock gating functions using 3-valued abstraction
SAT-based synthesis of clock gating functions using 3-valued abstraction
复制标题
使用 3 值抽象的基于 SAT 的时钟门控函数综合
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
K. Yorav
中科院分区：
文献类型：
--
作者：
Eli Arbel;Oleg Rokhlenko;K. Yorav
时钟门控是数字电路的一种降低功耗的技术，其工作原理是消除部分时钟网络的不必要切换，而时钟网络是硬件设计中的一个耗电组件。一种有效的时钟门控综合方法是基于使用BDDS的设计的功能分析。这种类型的算法试图为时钟门控电路建立BDD，然后以近似值减小其大小。如果特定锁存器的BDD变得太大，则对该锁存器进行选通的尝试被中止。我们用基于SAT的技术和三值抽象相结合来取代BDDS。我们的技术直接从电路产生近似，从而避免了爆炸。此外，我们的技术是递增的，因为如果超过时间或内存限制，它会产生部分结果(较弱的近似)。我们的实验表明，使用基于BDD的方法无法选通的锁存器中，超过70%的锁存器是通过基于SAT的方法选通的。
Clock gating is a power reduction technique for digital circuits that works by eliminating unnecessary switching of parts of the clock network, a power-hungry component in hardware designs. An effective approach to clock gating synthesis is based on a functional analysis of the design using BDDs. Algorithms of this type attempt to build a BDD for a clock gating circuit and then reduce its size with an approximation. If the BDD of a particular latch grows too large the attempt to gate that latch is aborted. We replace BDDs with a SAT-based technique combined with 3-valued abstraction. Our technique generates the approximation directly from the circuit, and thus avoids the explosion. Furthermore, our technique is incremental in the sense that it produces a partial result (a weaker approximation) if time or memory limits are exceeded. Our experimentation shows that more than 70% of latches that could not be gated using the BDD-based approach were gated by the SAT-based method.