Formal verification of a pipelined cryptographic circuit using equivalence checking and completion functions

In formal hardware verification, equivalence checking is often used but is unable to verify a pipelined circuit against a non-pipelined one. Without sophisticated optimizations such as structural matching, equivalence checkers can also run into state-space explosion problems. A solution is to supplement equivalence checking with the verification strategy or completion functions. In this work, three pipelined register-transfer-level implementations of the KASUMI cryptographic circuit were verified against a non-pipelined one. Our work established a practical method for constructing these completion functions efficiently in hardware description languages. At the trade-off of increased verification effort, the completion functions approach enables equivalence checking to handle both pipelined and non-pipelined circuits, and it can localize a bug into a pipeline stage.