Verifying and Testing Asynchronous Circuits Using Lotos

It is shown how Dill (Digital Logic in Lotos) can be used to specify, verify and test asynchronous (unclocked) hardware designs. New relations for (strong) conformance are defined for assessing a circuit implementation against its specification. An algorithm is also presented for generating and applying implementation tests based on a specification. Tools have been developed for automated verification of conformance and generation of tests. The approach is illustrated with three case studies that explore speed independence, delay insensitivity and testing of sample asynchronous circuits.