We present a new framework to express the semantics of asynchronous circuits, and as an application, an algorithm that will check an implementation given as a netlist against a specification given as a state graph (SG). The algorithm is based on an exploration of the specification that computes certain information (as symbolic states) about the corresponding implementation states, which information is represented as a Boolean formula. The algorithm is efficient, can be easily extended so as to use timing information, and in case of hazards, can provide the user with extensive and easy-to-use information about the cause of the hazard. While it induces potential conservativeness, we did not encounter such examples of false negatives.
展开▼
