| 基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法 |
| |
| 引用本文： | 李暾,屈婉霞,郭阳,刘功杰,李思昆.基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法[J].计算机学报,2007,30(7):1138-1144. |
| |
| 作者姓名： | 李暾 屈婉霞 郭阳 刘功杰 李思昆 |
| |
| 作者单位： | 国防科学技术大学计算机学院,长沙,410073 |
| |
| 摘 要： | 利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.
|
| 关 键 词： | 谓词抽象 Verilog约束逻辑编程 模型检验 符号模拟 符号模拟 约束逻辑编程 Verilog 谓词 抽象方法 Constraint Logic Programming Simulation Symbolic 速度 抽象技术 结果 实验 框架 统一 效率 字级 抽象系统 计算 求解 抽象问题 |
| 修稿时间： | 2005-05-30 |
Predicate Abstraction of RT-Level Verilog Using Symbolic Simulation and Constraint Logic Programming |
| |
| LI Tun,QU Wan-Xia,GUO Yang,LIU Gong-Jie,LI Si-Kun.Predicate Abstraction of RT-Level Verilog Using Symbolic Simulation and Constraint Logic Programming[J].Chinese Journal of Computers,2007,30(7):1138-1144. |
| |
| Authors: | LI Tun QU Wan-Xia GUO Yang LIU Gong-Jie LI Si-Kun |
| |
| Abstract: | |
| |
| Keywords: | predicate abstraction Verilog constraint logic programming model checking symbolic simulation |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
