Automatic abstraction refinement of TR for PDR
Journal
Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
Journal Volume
25-28-January-2016
Pages
121-126
Date Issued
2016
Author(s)
Abstract
Localization abstraction is a powerful technique that has long been a solution to the scalability problem of hardware model checking. However, computation resources are often inefficiently consumed during the repeated trial-and-errors between abstraction refinement engines and proof engines. To this end, many efforts have been made to combine the two independent techniques for better efficiency in recent years. In this paper, we present a novel model checking method that combines PDR (aka IC3) with a gate-level, hybrid abstraction technique to achieve further enhancement of scalability and performance for PDR. We implemented our work in ABC and evaluated it on the HWMCC13, HWMCC14 benchmark suites. The results show that our method substantially outperforms PDR as implemented in ABC and complements it on a large number of benchmark instances.
SDGs
Type
conference paper