Formal Verification of C-element Circuits

It is well known that the correct behavior of asynchronous circuits is not guaranteed when the inputs switch too slowly. The erroneous behavior is generally difficult to be spotted by simulation based methods. We applied formal methods to study the analog switching behavior of a full-buffer circuit composed of C-elements. We used our reach ability analysis tool COHO to compute all reachable states of two C-element designs and verified several analog properties. Based on these properties, we identified a sufficient condition under which the full-buffer circuit always supports the designed handshaking protocol. We also improved the COHO tool to automate the verification process, reduce error and improve performance.