Show simple item record

dc.contributor.authorboga, anil kumar
dc.date.accessioned2022-08-22 19:34:02 (GMT)
dc.date.available2022-08-22 19:34:02 (GMT)
dc.date.issued2022-08-22
dc.date.submitted2022-08-16
dc.identifier.urihttp://hdl.handle.net/10012/18606
dc.description.abstractData 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.en
dc.language.isoenen
dc.publisherUniversity of Waterlooen
dc.subjectcryptographyen
dc.subjectGalois fielden
dc.subjectformal verificationen
dc.subjectequivalence verificationen
dc.subjectalgebraic normal formen
dc.titleA graph based approach for formal verification of Galois field multipliersen
dc.typeMaster Thesisen
dc.pendingfalse
uws-etd.degree.departmentElectrical and Computer Engineeringen
uws-etd.degree.disciplineElectrical and Computer Engineeringen
uws-etd.degree.grantorUniversity of Waterlooen
uws-etd.degreeMaster of Applied Scienceen
uws-etd.embargo.terms0en
uws.contributor.advisorAagaard, mark
uws.contributor.affiliation1Faculty of Engineeringen
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.typeOfResourceTexten
uws.peerReviewStatusUnrevieweden
uws.scholarLevelGraduateen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record


UWSpace

University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages