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

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