Efficient verification of determinate speed-independent circuits

We present sufficient conditions for the correctness of speed-independent circuits with respect to their state graph (SG) specification, which can be tested in linear-time with respect to the size of the SG. Our correctness conditions consist of one safety condition and one progress condition. The progress condition detects deadlock conditions that are not present in the specification. The SG specifications considered are determinate, allowing input choice (conditionals) but not output choice (arbitration). The circuits considered are a network of basic gates; arbiters and mutual-exclusion elements are not allowed. We present an efficient algorithm to test the correctness conditions, in which false positives are not possible, but false negatives are possible. We have implemented the algorithm and present a table of run-time comparisons between our verification tool and the tool AVER by D. Dill on a large benchmark of asynchronous circuits. The results demonstrate run-times of over an order of magnitude faster than AVER and no false negatives were found. Our speedup is achieved by avoiding the state explosion problem caused by explicitly examining the behavior of internal signals.