An efficient finite-domain constraint solver for circuits

被引：22

作者：

Parthasarathy, G ^{[1
]}

Iyer, MK ^{[1
]}

Cheng, KT ^{[1
]}

Wang, LC ^{[1
]}

机构：

[1] Univ Calif Santa Barbara, Dept Elect & Comp Engn, Santa Barbara, CA 93106 USA

来源：

41ST DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2004 | 2004年

关键词：

design verification; decision procedures; Boolean satisfiability; integer linear programming; bit-vector arithmetic;

D O I：

10.1145/996566.996628

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper presents a novel hybrid finite-domain constraint solving engine for RTL circuits. We describe how DPLL search is modified for search in combined integer and Boolean domains by using efficient finite-domain constraint propagation. This enables efficient combination of Boolean SAT and linear integer arithmetic solving techniques. We automatically use control and data-path abstraction in RTL descriptions. We use conflict-based learning using the variables on the boundary of control and data-path for additional performance benefits. Finally, we analyze the hybrid constraint solver experimentally using some example circuits.

引用

页码：212 / 217

页数：6