Synthesis and verification of cyclic combinational circuits
Synthesis and verification of cyclic combinational circuits
复制标题
循环组合电路的综合与验证
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Chun
中科院分区：
文献类型：
--
作者：
Jui;Yung;Wan;Ching;Chun
先前的工作已经证明了通过在合成期间引入组合回路来实现更小化的组合电路的机会。然而，他们通过使用分支定界技术来探索电路的可能循环依赖性来实现这一点，这可能无法很好地扩展复杂的设计。本文提出了一种基于逻辑蕴涵的形式化算法来直接识别可循环结构候选，或在电路中主动创建可循环结构候选。此外，我们还提出了一个基于SAT的算法来验证所形成的循环是否是组合的。在一组IWLS 2005基准上进行的实验结果证明了识别和验证算法的有效性和可扩展性。与最先进的算法相比，我们的验证算法产生了2到2350倍的加速比。
Prior works have demonstrated opportunities for achieving more minimized combinational circuits by introducing combinational loops during the synthesis. However, they achieved this by using a branch-and-bound technique to explore possible cyclic dependencies of circuits, which may not scale well for complex designs. Instead of using exploration, this paper proposes a formal algorithm using logic implication to identify cyclifiable structure candidates directly, or to create them aggressively in circuits. Additionally, we also propose a SAT-based algorithm to validate whether the formed loops are combinational or not. The effectiveness and scalability of the identification and validation algorithms are demonstrated in the experimental results performed on a set of IWLS 2005 benchmarks. As compared to the state-of-the-art algorithm, our validation algorithm produces speedups ranging from 2 to 2350 times.