基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

• 作者: 刘功杰 屈婉霞 李思昆 李暾 郭阳
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 谓词抽象 Verilog约束逻辑编程 模型检验 符号模拟
• 年，卷（期）: 2007,（7）
• 所属期刊栏目: 研究论文与技术报告
• 页码范围: 1138-1144
• 页数: 7页
• 分类号: TP306
• 字数: 5745字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2007.07.011

摘要

利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郭阳	国防科学技术大学计算机学院	39	252	9.0	14.0
2	李暾	国防科学技术大学计算机学院	29	182	7.0	12.0
3	李思昆	国防科学技术大学计算机学院	133	1339	18.0	31.0
4	屈婉霞	国防科学技术大学计算机学院	8	88	5.0	8.0
5	刘功杰	国防科学技术大学计算机学院	4	7	1.0	2.0