Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver
M.K. Iyer, G. Parthasarathy, Kwang-Ting Tim Cheng · Design, Automation, and Test in Europe · 2005
We present new techniques for improving search in a hybrid Davis-Putnam-Logemann-Loveland based constraint solver for RTL (register-transfer level) circuits (HDPLL). In earlier work on HDPLL (Parthasarathy, G. et al., 41st DAC, 2004), the authors combined solvers for integer and Boolean domains using finite-domain constraint propagation with heuristic conflict-based learning. We describe a new algorithm that extends the conflict-based unique-implication point learning in Boolean SAT (satisfiability) solvers to hybrid Boolean-integer domains in HDPLL. We describe data-structures for efficient constraint propagation on the hybrid learned relations, similar to two-literal watching in Boolean SAT. We demonstrate that these new techniques provide considerable performance benefits when compared with other combinations of decision theories.