Automated, efficient, and sound verification of integer multipliers

Simple item page
dc.contributor.advisorHunt, Warren A., 1958-
dc.contributor.committeeMemberFussell, Donald S.
dc.contributor.committeeMemberOrshansky, Michael E.
dc.contributor.committeeMemberSlobodova, Anna
dc.contributor.committeeMemberTouba, Nur A.
dc.creatorTemel, Mertcan
dc.creator.orcid0000-0002-9738-587X
dc.date.accessioned2021-09-24T20:44:52Z
dc.date.available2021-09-24T20:44:52Z
dc.date.created2021-08
dc.date.issued2021-08-12
dc.date.submittedAugust 2021
dc.date.updated2021-09-24T20:44:53Z
dc.description.abstractFormal verification of multiplier designs has been studied for decades. However, the practicality of the state-of-the-art tools has been limited because they do not scale for large designs or they only support certain types of design methodologies. We have developed a new and widely applicable algorithm, S-C-Rewriting, for efficient and automatic verification of signed and unsigned arithmetic modules with embedded multipliers. The architectures of our target designs include Wallace, Dadda, 4-to-2 compressor trees, and more with Booth encoding and various types of final stage adders. The output of these multipliers may be truncated, right-shifted, or a combination of both, and they may be implemented as part of a multiply-accumulate, dot-product, or other arithmetic units with control logic. Our method and tool are verified using the ACL2 theorem prover, and users can trust the soundness of our verification results. Our experiments have shown that our approach scales well in terms of time and memory. We can soundly confirm the correctness of 1024x1024-bit isolated multiplier and similarly large dot-product designs within a few minutes. Additionally, we can quickly generate counterexamples for flawed designs. Our tool and benchmarks are available online for public use.
dc.description.departmentElectrical and Computer Engineering
dc.format.mimetypeapplication/pdf
dc.identifier.urihttps://hdl.handle.net/2152/88056
dc.identifier.urihttp://dx.doi.org/10.26153/tsw/14997
dc.language.isoen
dc.subjectFormal verification
dc.subjectHardware verification
dc.subjectACL2
dc.subjectMultiplier verification
dc.subjectInteger multipliers
dc.subjectTerm rewriting
dc.subjectInteractive theorem provers
dc.titleAutomated, efficient, and sound verification of integer multipliers
dc.typeThesis
dc.type.materialtext
thesis.degree.departmentElectrical and Computer Engineering
thesis.degree.disciplineElectrical and Computer Engineering
thesis.degree.grantorThe University of Texas at Austin
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy

Access full-text files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
TEMEL-DISSERTATION-2021.pdf
Size:
2.44 MB
Format:
Adobe Portable Document Format
Download

License bundle

Now showing 1 - 2 of 2
No Thumbnail Available
Name:
PROQUEST_LICENSE.txt
Size:
4.45 KB
Format:
Plain Text
Description:
Download
No Thumbnail Available
Name:
LICENSE.txt
Size:
1.84 KB
Format:
Plain Text
Description:
Download

Collections

UT Electronic Theses and Dissertations