Formal Verification of Completion-Completeness for NCL Circuits

Ensuring completion-completeness is required for delay-insensitivity when utilizing bit-wise completion to pipeline NCL circuits comprised of input-incomplete logic functions. Hence, this work presents an automated formal method to detect NCL circuits that are not completion-complete.