Synchronization-Based Abstraction Refinement for Modular Verification of Asynchronous Designs

This paper presents a modular verification approach for asynchronous circuits to address state explosion with a novel interface refinement method to reduce false counterexamples.This method borrows the idea of parallel composition, and it iteratively refines each component in a design by examining its interface interactions, and removes the behavior not synchronized with its neighbors. This method is further enhanced by synchronizing multiple components simultaneously so that inter-dependencies among components are considered. The experiments on several large asynchronous circuits show that this method efficiently removes impossible behavior from each component including ones violating correctness requirements.