《计算机学报》文章摘要   全文下载
文章题目	基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法
作者	李暾 屈婉霞 郭阳 刘功杰 李思昆
作者单位	(国防科学技术大学计算机学院 长沙 410073)
发表年份	2007
发表月份	7期(1138—1144)
文章摘要	摘要 利用人工智能最新研究成果——约束逻辑编程对Verilog描述进行谓词抽象，并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型，然后结合要抽象的谓词，将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时，不需要像基于SAT的方法那样将字级约束打散成位级约束，求解效率显著提高；提供了一个统一的框架用于描述各种约束.实验结果表明，与基于SAT的抽象技术相比，基于约束逻辑编程的抽象方法的求解速度有显著提高. 关键词 谓词抽象；Verilog 约束逻辑编程；模型检验；符号模拟 中图法分类号 TP306