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

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

改进的时间帧展开的时序电路等价验证算法

提出一种改进的基于时间帧展开的时序电路等价验证算法，其来源于模型检查中的基于数学归纳的验证算法，在使用并简化了SAT问题中不可满足子集提取过程后，将基本条件检查和归纳检查合并处理．为了能在时间帧展开过程中减少状态搜索空间，利用结构不动点技术并提出了准动态唯一状态约束等改进的方法．实验表明，随着时间帧的不断展开，文中算法运行时间的增长速度明显慢于基于数学归纳法的验证算法，其适合验证经过时序优化后的电路．     

基于状态转换图同构求解的等价性验证算法

文中提出了一种基于状态转换图同构求解的时序电路等价性验证算法.算法将两时序电路的等价性问题转化为验证相应状态转换图的同构性.首先将初始状态对匹配为待验证对,然后采用递归的方法验证以初始状态对的下一状态对为初始状态的子状态转换图是否同构,从而得到时序电路是否等价的信息.若两状态转换图同构,则两图中的状态均可--配对为待验证状态对,即所有的代验证状态对均为等价状态对.该方法可以有效地克服算法级描述到底层实现之间跨度太大的问题.     

三维几何约束系统的等价性分析

针对过约束、完整约束和欠约束三维几何约束系统的求解问题,提出了等价性分析方法.该方法基于三维几何约束系统的内在等价性,充分挖掘几何领域知识,依据拆解约束闭环、缩减约束闭环和析出约束闭环等原则,采用等价约束替换来处理几何约束闭环问题,优化几何约束图的结构,实现几何约束系统的优化分解.最后用多个实例验证了该方法的正确性和有...     

利用状态缓存的时序等价性验证算法

为了提高时序电路的等价性验证速度,提出一种改进的基于寄存器匹配的验证算法.除了利用原像计算避免误判之外,该算法还将可达状态和不可达状态引入到验证过程中.将仿真过程中从初始状态可以到达的状态记录为可达状态,将验证过程中确认不能从初始状态到达的状态记录为不可达状态,利用它们减少验证过程中的原像计算.基于mcnc91电路的实验数据表明,该算法有效地减少了验证时间.     

基于电路拓扑结构分析的等价性验证方法

随着集成电路设计规模的日益增大,结合多种推理引擎已成为组合电路形式化等价性验证的重要手段.提出一种基于电路拓扑结构分析的组合等价性验证方法,将电路的拓扑结构与验证算法的复杂性关联起来.在验证过程开始之前,利用min-cut方法计算表征电路复杂性的"电路宽度",以确定最佳的推理引擎,避免了传统的引擎切换过程,提高了算法的效率.针对ISCAS85电路的实验结果表明了该方法的效率和可行性.     

基于多项式符号代数方法的高层次数据通路的等价验证

基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求.由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法.深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式.从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Gr(o)bner基计算的有效代数求解算法.针对不同基准数据通路的实验结果表明了该算法的有效性.     

基于虚拟可重构平台的时序电路演化设计

目前,电路进化设计是演化硬件研究的主要方向之一。而时序电路由于存在反馈环不便于进行电路描述和软件仿真。文中对时序电路的演化设计方法进行了改进,提出了专门针对时序电路演化的虚拟可重构平台,建立起电路编码与HDL代码的映射关系。应用TEXTIO和MATLAB来辅助仿真测试过程,使测试向量数量巨大、难以处理的问题得到很好地解决。最后调用ModelSim完成了FSM的演化实验。实验结果验证了基于此平台演化时序电路的可行性和有效性。     

使用输出分组和电路可满足性的等价性验证算法

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

Petri 网的步问题研究

在基于Petri 网的模型验证方法中,步被广泛用于减少变迁实施产生的语义交织.为了研究基于步的构造算法的计算复杂性,提出步的判定问题,并证明该问题是NP 完全的.进一步给出了极大步问题的多项式时间算法和最大步问题的NP 等价性证明.最后分析两类特殊子问题是P 问题.     

延迟时间Petri网的验证分析

延迟时间Petri网（Delay Time Petri Nets，DTPN）是一类重要的时间扩展Petri网系统，解决了其他时间扩展Petri网（如时间Petri网）在保存时间约束时所面临的困难。可调度验证的目的是验证工作流模型时间约束的合理性，对流程实例的时间可达性进行仿真。提出一种基于DTPN的时间约束工作流验证分析方法。给出了DTPN的相关定义，并结合工作流控制结构描述了变迁可触发的时间条件；提出了DTPN触发点的概念以及基于此的验证分析算法；简要分析了DTPN的特性。DTPN的研究丰富完善了现有时间Petri网体系，具有积极的意义。     

Quantifier-free encoding of invariants for hybrid systems

Hybrid systems are a clean modeling framework for embedded systems, which feature integrated discrete and continuous dynamics. A well-known source of complexity comes from the time invariants, which represent an implicit quantification of a constraint over all time points of a continuous transition. Emerging techniques based on Satisfiability Modulo Theory (SMT) have been found promising for the verification and validation of hybrid systems because they combine discrete reasoning with solvers for first-order theories. However, these techniques are efficient for quantifier-free theories and the current approaches have so far either ignored time invariants or have been limited to hybrid systems with linear constraints. In this paper, we propose a new method that encodes a class of hybrid systems into transition systems with quantifier-free formulas. The method does not rely on expensive quantifier elimination procedures. Rather, it exploits the sequential nature of the transition system to split the continuous evolution enforcing the invariants on the discrete time points. This way, we can encode all hybrid systems whose invariants can be expressed in terms of polynomial constraints. This pushes the application of SMT-based techniques beyond the standard linear case.     

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

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

基于双线性对的可公开验证多秘密共享方案

现有可公开验证多秘密共享方案只能由Lagrange插值多项式构造,且共享的秘密仅限于有限域或加法群。为解决上述问题,提出一个基于双线性对的可公开验证多秘密共享方案。该方案中每个参与者需持有2个秘密份额来重构多个秘密,并且在秘密分发的同时生成验证信息。任何人都可以通过公开的验证信息对秘密份额的有效性进行验证,及时检测分发者和参与者的欺骗行为。在秘密重构阶段采用Hermite插值定理重构秘密多项式,并结合双线性运算重构秘密。分析结果表明,在双线性Diffie-Hellman问题假设下,该方案能抵抗内外部攻击,具有较高的安全性。     

高速RS编译码器的设计及其FPGA实现

在分析RS（Reed-Solomon）码编译码基本原理的基础上,对编码过程中的乘法电路实现进行了深入分析,对译码过程中用于错误位置多项式和错误值多项式计算的BM（Berlekamp-Massey）迭代算法进行改进,并设计了适合于FPGA硬件实现的伴随式计算策略和钱搜索电路。硬件实现结果表明,改进算法能有效节省硬件资源,在Xilinx公司的XC4VSX35 FPGA上仅需要总资源的15%就可以实现（31,15）RS码编译码器电路,且在200 MHz系统时钟频率时达到10 Mb/s的译码速率,实现了高速数据处理。     

基于她分解与多项式的无线传感器网络密钥算法

提出了基于QR分解与二元多项式的密钥建立与分配方案。该方案以二元多项式的计算结果作为无线传感器网络的密钥。二元多项式的其中一个参数由对称矩阵进行QR分解生成,节点部署后交换Q矩阵的行信息再与R矩阵的列信息相乘生成多项式的参数。多项式的另一个参数由各自生成的随机数确定。分析结果表明：该方案可以提高存储效率、网络连通性、抗捕获性能,并能提供额外的通信链路验证。     

一种可测性分析的新方法

提出一种基于时序泰勒展开图（TTED）的VLSI高层可测性分析（TA）新方法,以时序泰勒展开图（TTED）为关键敏化路径建模,建立起确定性和概率性故障的统一表示模型。利用符号变量获取线路的敏感性,并且考虑电路的单敏化和多敏化情况,进行电路的可测性计算和分析,取得了较好的效果,实验证实了该方法的有效性。     

基于扰动属性投影的说话人确认系统?

在说话人确认系统中,由于训练和测试语音来自不同的信道,会产生信道失配现象。为此,提出一种基于扰动属性投影的说话人确认系统。利用有信道标注信息的语音训练出高维空间映射矩阵,通过映射将自适应得到的超矢量作为SVM的输入,削弱说话人特征中的信道信息。实验结果表明,该系统能降低信道失配带来的负面影响。     

基于SPEA2+算法的Web服务选择研究

服务选择算法是影响组合服务的QoS和服务组合性能高低的关键因素。针对将多维QoS属性加权聚合为一个目标函数进行优化的选择算法不能实质性地解决基于QoS的Web服务选择问题,采用改进的强度Pareto进化算法（SPEA2+）多目标优化求解该问题,设计了一种Web服务选择算法。该算法在满足声誉、可靠性和可利用性属性的约束下,同时最小化服务时间T和服务费用C,以产生Pareto最优解集。通过与运用SPEA2算法求解该问题的实验对比,表明了两算法所获取的Pareto最优解集中QoS属性T和C各均值各有优劣,用户可依据对T或C的偏好择优选择。