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

摘要：在数据控制流图(CDFG)结构的基础上,结合模拟验证和模型检测的优点,对需要验证的系统性质进行分类,采用不同的验证方法,提高验证的能力。通过对OVL语言和CTL描述进行改进,针对模拟验证、CDFG图匹配、模型检测3种方法设计相应的性质,实验结果表明这种分治验证策略有助于提高系统验证的效率和规模。

摘要：为了提高芯片设计中功能验证环节的效率,提出了一种对系统的功能特性归类划分、自动选择适合的验证技术的协同验证方法,构建了多种验证技术之间无缝协作的平台。该协同验证方法所依据的策略是:特定的功能特性采用特定的验证技术更有效。因此,利用不同验证技术的互补验证能力,可提高验证效率。协同验证平台的实现是基于从控制数据流图得到的细化模型,该细化模型采用了包括特性分组、变量重排、结构细化等模型优化技术,以提高验证速度。根据在ITC99上的验证,证明了该协同验证方法的有效性和实用性。

摘要：提出一种高效的机器人相平面建模方法 .此方法采用 B样条曲线构成路径 ,依据 B样条曲线参数划分相平面 ,利用运动约束限制建模区域 ,为启发式搜索提供启发信息以加快搜索进程 .

摘要：随着IC技术的发展 ,降低连线拥挤度已经成为一个保证布线成功率的至关重要的因素 提出一种标准单元增量式布局算法C ECOP 该算法通过一个新型的布线估计模型来精确估算布局以后的走线情况 ,利用力驱动的方法进行单元插入和单元推移来消除局部拥挤 ,同时进一步优化线长 来自美国工业界的测试实例表明 ,该算法能够很好地消除走线局部拥挤 ,同时尽量维持原有布局方案的电路性能 。

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

摘要：“行动研究”是当前许多学校所采用的一种科研方法，这种方法对于突显中小学校课题研究的实践性，促使教育科研与学校日常教育工作的融合起到了积极的作用。许多学校结合实际工作设计研究活动，注重实践操作，关注行动的效果，使科研更贴近学校教育实际，贴近教师工作实际。

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

摘要：本文针对甚大规模集成电路的时延驱动布局问题提出了一个新的解决途径 ,其策略是将结群技术应用于二次规划布局过程中 .结群的作用是可大幅度地降低布局部件的数量 .本文设计了一个高效的结群算法CARGO ,其优点是具有全局最优性并且运行速度很快 .采用了一个基于路径的时延驱动二次规划布局算法对结群后的电路完成布局过程 .由于二次规划布局算法能够在很短时间内寻找到全局最优解 ,故本文的算法更有希望彻底解决甚大规模电路的布局问题 .在一组MCMC标准测试电路上对算法进行了测试 。

摘要：A new partitioning methodology is presented to accelerate 130nm and beyond large scale alternating phase shift mask(Alt PSM) design *** method deals with granularity self *** conflicts resolution approaches are described and strategies guaranteeing phase compatible during layout compaction are also *** efficient CAD prototype for dark field Alt PSM based on these algorithms is *** experimental results on several industry layouts show that the tool can successfully cope with the rapid growth of phase conflicts with good quality and satisfy lower resource consumption with different requirements of precision and speedup.