|
|||||
|
|
| 一个适于形式验证的ATPG引擎 | |
| 引用本文： | 李光辉,邵明,李晓维.一个适于形式验证的ATPG引擎[J].计算机研究与发展,2004,41(5):886-893. |
| 作者姓名： | 李光辉 邵明 李晓维 |
| 作者单位： | 1. 中国科学院计算技术研究所,北京,100080;浙江林学院信息系,杭州,311300;中国科学院研究生院,北京,100039 2. 中国科学院计算技术研究所,北京,100080;中国科学院研究生院,北京,100039 3. 中国科学院计算技术研究所,北京,100080 |
| 基金项目： | 国家自然科学基金重点项目 ( 90 2 0 70 0 2)，浙江省自然科学基金项目 (M 60 3 0 97)，北京市重点科技基金项目 (H 0 2 0 12 0 12 0 13 0 )，中国科学院计算技术研究所领域前沿青年基金项目 ( 2 0 0 2 6180 6) |
| 摘 要： | 自动测试产生(ATPG)不仅应用于芯片测试向量生成，也是芯片设计验证的重要引擎之一．提出了一种组合电路测试产生的代数方法，既可作为组合验证的ATPG引擎，又可用于通常的测试产生．该算法充分发挥了二叉判决图(BDD)及布尔可满足性(SAT)的优势，通过启发式策略实现SAT算法与BDD算法的交替，防止因构造BDD可能导致的内存爆炸，而且使用增量的可满足性算法，进一步提高了算法的效率．实验结果表明了该算法的可行性和有效性． |
| 关 键 词： | 组合电路 测试产生 形式验证 二叉判决图 布尔可满足性 |
An ATPG Engine for Formal Verification |
|
| LI Guang Hui ,,SHAO Ming ,and LI Xiao Wei.An ATPG Engine for Formal Verification[J].Journal of Computer Research and Development,2004,41(5):886-893. | |
| Authors: | LI Guang Hui SHAO Ming and LI Xiao Wei |
| Affiliation: | LI Guang Hui 1,2,3,SHAO Ming 1,3,and LI Xiao Wei 1 1 |
| Abstract: | ATPG can generate patterns for testing integrated circuit chips, it is also an important engine for design verification In this paper, an algebraic algorithm for combinational circuits test generation is presented, it can also be an ATPG engine for combinational verification This algorithm makes full use of the advantages of binary decision diagram (BDD) and Boolean satisfiability (SAT) Through interleaving SAT based algorithm with BDD based algorithm with some heuristics, it avoids potential memory explosion caused by constructing BDDs Moreover, this algorithm uses incremental satisfiability, which improves the algorithm's efficiency The experimental results demonstrate the effectiveness and feasibility of this algorithm |
| Keywords: | combinational circuit test generation formal verification BDD SAT |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ | |