Checking nested properties using bounded model checking and sequential ATPG

This paper develops a novel approach to formally verify nested VLSI circuit properties, using bounded model checking and gate-level sequential ATPG tools. This approach improves the verification quality by devising an algorithm that checks nested realistic properties. This makes ATPG verification based tools applicable to realistic properties. We also show that the performance of our approach is superior when compared to SAT-based techniques in both efficiency and capacity, especially for large bounds and for complex properties.