QQ客服 官方微博 反馈留言

题名	数字系统模型检验研究
作者	王明全
学位类别	博士
答辩日期	2007-05-29
授予单位	中国科学院沈阳自动化研究所
授予地点	沈阳自动化研究所
导师	于海斌 ; 王宏
关键词	形式化验证 模型检验 抽象精炼 BDD 优化
其他题名	Research of Digital System Model Checking
学位专业	机械电子工程
中文摘要	模型检验在芯片工业界已经成为一种广泛认可的自动化的数字系统形式化验证工具，它可以明确地证明所设计的数字系统是否满足设计规范要求。尽管近年来模型检验获得了长足的发展，但是在处理容量方面还存在着进一步推广应用的巨大障碍——受困于状态爆炸问题，目前已有的模型检验工具还不能直接验证大部分的工业级数字系统设计。抽象精炼是一种通过迭代计算获得简化的抽象模型来帮助验证原始模型的算法，是目前解决模型检验处理容量问题最好的办法。BDD能够简洁有效地表示数字系统模型和时态逻辑公式，可以从化简抽象模型结构表示的角度来降低模型的复杂度，减小抽象模型BDD的规模是另外一种减轻模型检验状态爆炸问题的解决手段。本文针对模型检验所面临的状态爆炸问题提出了一种新的精细抽象方法以及基于此方法的二阶抽象精炼算法，用来获得最优或者近似最优的抽象模型，提高模型检验算法的处理容量和效率。此外，本文还提出了一种新的基于遗传禁忌混合策略的BDD优化算法，用来有效地降低抽象模型的BDD规模。 精细抽象方法是通过采用比其它抽象方法更小的抽象粒度，在抽象过程中仅仅将那些特性验证必需的电路元素——状态变量和中间组合变量添加到抽象模型中去，而不是将状态变量连同它所有的扇入组合逻辑一同添加到抽象模型中去。这种抽象方法在验证具有复杂组合逻辑的系统具有优势。基于精细抽象方法，本文提出的二阶抽象精炼算法可以利用K-可控性计算和K-协作性计算分别搜索用于模型精炼的状态和状态转移关系，迭代地依次分别对状态变量和中间组合变量进行抽象精炼。同其它已有的抽象精炼算法相比，这种算法可以提供给出更简洁的抽象模型用于特性模型检验，而消耗的运行时间却更少。在二阶抽象精炼算法中采用了最小固定点MBM机制来约束不可见变量的随意赋值，用来减少迭代过程中出现的伪反例的数量，以便提高计算效率。算法实验分析显示基于精细抽象方法的二阶抽象精炼算法同其它已有的抽象精炼算法相比能够获得较简的抽象模型，提高了模型检验工具处理大规模电路系统的能力。 基于遗传禁忌混合搜索策略的BDD优化算法将遗传算法的全局搜索能力同禁忌搜索的局部邻域搜索能力相结合来搜索最优的BDD状态排序，来获得最优的BDD结构。算法的架构分为两层，首先应用禁忌搜索给出所有最有希望的BDD变量候选排序，然后对这些候选排序进行遗传进化进而获得最优或者近似最优的BDD变量排序。算法中采用了相邻变量互换操作通过均匀分布随机地在解空间内生成邻域解，提高了邻域搜索的性能。算法实验分析显示这种混合了禁忌和遗传策略的BDD优化算法同其它已有的BDD优化算法相比能够取得规模更小的BDD表示，而且在运行时间上比单纯的基于遗传策略的BDD优化算法效率更高。针对此算法的未来工作将集中在如何提高算法的收敛速度上。
索取号	TP271/W34/2007
英文摘要	Model checking is a widely used automatic formal verification technique for proving that a digital system satisfies a user-defined specification. Despite its recent advances, the primary obstacle to its widespread application is that its capacity can not handle state explosion problem: the state-of-the-art model checker cannot directly handle most industrial-scale designs. Abstraction refinement, an iterative process of synthesizing a simplified model to help verifying the original model, is a promising solution to the capacity problem. BDD, a compact representation of digital system model and temporal logic formulas can be used to reduce the model complexity by the aspect of data structure simplification. It is another likely approach to lighten the state explosion problem. In this thesis, a fine abstraction approach and a two-order abstraction refinement algorithm based on the fine abstraction are proposed to efficiently reach or come near to the simplest abstraction model, and a new BDD minimization algorithm based on genetic tabu hybrid strategy is proposed to efficiently reduce BDD size of model. The fine abstraction approach can make the abstraction granularity smaller. With its advantage of including only the relevant circuits atoms of state variables and intermediate combinational variables rather than state variables with their all fan-in combinational logics, the fine abstraction is proven indispensable in verifying systems with complex combinational logics. Based on K-controllability computation and K-cooperativity computation this abstraction method, a two-order abstraction refinement algorithm is proposed to identify the refinement information of states and state transitions respectively. The algorithm iteratively refines state variables and intermediate combinational variables in turn. Compared to other successful abstraction refinement algorithms, this algorithm often produces a smaller abstract model that can prove or refute the same property by consuming the shortest runtime almost. The Least fixpoint Machine-By-Machine mechanism is applied to constrain invisible variables’ arbitrary valuations to reduce the pseudo counterexamples. Analytical and experimental studies demonstrate that the fine abstraction approach and the two-order abstraction refinement techniques proposed in this thesis are the key to applying model checking to large systems. The BDD minimization algorithm based on a genetic tabu hybrid strategy presented in this thesis can reduce BDD size of model efficiently. The new BDD minimization combines the global space search of genetic algorithm with the local neighborhood search and the gradual global optimizing of tabu search. The architecture of algorithm is constructed in two level, on which all promising candidate BDD variable ordering searched locally by tabu are send to evolve genetically. The variables swap and the uniform distribution are utilized to generate neighborhood solutions in the search space. Analytical and experimental studies demonstrate the presented algorithm has more size-reduction advantage than other approaches and more runtime efficiency than simplex genetic based approach. The future work will be focused on how to improve the convergence speed of the new algorithm.
语种	中文
产权排序	1
公开日期	2010-11-29
页码	164
分类号	TP271
内容类型	学位论文
源URL	[http://ir.sia.ac.cn//handle/173321/65]
专题	沈阳自动化研究所_工业信息学研究室_工业控制系统研究室
推荐引用方式 GB/T 7714	王明全. 数字系统模型检验研究[D]. 沈阳自动化研究所. 中国科学院沈阳自动化研究所. 2007.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。