不可满足子式在谓词抽象中的应用与分析

作     者：张建民 黎铁军 张峻 庞征斌 李思昆 ZHANG Jianmin;LI Tiejun;ZHANG Jun;PANG Zhengbin;LI Sikun

作者机构：国防科学技术大学计算机学院长沙410073 

基　　金：国家863计划项目(2012AA01A301) 国家自然科学基金资助项目(61103083 61133007) 

出 版 物：《计算机应用》 (journal of Computer Applications)

年 卷 期：2014年第34卷第A1期

页      码：273-276页

摘      要：随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少谓词抽象过程中精化迭代的次数,从而提高形式化验证效率。针对微处理器的指令Cache部件,将两种最小不可满足子式的求解算法进行了比较,结果表明贪心遗传算法在运行效率方面优于分支-限界算法。并且深入分析了不可满足子式在硬件谓词抽象中的作用,以及如何加速芯片的形式化验证过程。

主 题 词：功能验证 形式化方法 谓词抽象 布尔可满足性 最小不可满足子式 

学科分类：081203[081203] 08[工学] 0835[0835] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203735481...