Formal Verification of Pipelined Cryptographic Circuits: A Functional Approach

Cryptographic circuits are essential in systems where security is the main criteria. Therefore, it is crucial to ensure the correctness of not only the cryptographic algorithms, but also their hardware implementations. Formal methods, unlike the other validation techniques, guarantee the absence of errors.The problem is that designers still use conventional imperative Hardware Description Languages (HDLs), which are poorly suited for formal verification. This paper presents an automatic verification methodology for the pipelined cryptographic circuits using formal methods. It consists of using the functional HDL Lava to describe and verify the equivalence between the behavioural specification and structural implementation of a circuit. To the best of our knowledge, we are the first to use this functional HDL for that purpose. To show the features of the proposed approach, it was applied to verify the pipelined implementation of the cryptographic circuit AES (Advanced Encryption Standard). © 2021 Slovene Society Informatika. All rights reserved.