Bounded Model Checking for RTL Circuits Based on Algorithm Abstraction Refinement

ANSI-C algorithm abstraction refinement for RTL circuits is investigated, with the goal of reducing the complexity of bounded model checking. This new method abstracts an ANSI-C algorithm from a verified RTL circuit, and then optimizes the algorithm for the ANSI-C bounded model checker CBMC. When a spurious counterexample is generated, this method refines the ANSI-C algorithm in more details. Equivalence checking between ANSI-C algorithms and RTL circuits, and that between the ANSI-C algorithms and their optimized versions are needed. Comparisons with other methods show that this new method is efficient