定点数据通路的等价验证

以有限环代数为理论基础,提出一个定点数据通路的等价验证算法.该算法能有效地对实现多项式运算的寄存器传输级(register transfer level, RTL)定点数据通路进行等价验证.理论分析表明该算法的时间复杂性优于文献中存在的算法;实验结果表明该算法不论是对等价的数据通路的验证还是对含有故障的数据通路的验证均比已有的算法节省CPU时间.     

定点算术数据通路的等价性检验方法

以vanishing多项式理想的极小强Gr-bner基为理论基础,提出一种针对定点算术数据通路的等价性检验方法.通过使用多项式函数建模定点数据通路的设计规范和寄存器传输级实现,将等价性检验问题转化为判断一个多项式函数是否为vanishing多项式、vanishing多项式理想的极小强Gr-bner基被用来有效地解决该问题.理论分析和实验结果表明,与现有的算法相比,该方法在时间消耗上具有一定的优势.     

基于Mining-SEC方法的电路等价性验证

针对时序电路的等价性验证难题,提出基于Mining-SEC的定界等价性验证方法。将待验证时序电路按时间帧展开为多项式符号代数表示的电路集合,利用时间序列数据挖掘方法挖掘其中的不变量和相应的全局约束,不变量可以是任意多项式。此外还可挖掘电路中的不合法约束和复杂的多项式关系,通过以上方法可以明显降低求解空间。使用基于SMT的验证引擎检验电路等价性。实验结果表明,该方法可以快速地实现验证收敛,得到平均1~2个量级的验证加速,并且可以有效消除虚假验证。     

一类并发实时系统的自动验证

一个被广泛用于验证实时系统的方法是根据被验证的实时性质,使用适当的双向模拟等价关系使无限的状态空间转化为有限的状态等价类空间.算法只需要在这个有限的等价类空间里搜索就可以得到正确答案.但是,这个等价类空间的规模一般随着系统规模的增大而产生爆炸性的增长,以至于在很多情况下,穷尽搜索这个空间是不现实的.该文引入了一个等价关系来验证一个由多个实时自动机通过共享变量组成的并发系统是否满足一个线性时段特性.同时,还引入了格局之间的兼容关系来避免对状态等价类空间的穷尽搜索.基于这两个关系,文章提出了一个算法来验证是否一个实时自动机网满足一个线性时段特性.实例研究显示,此算法在某些情况下比其他一些工具有更好的时间和空间效率.     

装备故障样本优化方法研究

测试性验证装备的故障样本往往相互关联,全部注入费用较高、代价较大.为了降低验证试验费用,采用适当方法对故障样本进行优化分析.为提高故障检测率,提出了一种等价样本的故障样本优化方法.方法在分析故障-测试关联矩阵及其扩展、故障模式功能等价集合和故障模式测试等价集合的基础上,构建了故障样本等价集合,并进行重要度特征分析和最大熵求解,确定了最小的故障样本集合.通过对某型试验台故障样本优化实例分析,并与传统的方法进行了试验结果对比分析,使得故障样本数量、试验费用大为减少,提高了测试性验证的经济性.     

一种基于MapReduce的OpenFlow网络属性并行验证算法

针对OpenFlow网络中流表配置错误引起转发回路、路由黑洞和访问控制规则失效等问题,提出一种并行的基于MapReduce的OpenFlow网络属性验证算法。通过在Map阶段划分规则等价类,在Reduce阶段为规则等价类构建基于交换机端口谓词的网络转发图并分析可达性,实现对网络属性的并行验证。同时,通过采用原子谓词将传统可达性分析中的规则匹配域多维集合运算转换为整数集合运算,以进一步提高可达性分析效率。此外,基于原子谓词的谓词表达方式可消除交换机端口谓词集合中的冗余项,降低存储开销。最后,通过理论分析和仿真实验验证了算法的正确性及在时间和存储开销方面的优越性。     

角色工程中一种最小角色集的求解算法

角色工程是基于角色访问控制(Role-Based Access Control,RBAC)中的一个重要研究方向,它主要研究角色的获取与优化。目前已有很多关于角色获取与优化的研究,但这些研究所提出的算法要么复杂度较高(NP完全的),要么不能保证优化的效果是最优的。因此,研究建立了一种新的最小角色集求解算法。该算法的时间复杂度是多项式的,而且可以保证优化效果是最优的。首先通过引入代数方法对数据进行预处理,使用极大线性无关组对角色集合进行化简;然后在分析了集合各个运算符特点的基础上,利用概念格模型建立等价类,并最终获得最小角色集。实验结果表明所提算法是有效的。     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

满秩仿Hermite多项式矩阵的J一谱分解计算

基于仿等价变换实现了满秩仿Hermite多项式矩阵的J-谱分解计算.对于一个满秩的仿Hermite多项式矩阵,首先用仿等价变换将其变换为单模的满秩仿Hermite多项式矩阵,进一步再用仿等价变换将其变换为常数满秩矩阵,最后变换为J-矩阵.将这些变换矩阵积累起来,得到满秩仿Hermite多项式矩阵的J-谱分解.在作者发展的多项式矩阵运算程序库的基础上,给出了实现所提出的计算方法的算法.数例表明,该方法是有效的.     

满秩仿Hermite多项式矩阵的J-谱分解计算

基于仿等价变换实现了满秩仿Hermite多项式矩阵的J-谱分解计算.对于一个满秩的 仿Hermite多项式矩阵,首先用仿等价变换将其变换为单模的满秩仿Hermite多项式矩阵,进 一步再用仿等价变换将其变换为常数满秩矩阵,最后变换为J-矩阵.将这些变换矩阵积累起 来,得到满秩仿Hermite多项式矩阵的J-谱分解.在作者发展的多项式矩阵运算程序库的基础 上,给出了实现所提出的计算方法的算法.数例表明,该方法是有效的.     

高效能ESCA协处理器验证技术研究

处理器结构的日益复杂使得对处理器功能进行有效验证变得越来越重要和关键。基于一款高效能计算协处理器ESCA,讨论了边界值验证、等价类验证和决策表验证等三类验证方法在ESCA处理器功能验证中的具体实现,并针对ESCA处理器中不同功能模块的基本特性提出了一种综合验证方法。实验结果表明,采用综合验证方法进行的ESCA处理器功能验证,不仅高效保证了验证案例集的生成,而且以较少的验证工作量实现了100%功能覆盖率,有效减少了ESCA处理器功能验证时间,提高了验证效率。     

基于逻辑等效模型的快速功能仿真验证

随着集成电路设计技术的发展,集成电路的规模越来越大,这使得在设计的各个阶段设计验证越来越重要,验证耗时的缩短也成为了SOC设计的关键。介绍了基于逻辑等效模型的快速功能仿真验证的方法和技巧,首先研究了验证的策略和方法,然后阐述了采用NC-Verilog进行快速功能仿真验证所使用的逻辑等效模型,最后给出了该方案的仿真结果和结论,证明该技术不仅能达到功能仿真验证的目的,而且有效地缩短了仿真周期,显著地提高了仿真效率。     

基于FPGA的智能卡验证平台设计

随着集成电路设计技术的发展和芯片集成度的提高,验证已经成为芯片设计流程中的主要瓶颈。本文设计了一个基于FPGA的智能卡验证平台,并对验证方法做了详细阐述。本文对于双界面智能卡芯片验证的成功实践,不仅是对FPGA验证理论的证实,而且验证的思路和方法对其他芯片有一定的指导意义。     

RISC指令集众核处理器功能验证与实现

众核技术已成为当前处理器体系结构发展的必然趋势,如何对众核处理器设计进行有效而充分的验证,成为当今IC设计验证领域的研究热点之一,也是众核处理器芯片能否成功流片的关键因素之一。目前工业界采用基于仿真的验证作为主要的验证方式,重点介绍了以覆盖率为导向的RISC众核处理器的功能验证环境的整体设计,提出了“被动式”的验证思想,并采用“软硬件协同验证”的策略,最终达到每条指令都比对通过的验证目标,辅以后期阶段所引入的时序验证策略和功耗评估策略,完整地提出了一套芯片验证平台搭建和验证功能实现的方法流程。     

通用CPU设计验证中的等价性检验方法

针对传统的模拟验证方法需要大量的时间且难以获得完全的覆盖率的局限性,提出了目前应用最广泛的一种形式验证方法——等价性检验在一款通用CPU设计验证中的应用方案,包括寄存器传输级(RTL)设计与门级网表、门级网表与门级网表、RTL设计与RTL设计之间的功能等价性验证．此外,给出了验证过程中一些常见问题的解决办法．验证结果表明了该方法的可行性,显著地减少了门级模拟的时间．     

Partial order reduction for state/event LTL with application to component-interaction automata

Software systems assembled from a large number of autonomous components become an interesting target for formal verification due to the issue of correct interplay in component interaction. State/event LTL (Chaki et al. (2004, 2005) [1] and [2]) incorporates both states and events to express important properties of component-based software systems.The main contribution of this paper is a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.To bring some evidence of the method’s efficiency, we present some of the results obtained by employing the partial order reduction technique within our tool for verification of component-based systems modelled using the formalism of component-interaction automata (Brim et al. (2005) [3]).     

面向SoC的事务级验证研究

随着集成电路的快速发展,一个SoC的规模已经在几百万门至几千万门左右,面对这样高的复杂度,功能验证成为芯片设计中的一个挑战。传统的验证方法已经成为SoC设计的“瓶颈”。基于事务的验证方法成为SoC设计中功能验证最有效的途径之一。文中重点阐述了基于事务验证的相关概念,给出了完成SoC事务验证的一般流程和设计方法,并详细分析了事务验证平台的设计调试和功能覆盖率分析,最后对传统的验证方法和基于事务的验证方法进行了比较,给出了基于事务验证方法的优点。     

时序电路等价性检验中的存储元素映射方法研究

随着集成电路规模越来越大,系统的功能日益复杂,功能验证已成为整个设计流程的瓶颈.对于大规模的时序电路,传统基于状态空间遍历的等价性检验方法可能会遇到内存爆炸问题.为了降低等价性检验方法的复杂度,提高验证效率和处理大规模电路的能力,通常需要构造两个被验证电路的存储元素映射之间的映射关系,从而将时序电路等价性检验问题转化为组合电路等价性检验问题.较全面地介绍了时序电路等价性检验的基本方法及其研究进展,讨论了基于存储元素映射的时序电路等价检验方法的基本思想,并介绍了若干具有代表性的存储元素映射方法,展望了集成电路等价检验方法的研究发展方向.     

Coinductive Verification of Program Optimizations Using Similarity Relations

Formal verification methods have gained increased importance due to their ability to guarantee system correctness and improve reliability. Nevertheless, the question how proofs are to be formalized in theorem provers is far from being trivial, yet very important as one needs to spend much more time on verification if the formalization was not cleverly chosen. In this paper, we develop and compare two different possibilities to express coinductive proofs in the theorem prover Isabelle/HOL. Coinduction is a proof method that allows for the verification of properties of also non-terminating state-transition systems. Since coinduction is not as widely used as other proof techniques as e.g. induction, there are much fewer “recipes” available how to formalize corresponding proofs and there are also fewer proof strategies implemented in theorem provers for coinduction. In this paper, we investigate formalizations for coinductive proofs of properties on state transition sequences. In particular, we compare two different possibilities for their formalization and show their equivalence. The first of these two formalizations captures the mathematical intuition, while the second can be used more easily in a theorem prover. We have formally verified the equivalence of these criteria in Isabelle/HOL, thus establishing a coalgebraic verification framework. To demonstrate that our verification framework is suitable for the verification of compiler optimizations, we have introduced three different, rather simple transformations that capture typical problems in the verification of optimizing compilers, even for non-terminating source programs.     

NC图形验证与仿真技术的研究概况

数控程序图形验证与仿真技术的研究对保证加工质量提高加工效率具有重要意义,同时也是虚拟制造技术的主要研究内容之一,该文从国外NC几何验证、NC物理验证以及我国的NC图形验证三个方面对NC图形验证技术的发展概况作了较全面的论述,并指出其中存在的不足和尚待解决的问题。最后提出一种新的复杂曲面NC图形验证的体系结构。