面向通讯应用的自动对偶综合方法研究

通讯应用是半导体工业的主要推动力之一。在通讯芯片设计项目中，耗时最长且最容易出错的工作，在于设计和验证通讯协议栈的对偶电路。本项目的目标在于，在我们发表于ICCAD'09的初步研究成果基础上，提出全新的理论框架，以自动产生对偶电路的寄存器传输级(RTL)代码，从而提升通讯芯片的设计质量，并缩短设计周期。为达到上述目标，将从以下方面开展研究：首先，通过引进可满足性模(SMT)方法，提升算法抽象层次，以降低算法时间开销，并提升结果可读性；其次，提出弱化的"最终唯一"概念，以支持对多参数组复杂电路进行对偶综合；再次，提出基于时态变量划分的解枚举算法，以改善对偶电路的时序和面积；最后，提出面向冗余数据流的对偶综合算法，以提高对偶电路的可靠性。本项目提出的理论框架和实现技术，能极大的提升通讯芯片的设计效率和质量，具有重大的学术价值和应用前景。

在本项目执行期间，获得了以下主要研究成果。..1、在我们发表于ICCAD09的原始对偶综合算法基础上，增加对环形路径条件的检测公式，将解码器在有限长度上不存在的结论，扩展到无限长路径上，从而解决了原始算法不停机的问题。研究成果发表于IEEE Transaction on CAD of Integrated Circuits and Systems(TCAD),2011年第10期。..2、提出了自动推导外部断言的算法，以减少用户手工工作。该算法迭代的运行成果1的算法，使用每次迭代中产生的SAT公式，求解并剔除解码器不存在的外部断言。有限状态假设保证了该算法的停机性。研究成果发表于International Conference on Computer Aided Design(ICCAD11)。...3、提出了全新算法以发掘多个同时存在的解码器及其对应断言。该算法迭代的构造函数依赖问题的SAT公式，以检查当现有已发掘的解码器集合具有相同的输出时，是否能够导致所有潜在解码器的混合SAT公式具有不同的输出。若是，则表明仍然存在尚未被发掘的解码器，而混合SAT公式在外部配置信号集合的解上的投影，即为新的解码器的迁移关系。该算法迭代运行直至函数依赖问题的SAT公式不可满足为止。研究成果发表于IEEE Transaction on CAD of Integrated Circuits and Systems(TCAD),2012年第8期。...4、提出基于Craig插值的特征化算法，以加快生成解码器的速度。该算法构造迁移关系的不可满足SAT公式，并从SAT求解器产生的resolution序列中产生解码器的布尔函数。该算法也发表于IEEE Transaction on CAD of Integrated Circuits and Systems(TCAD),2012年第8期。..5、由于本小组的开创性工作，使得对偶综合引起了国际学术界的关注和跟进研究。自2011年以来，在EDA领域的顶级会议ICCAD[4]和DAC[6]，以及顶级期刊IEEE Transaction on CAD of Integrated Circuits and Systems[5]上共发表了3篇来自其他研究小组的论文。这些工作给出了意想不到的发现，是对我们研究工作的巨大推进和有益补冲。