CAJ | 학술논문

随着软硬件设计的规模越来越大，功能越来越复杂，往往导致形式化验证出现“组合爆炸”问题，而谓词抽象方法是解决状态空间“组合爆炸”问题的重要技术之一。面向硬件的谓词抽象方法是不可满足子式的典型应用，通过求解不可满足子式，能够减少谓词抽象过程中精化迭代的次数，从而提高形式化验证效率。针对微处理器的指令Cache部件，将两种最小不可满足子式的求解算法进行了比较，结果表明贪心遗传算法在运行效率方面优于分支-限界算法。并且深入分析了不可满足子式在硬件谓词抽象中的作用，以及如何加速芯片的形式化验证过程。
수착연경건설계적규모월래월대，공능월래월복잡，왕왕도치형식화험증출현“조합폭작”문제，이위사추상방법시해결상태공간“조합폭작”문제적중요기술지일。면향경건적위사추상방법시불가만족자식적전형응용，통과구해불가만족자식，능구감소위사추상과정중정화질대적차수，종이제고형식화험증효솔。침대미처리기적지령Cache부건，장량충최소불가만족자식적구해산법진행료비교，결과표명탐심유전산법재운행효솔방면우우분지-한계산법。병차심입분석료불가만족자식재경건위사추상중적작용，이급여하가속심편적형식화험증과정。
With the growing scale and complexity of software and hardware designs, formal verification generally meets the “combination explosion” problems in modern 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.