Verification of asynchronous interface circuits with bounded wire delays

The problem of verifying that the gate-level implementation of an asynchronous circuit, with given or extracted bounds on wire and gate delays, is equivalent to a specification of the asynchronous circuit behavior described as a classical flow table, under the fundamental mode of operation, is considered. A procedure for extracting the complete set of possible flow tables from a gate-level description of an asynchronous circuit under the bounded wire delay model is given. Given an extracted flow table and the initial flow table specification, procedures for constructing a product flow table so as to check for machine equivalence are discussed.<>