摘要
介绍了推广化符号轨迹赋值中常用的模型检验强可满足性算法,分析了产生伪报错的原因,提出了一种降低伪报错的改进算法.该算法在前算法的基础之上减少了边的计算量,降低了由于抽象带来的伪报错问题,从而大大提高了计算过程中的准确率.实验结果表明,该改进算法在降低伪报错和减少计算量方面有明显提高.
The paper introduced a strong model checking （SMC） algorithm in generalized symbolic trajectory evaluation （GSTE） and analyzed the reason leading to false negative, proposed the improved SMC algorithm to reduce the false negative. The algorithm decreases the calculation on the edges and takes the false negative from abstract to improve the accuracy. Experimental results show the improved algorithm makes a big progress on reducing false negative and calculation.
出处
《微电子学与计算机》
CSCD
北大核心
2008年第5期207-210,共4页
Microelectronics & Computer
基金
国家"八六三"计划项目(2006AA01Z173)
关键词
符号化轨迹赋值
推广化符号轨迹赋值
伪报错
形式化验证
模型检验强可满足性
symbolic trajectory evaluation
generalized symbolic trajectory evaluation
false negative
formal verification
strong model checking
