摘要
随着软硬件设计的规模越来越大,功能越来越复杂,往往导致形式化验证出现"组合爆炸"问题,而谓词抽象方法是解决状态空间"组合爆炸"问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用,通过求解不可满足子式,能够减少谓词抽象过程中精化迭代的次数,从而提高形式化验证效率。针对微处理器的指令Cache部件,将两种最小不可满足子式的求解算法进行了比较,结果表明贪心遗传算法在运行效率方面优于分支-限界算法。并且深入分析了不可满足子式在硬件谓词抽象中的作用,以及如何加速芯片的形式化验证过程。
With the growing scale and complexity of software and hardware designs, formal verification generally meets the ＂combination explosion＂ problems in modem CAD flows. Predicate abstraction is an important technique to solve the ＂combination explosion＂ of verification state space. Predicate abstraction for hardware is a typical application of unsatisfiable subformula. The number of iteration in refinement procedure was reduced to improve the efficiency of formal verification, by computing the unsatisfiable subformulae. In this paper, two unsatisfiable subformula extraction algorithms were compared on the instruction Cache unit of a microprocessor. The experimental results show that the greedy generic algorithm outperforms the branch-bound algorithm. Furthermore it is proven that the unsatisfiable subformula plays an important role in predicate abstraction, and it can improve the efficiency of formal verification.
出处
《计算机应用》
CSCD
北大核心
2014年第A01期273-276,共4页
journal of Computer Applications
基金
国家863计划项目(2012AA01A301)
国家自然科学基金资助项目(61103083
61133007)
关键词
功能验证
形式化方法
谓词抽象
布尔可满足性
最小不可满足子式
functional verification
formal method
predicate abstraction
boolean satisfiability
minimal unsatisfiablesub formula
