摘要：提出一新的验证算法,利用电路拓扑信息选择有效割集,以减小验证规模,并对割集进行无依赖性处理,减少伪错误发生概率,提高验证效率;同时,利用启发式信息选择复杂度较高的节点变量进行量化,进一步减小二叉决策图(BDD)的内存要求.最后用ISCAS’85电路的实验结果证明了该算法的有效性.

摘要：介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间.实验结果表明,该算法是实用有效的.

摘要：为了提高组合电路的等价性验证速度,提出了一种利用电路内部等价信息的新型验证方法.该方法结合了通用割集和专用割集.从原始输出进行回溯得到通用割集,用通用割集验证所有候选等价点(CEP)的等价性.从特定候选等价点进行回溯得到专用割集,通过消除高层次结点间的依赖关系对专用割集进行优化,用专用割集验证特定候选等价点的等价性.实验结果表明,与传统依赖性处理策略相比,该验证方法中的依赖性处理策略减少了验证时间.与只基于通用割集或专用割集的验证方法相比,该方法可以使组合电路的验证速度明显提高.

摘要：提出基于CK810处理器的16/32位混编指令集汇编链接时优化技术。利用汇编输出二进制文件,根据CK810处理器的16/32位混编指令集中指令及操作数的特征,动态选择指令的编码方式,实现对指令relax,最大程度地提高了程序的代码密度。对于在汇编时不能确定编码方式的指令,通过留出重定位的方式,由链接时完成优化。在链接时,利用信息的确定性,实现对整个程序的压缩和指令的替换,使得程序执行效率更高,代码占用空间更小。汇编链接时优化技术克服了传统编译器只限于一个模块优化的缺点,把优化范围扩展到整个程序,实现了跨模块的优化,使得基于CK810处理器的程序代码密度平均提高7.52%,性能平均提升7.91%。

摘要：本文描述了一个基于等价性验证的逻辑综合引擎,它实现了从RTL级到网表级的综合。设计验证系统的初衷是验证给定设计从RTL级到网表级自动综合后电路的正确性,所以综合引擎本身的正确性是本文首要关注的问题。为了提高等价性验证引擎的工作效率,本文还提出并实现了一系列保持电路相似性的方法。最后,本文以SYNOPSYS的等价性验证工具FORMALITY作为比较,试验结果表明本系统是有效的。

摘要：猜测并行化编译,即线程级猜测(TLS)编译,可将原来顺序运行的程序并行化。但由于猜测数据的不确定性引起的数据管理开销过大,以及猜测线程失败引起的线程回滚开销,使得并行后的执行性能较低。针对上述问题,提出一种HL-TLS并行化编译优化框架。HL-TLS能有效地标记并行化的循环体为热点循环体,采用对最高层次热点循环体进行更激进的并行化的方式提高性能,而对非热点循环体采用保守的顺序执行以减少开销。实验结果表明,使用HL-TLS编译优化框架,实验程序的执行效率可以提高20%。

摘要：随着近年来高效SAT(Satisfiability)求解算法提出,SAT已成为集成电路形式验证方法中重要引擎之一。但在运用SAT验证时需将电路结构转化为成OR-AND两级逻辑描述,丢失了电路的拓扑信息。本文利用改善的静态隐含策略来提取有用子句作为预处理,来加快验证过程。本文算法在原有静态隐含技术的基础上,引入了关联节点隐含及隐含过程加速策略。给出的ISCAS85电路的实验结果表明算法的有效性。

摘要：割集在组合电路等价性验证中得到了广泛的应用,已有的方法常构造能将整个电路一分为二的割集,虽然这种割集在验证后续节点时可以重用已构建的BDD,但它的排序对大多数后续节点都很差,容易引起内存爆炸问题。本文中的割集只针对要验证等价性的某一对点,避免了上述问题。ISCAS85的实验结果表明了它的有效性。

摘要：在实时图像处理系统中,为了在规定的时间内实现大量的运算处理,需要采取提高运算速度的措施。应用MPC5200为核心的高性能运算处理器,在对目标检测识别算法的实验分析基础上,开发了实时图像处理软件,实现了视频图像的采集和图像目标的实时处理。