Structural search for RTL with predicate learning

The authors presented an efficient search strategy for satisfiability checking on circuits represented at the register-transfer-level (RTL). The authors used the RTL circuit structure by extending concepts from classic automatic test-pattern generation (ATPG) algorithms and interval-arithmetic to guide the search process. The idea of Boolean recursive learning was extended on predicate logic in the RTL using Boolean and interval constraint propagation in the control and data-path of the circuit. This is used as a pre-processing step to derive relations between predicate logic signals that are used to augment the search. It is demonstrated experimentally that these methods provide significant improvement over current techniques on sample benchmarks.