| 在形式验证和ATPG中的布尔可满足性问题 |
| |
| 引用本文： | 邓雨春,杨士元,王红,薛月菊. 在形式验证和ATPG中的布尔可满足性问题[J]. 计算机辅助设计与图形学学报, 2003, 15(10): 1207-1212 |
| |
| 作者姓名： | 邓雨春 杨士元 王红 薛月菊 |
| |
| 作者单位： | 清华大学自动化系,北京,100084 |
| |
| 基金项目： | 国家自然科学基金重大项目 (90 2 0 70 16)资助 |
| |
| 摘 要： | 介绍布尔可满足性(SAT)求解程序在测试向量自动生成、符号模型检查、组合等价性检查和RTL电路设计验证等电子设计自动化领域中的应用．着重阐述如何在算法中有机地结合电路拓扑结构及其与特定应用相关的信息，以便提高问题求解效率．最后给出下一步可能的研究方向。
|
| 关 键 词： | 数字电路 电路设计自动化 形式验证 ATPG 布尔可满足性 |
| 修稿时间： | 2002-08-13 |
Formal Verification and ATPG Using Boolean Satisfiability |
| |
| Deng Yuchun Yang Shiyuan Wang Hong Xue Yueju. Formal Verification and ATPG Using Boolean Satisfiability[J]. Journal of Computer-Aided Design & Computer Graphics, 2003, 15(10): 1207-1212 |
| |
| Authors: | Deng Yuchun Yang Shiyuan Wang Hong Xue Yueju |
| |
| Abstract: | Boolean Satisfiability is probably the most studied of combinatorial search problems and finds a number of applications in electronic design automation (EDA). In recent years, quite a few new and efficient SAT solvers have been developed, which make it possible solving much larger problem instances. We highlight the use of SAT algorithm to solve lots of EDA problems in such diverse areas as test pattern generation, symbolic model checking, combinational equivalence checking, and verification for RTL design. In addition, it is stressed how the useful information of circuit structure and specific problems to be solved is introduced to accelerate the SAT based algorithms. |
| |
| Keywords: | Boolean satisfiability formal verification automatic test pattern generation (ATPG) symbolic model checking equivalence checking RTL design |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
