A graph based approach for formal verification of Galois field multipliers

Abstract

Data transfer between devices has increased rapidly with improvements in technology and the internet. To protect data from hackers, data is encrypted using methods of cryptography. To make the process of encryption faster, these circuits are often implemented in hardware. A bug in these circuits compromise the security of these systems. Cryptography circuits are becoming large and complex due to the increase in the importance of security and computation power available to the hacker. Hence verification of these circuits is of utmost importance. Time and resources taken by conventional methods increase exponentially with the size and complexity of circuits. Formal verification has the potential to improve the verification process by providing better than exponential complexity for some systems.

Conventional formal verification methods do not perform well on cryptography circuits as they are ''xor'' rich circuits. Cryptography circuits often consist of Galois field circuits. Galois field circuits are also widely used in various fields like communication, security and signal processing. There are two main operations in Galois field namely addition and multiplication. Addition is simply bitwise ''xor'' of operands. Multiplication is more complicated. Mastrovito, Montgomery and Karatsuba multipliers are optimized algorithms for multiplication. In this thesis, we developed novel methods for the formal verification of Galois field multipliers.

Equivalence verification of Galois field circuits becomes challenging as the size of inputs increases because the asymptotic worst-case complexity is exponential. The previous best-known method reduces the time and memory to some extent by using parallelism. In this thesis, a novel formal verification method is developed which provides a range of 4$\times$--256$\times$ speedup when compared to the previously best-known method. We developed novel data structures and algorithms based on using the algebraic normal form as a canonical graph-based representation of Boolean functions. We have developed various normalization methods for our data structures. Experiments were performed on bit-level synthesized Mastrovito, Montgomery and Karatsuba multipliers.