Mining Complex Boolean Expressions for Sequential Equivalence Checking

摘要：

We propose a novel technique to mine powerful and generalized boolean relations among flip-flops in a sequential circuit for sequential equivalence checking. In contrast to traditional learning methods, our mining algorithm can detect inductive invariants as well as illegal state cubes. These invariants can be arbitrary boolean expressions and can thus prune a large dont care space during equivalence checking. Experimental results demonstrate that these general invariants can be very effective for sequential equivalence checking of circuits with no or very few equivalent signals between them, with low computational costs.

关键词： Sequential Equivalence Checking BLOSOM Re-descriptions Induction based proof

作者: Neha God Michael S. Hsiao Narendran Ramakrishnant Mohammed J. Zaki

作者单位: Department of Electrical and Computer Engineering, Virginia Tech, Blacksburg, VA, 24061 Department of Computer Science, Virginia Polytechnic Institute and State University, Blacksburg, VA, Department of Computer Science, Rensselaer Polytechnic Institute, Troy, New York, USA 12180

会议类型: 国际会议

会议名称: 2010 19th IEEE Asian Test Symposium(第19届IEEE亚洲测试技术学术会议 ATS 2010)

会议地点: 上海

会议语种:英文

页码: 442-447

在线出版日期: 2010-12-01（万方平台首次上网日期，不代表论文的发表时间）