基于线性规划的RTL可满足性求解和性质检验

采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题．深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法．通过将RTL性质转化为虚拟RTL电路,找到了一种验证RTL性质的方法．通过实验,并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较,证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势．     

RTL验证中的混合可满足性求解

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.     

一种基于混合仿真技术的电路并行后仿真加速算法

随着集成电路制造工艺的发展,芯片的特征尺寸不断地缩小,寄生电阻和电容对电路性能的影响也变得越来越显著,电路后仿真成为集成电路设计验证不可缺少的关键技术.但是集成电路规模的不断增大,寄生电阻和电容的数目急剧膨胀,电路后仿真中求解线性方程组所需要的时间急剧增加,导致电路验证时间越来越长,影响集成电路的设计周期和产品交付时间.文中利用超图划分的方法将电路划分成若干个相互耦合的子模块,子模块的矩阵求解应用LU分解方法,顶层矩阵求解利用GMRES方法;针对GMRES方法收敛速度慢的问题,根据快节点和电源网格节点本身的物理特性提出一种预处理算法,能够显著加速线性方程组的求解速度,从而提升电路的仿真效率.该算法已经应用到华大九天的电路仿真工具ALPS中,通过大量工业实际用例的测试,证明了算法的有效性.     

一种基于点割的电路划分算法

文中提出了一种基于IG图(Intersection Graph)点割的电路划分算法,引入IG图模型,根据电路中信号网络间的交互关系构建IG图,直接对电路信号网络IG图进行最小点割划分,从而实现对电路单元(模块)的划分.该算法既有效地解决了电路超图与图之间转换的一致性问题,又实现了点割目标值与直接电路划分目标值的一致性,IG图点割集的大小即为真实电路划分的目标值.此外,通过给每个电路网络赋权重的方式构建带权重网络交互图,实现对电路网络划分的面积平衡进行近似控制,满足电路划分对面积平衡的特殊要求.采用MCNC提供的标准电路测试数据进行测试,实验结果表明,基于IG图点割的电路划分算法较基于网络超图HDN划分的K-DualFM算法平均有3%~7.8%的提高;同时,基于IG图点割的随机优化算法ROP比基于超图划分的FM优化算法具有更强的全局优化能力,划分结果提高18%,比基于二部图匹配的点割优化算法提高36%,对较大规模数据划分优化效果更好.     

在形式验证和ATPG中的布尔可满足性问题

介绍布尔可满足性(SAT)求解程序在测试向量自动生成、符号模型检查、组合等价性检查和RTL电路设计验证等电子设计自动化领域中的应用．着重阐述如何在算法中有机地结合电路拓扑结构及其与特定应用相关的信息，以便提高问题求解效率．最后给出下一步可能的研究方向。     

基于再聚类和离散优化的k路划分算法

为了寻得集成电路更优的k路划分,提出将再聚类和离散优化应用于k路划分算法.首先利用再聚类缩小超图规模,即根据给定划分计算顶点间的评级函数值,依据取值大小进行顶点聚类;然后将超图转换为星型图,并将k路划分问题转换为无约束的离散优化问题;进而设计一个算法迭代移动增益值最大的顶点,在算法求解过程中放宽平衡约束,允许暂时处于不可行域的解,扩大问题的求解空间.在同一平台上使用ISPD98电路测试基准对所提算法、hMETIS-Kway和KaHyPar-K进行测试,并比较最小割值和运行时间.实验结果表明该算法优于hMETIS-Kway,特别是在k=2时,最小割值减少了0.173,速度提升了0.706.此外,该算法对KaHyPar-K也有相应的改进效果.     

基于SMT求解器的微处理器指令验证数据约束生成技术

处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory, SMT)的指令约束求解方法：利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法：首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益.     

SMT求解技术的发展及最新应用研究综述

可满足性模理论(satisfiability modulo theories, SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.     

RTL数据通路模拟矢量自动生成方法研究与实现

针对已有的RTL数据通路模拟矢量自动生成方法的不足,提出一种利用约束逻辑编辑(CLP)自动生成数据通路模拟矢量的新方法．该方法首先对给定的Verilog RTL描述采用程序切片进行设计化简,然后对化简后的结果基于位向量算术原理生成CLP约束,并利用CLP求解器GProlog进行约束求解,最终生成满足输出要求的模拟矢量．该方法约束求解速度快,生成的约束是统一的,得到的模拟矢量较完备,能满足模拟验证的要求．实验结果表明,文中方法是一种高效的RTL数据通路模拟矢量自动生成方法．     

采用二元CSP引擎求解RTL数据通路的可满足性

针对寄存器传输级(RTL)验证和测试过程中非常重要的数据通路可满足性求解问题,提出一种基于二元约束满足问题(CSP)的求解方法,包括数据通路提取、二元CSP建模和搜索求解3个步骤.数据通路提取通过对接口布尔变量和某些字变量赋值,为各个数据通路器件建立环境;二元CSP建模则根据该环境和各个数据通路器件的功能,将数据通路的可满足性问题转化为二元CSP描述;该二元CSP问题的描述被送入到二元CSP引擎,并采用冲突引导的回跳搜索策略进行求解,获得有解的例证或无解的判定.实验结果表明,即使在没有采取很多优化策略的条件下,该方法仍有较好的性能,并优于基于线性规划(LP)的求解方法.     

Hypergraph-partitioning-based decomposition for parallelsparse-matrix vector multiplication

In this work, we show that the standard graph-partitioning-based decomposition of sparse matrices does not reflect the actual communication volume requirement for parallel matrix-vector multiplication. We propose two computational hypergraph models which avoid this crucial deficiency of the graph model. The proposed models reduce the decomposition problem to the well-known hypergraph partitioning problem. The recently proposed successful multilevel framework is exploited to develop a multilevel hypergraph partitioning tool PaToH for the experimental verification of our proposed hypergraph models. Experimental results on a wide range of realistic sparse test matrices confirm the validity of the proposed hypergraph models. In the decomposition of the test matrices, the hypergraph models using PaToH and hMeTiS result in up to 63 percent less communication volume (30 to 38 percent less on the average) than the graph model using MeTiS, while PaToH is only 1.3-2.3 times slower than MeTiS on the average     

硬件加速功能验证问题的DAG划分算法

功能验证是超大规模集成电路(very large scale integration, VLSI)设计的一个基本环节. 随着超大规模电路的普及与发展, 在单处理器上对整个电路进行功能验证在可行性和效率上都存在较大的缺陷. 基于硬件加速器的功能验证是将整个电路划分成若干个规模更小的子电路; 然后在多个硬件处理器上并行的执行功能验证. 当电路划分结果的并行性较优时可提高功能验证的效率, 缩短时间周期. 类似电路设计中的其他划分问题, 用于硬件加速功能验证的电路划分问题可以被抽象成图划分问题. 相较于传统图划分问题, 硬件加速功能验证的划分问题还需要保证较小的模拟深度和较高的调度并行性. 为了满足硬件加速功能验证的划分需求, 提出了一种基于传统多级图划分策略的有效算法. 该算法结合调度思想, 利用电路的关键路径信息和时序信息, 将硬件加速功能验证问题转化为有向无环图的多级划分问题. 随机电路网表数据的实验结果表明, 所构造的算法可以有效的减少关键路径长度并且不会引起切边数的增长恶化.     

用于RTL设计验证的静态错误检测方法

为快速有效地对集成电路设计中潜在的常见错误进行检测,提出一种基于静态分析的错误检测方法。该方法可以自动地提取待测寄存器传输级(RTL)设计的行为信息,检测出设计中常见的错误,如状态机死锁、管脚配置错误。实验结果表明,静态检测相对于其他验证方法自动化程度高、检测速度快、检测准确度高、检测代码可重用,可以在模拟之前发现设计中的错误。     

基于软件模拟的SoC功能验证技术研究进展

软件模拟验证在SoC设计中得到了广泛的研究和应用,是目前SoC功能验证的主要方法.文中从高度抽象化、可重用和自动化三个方面梳理和综述了基于软件模拟的SoC功能验证技术的研究进展.同时,基于断言的验证在SoC的功能验证技术中起到重要的辅助性作用,文中阐述了断言技术的研究进展.最后,对软件模拟验证技术的发展趋势进行了展望.     

一种SOC原型机的建立与IP模块验证

SOC（System On Chip）将原来分立器件实现的CPUs、DSPs和存储器等模块整合在一个单芯片内,这种设计方法使得外围的IP模块的复用变得非常重要.而复用的IP模块必须嵌入到SOC中进行系统验证后才能使用,系统功能验证通常使用原型机的验证方法.该文论述了汉芯SOC的FPGA原型机验证环境的实现方法,以及如何使用串口建立起PC机与原型机的通讯.原型机验证中的一个普遍问题是ASIC设计代码不能直接映射到FPGA,否则会造成FPGA实现的硬件效率低,甚至时序不能满足从而导致验证失败,该文以门控时钟为例,对这种代码的转换提出一种可行的方法,并对转换前后的性能做了对比.最后,以一个常用的IP模块为例,对复用IP模块的系统原型机实时验证进行技术研究与探讨.     

面向soc芯片的跨时钟域设计和验证

随着高性能、低功耗芯片的发展,多时钟域和跨时钟域(Clock Domain Crossing, CDC)设计越来越多,CDC设计和验证越来越重要。阐述了5种常用的同步器设计模板。验证方法提出了层次化的验证流程:结构化检查,基于断言的验证(assertion-based verification, ABV),对关键模块进行形式化验证。CI)C设计应用于研发的一款65nm工艺SOC芯片(最高主频1GHz,10个时钟域设计、多种工作模式),该芯片已流片回来。经测试,芯片的功能正确,说明设计和验证方法是完备的。     

事务级形式验证技术及8051验证模型

提出一种基于事务的用于电路系统的形式验证方法(TBFV)．应用该方法，验证工程师可以在行为级对系统进行验证，无需了解设计的细节．为了对该方法进行示范，验证了8051的RTL级实现，并给出了8051指令集的TBFV模型．     

基于属性分布相似度的超图高维聚类算法研究

在许多聚类应用中,数据对象是具有高维、稀疏、二元的特征。传统聚类算法无法有效地处理此类数据。该文提出一种基于超图模型的高维聚类算法,通过定义对象属性分布特征向量和对象间属性分布相似度,建立超图模型,并应用超图分割法进行聚类。聚类结果通过簇内奇异特征值进行评价。实验结果和算法分析表明,该算法可以有效地进行聚类知识挖掘。     

Clustering ensemble via structured hypergraph learning

Clustering ensemble integrates multiple base clustering results to obtain a consensus result and thus improves the stability and robustness of the single clustering method. Since it is natural to use a hypergraph to represent the multiple base clustering results, where instances are represented by nodes and base clusters are represented by hyperedges, some hypergraph based clustering ensemble methods are proposed. Conventional hypergraph based methods obtain the final consensus result by partitioning a pre-defined static hypergraph. However, since base clusters may be imperfect due to the unreliability of base clustering methods, the pre-defined hypergraph constructed from the base clusters is also unreliable. Therefore, directly obtaining the final clustering result by partitioning the unreliable hypergraph is inappropriate. To tackle this problem, in this paper, we propose a clustering ensemble method via structured hypergraph learning, i.e., instead of being constructed directly, the hypergraph is dynamically learned from base results, which will be more reliable. Moreover, when dynamically learning the hypergraph, we enforce it to have a clear clustering structure, which will be more appropriate for clustering tasks, and thus we do not need to perform any uncertain postprocessing, such as hypergraph partitioning. Extensive experiments show that, our method not only performs better than the conventional hypergraph based ensemble methods, but also outperforms the state-of-the-art clustering ensemble methods.