Equivalence verification for NULL Convention Logic (NCL) circuits

NULL Convention Logic (NCL) circuits are asynchronous circuits and find application in SoC design due to their delay-insensitive nature, which allows ease in resolution of timing issues in IP component reuse for SoC. NCL components are typically synthesized from synchronous circuits. For any design paradigm to be feasible, verification is an important factor. We present a formal verification methodology for checking equivalence of NCL circuits against their synchronous parent circuits. The methodology includes a procedure that computes the reachable states of NCL sequential circuits and a refinement mapping function that can be used to map NCL circuit states onto synchronous circuit states. The methodology is demonstrated by verifying the correctness of several NCL circuits.