@misc(acl2-github,
 title        = {{ACL2 System and Community Books}},
 url          = {https://github.com/acl2/acl2},
)
@inproceedings(10.1145/1217975.1217992,
 author       = {Robert S. Boyer and Warren A. Hunt},
 year         = {2006},
 title        = {Function Memoization and Unique Object Representation for ACL2 Functions},
 booktitle    = {Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications},
 series       = {ACL2 '06},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {81\IeC{\textendash}89},
 doi          = {10.1145/1217975.1217992},
)
@inproceedings(bmd-paper,
 author       = {Randal E. Bryant and Yirng-An Chen},
 year         = {1994},
 title        = {"{Verification of Arithmetic Functions with Binary Moment Diagrams}"},
 booktitle    = {DAC 1994},
 doi          = {10.21236/ada281028},
)
@inproceedings(bdd-paper,
 author       = {Jerry R. Burch},
 year         = {1991},
 title        = {{Using BDDs to Verify Multipliers}},
 booktitle    = {Proceedings of the 28th ACM/IEEE Design Automation Conference},
 series       = {DAC \IeC{\textquoteright}91},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {408\IeC{\textendash}412},
 doi          = {10.1145/127601.127703},
)
@article(Ciesielski2019UnderstandingAR,
 author       = {Maciej Ciesielski and Tiankai Su and Atif Yasin and Cunxi Yu},
 year         = {2019},
 title        = {{Understanding Algebraic Rewriting for Arithmetic Circuit Verification: a Bit-Flow Model}},
 journal      = {{IEEE} Transactions on Computer-Aided Design of Integrated Circuits and Systems},
 doi          = {10.1109/tcad.2019.2912944},
)
@misc(acl2-doc,
 author       = {ACL2 Community},
 year         = {Accessed Jan 1, 2021},
 title        = {ACL2+Books Documentation},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html},
)
@article(homma,
 author       = {Naofumi Homma and Yuki Watanabe and Takafumi Aoki and Tatsuo Higuchi},
 year         = {2006},
 title        = {{Formal Design of Arithmetic Circuits Based on Arithmetic Description Language}},
 journal      = {IEICE Transactions},
 volume       = {89-A},
 pages        = {3500--3509},
 doi          = {10.1109/ispacs.2006.364918},
 url          = {https://www.ecsis.riec.tohoku.ac.jp/topics/amg/},
)
@inproceedings(hunt-meta,
 author       = {Warren A. Hunt and Matt Kaufmann and Robert Bellarmine Krug and J. Strother Moore and Eric Whitman Smith},
 year         = {2005},
 title        = {Meta Reasoning in {ACL2}},
 editor       = {Joe Hurd and Tom Melham},
 booktitle    = {Theorem Proving in Higher Order Logics},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {163--178},
 doi          = {10.1007/11541868_11},
)
@article(Hunt2017IndustrialHA,
 author       = {Warren A. Hunt and Matt Kaufmann and {Moore, J S.} and Anna Slobodova},
 year         = {2017},
 title        = {{Industrial Hardware and Software Verification with {ACL}2}},
 journal      = {Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences},
 volume       = {375},
 number       = {2104},
 pages        = {20150399},
 doi          = {10.1098/rsta.2015.0399},
)
@incollection(hardin-centaur,
 author       = {Warren A. Hunt and Sol Swords and Jared Davis and Anna Slobodova},
 year         = {2010},
 title        = {{Use of Formal Verification at Centaur Technology}},
 editor       = {David Hardin},
 booktitle    = {{Design and Verification of Microprocessor Systems for High-Assurance Applications}},
 publisher    = {Springer},
 pages        = {65--88},
 doi          = {10.1007/978-1-4419-1539-9\_3},
)
@inproceedings(jason-baumgartner,
 author       = {Christian Jacobi and Kai Weber and Viresh Paruthi and Jason Baumgartner},
 year         = {2005},
 title        = {Automatic Formal Verification of Fused-Multiply-Add FPUs},
 booktitle    = {Proceedings of the Conference on Design, Automation and Test in Europe - Volume 2},
 series       = {DATE \IeC{\textquoteright}05},
 publisher    = {IEEE Computer Society},
 address      = {USA},
 pages        = {1298\IeC{\textendash}1303},
 doi          = {10.1109/DATE.2005.75},
)
@inproceedings(conf-date-KaivolaN02,
 author       = {Roope Kaivola and Naren Narasimhan},
 year         = {2002},
 title        = {{Formal Verification of the Pentium {\textregistered} 4 Floating-Point Multiplier}},
 booktitle    = {2002 Design, Automation and Test in Europe Conference and Exposition {(DATE} 2002), 4-8 March 2002, Paris, France},
 pages        = {20--27},
 doi          = {10.1109/DATE.2002.998245},
)
@inproceedings(dkaufmann-FMCAD19,
 author       = {D. {Kaufmann} and A. {Biere} and M. {Kauers}},
 year         = {2019},
 title        = {{Verifying Large Multipliers by Combining SAT and Computer Algebra}},
 booktitle    = {2019 Formal Methods in Computer Aided Design (FMCAD)},
 pages        = {28--36},
 doi          = {10.23919/FMCAD.2019.8894250},
)
@incollection(DBLP:books/sp/10/KaufmannM10,
 author       = {Matt Kaufmann and J. Strother Moore},
 year         = {2010},
 title        = {{ACL2} and Its Applications to Digital System Verification},
 editor       = {David S. Hardin},
 booktitle    = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
 publisher    = {Springer},
 pages        = {1--21},
 doi          = {10.1007/978-1-4419-1539-9\_1},
)
@incollection(acl2-2,
 author       = {Matt Kaufmann and J. Strother Moore},
 year         = {2010},
 title        = {{ACL2} and Its Applications to Digital System Verification},
 editor       = {David S. Hardin},
 booktitle    = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
 publisher    = {Springer},
 pages        = {1--21},
 doi          = {10.1007/978-1-4419-1539-9\_1},
)
@article(clause-processors,
 author       = {Matt Kaufmann and Jstrother Moore and Sandip Ray and Erik Reeber},
 year         = {2009},
 title        = {Integrating External Deduction Tools with ACL2},
 journal      = {J. Applied Logic},
 volume       = {7},
 pages        = {3--25},
 doi          = {10.1016/j.jal.2007.07.002},
)
@article(Mahzoon2018PolyCleanerCY,
 author       = {Alireza Mahzoon and Gro{\ss}e, Daniel and Rolf Drechsler},
 year         = {2018},
 title        = {{PolyCleaner: Clean your Polynomials before Backward Rewriting to verify Million-gate Multipliers}},
 journal      = {2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)},
 pages        = {1--8},
 doi          = {10.1145/3240765.3240837},
)
@inproceedings(Mahzoondac2019,
 author       = {Alireza Mahzoon and Gro{\ss}e, Daniel and Rolf Drechsler},
 year         = {2019},
 title        = {{RevSCA: Using Reverse Engineering to Bring Light into Backward Rewriting for Big and Dirty Multipliers}},
 booktitle    = {Proceedings of the 56th Annual Design Automation Conference 2019},
 series       = {DAC '19},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {185:1--185:6},
 doi          = {10.1145/3316781.3317898},
)
@misc(sca-genmul,
 author       = {Alireza Mahzoon and Gro{\ss}e, Daniel and Rolf Drechsler},
 year         = {2019},
 title        = {{SCA Multiplier Generator GenMul}},
 url          = {http://www.sca-verification.org},
)
@inproceedings(acl2-1,
 author       = {J. Strother Moore and Marijn J. H. Heule},
 year         = {2017},
 title        = {Industrial Use of {ACL2:} Applications, Achievements, Challenges, and Directions},
 editor       = {Giles Reger and Dmitriy Traytel},
 booktitle    = {{ARCADE} 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017},
 series       = {EPiC Series in Computing},
 volume       = {51},
 publisher    = {EasyChair},
 pages        = {42--45},
 doi          = {10.29007/dh3f},
)
@book(russinoff2019formal,
 author       = {David M. Russinoff},
 year         = {2019},
 title        = {{Formal Verification of Floating-Point Hardware Design: A Mathematical Approach}},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-95513-1},
)
@inproceedings(amr-ahmed2016,
 author       = {Sayed-Ahmed, Amr and Gro{\ss}e, Daniel and K\IeC{\"u}hne, Ulrich and Mathias Soeken and Rolf Drechsler},
 year         = {2016},
 title        = {{Formal Verification of Integer Multipliers by Combining Gr\IeC{\"o}bner Basis with Logic Reduction}},
 booktitle    = {Proceedings of the 2016 Design, Automation {\&} Test in Europe Conference {\&} Exhibition ({DATE})},
 publisher    = {Research Publishing Services},
 pages        = {1048--1053},
 doi          = {10.3850/9783981537079\_0248},
)
@inproceedings(memocode11,
 author       = {Anna Slobodova and Jared Davis and Sol Swords and Warren A. Hunt},
 year         = {2011},
 title        = {{A Flexible Formal Verification Framework for Industrial Scale Validation}},
 booktitle    = {Proceedings of the $9$th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE)},
 publisher    = {IEEE/ACM},
 address      = {Cambridge, UK},
 pages        = {89--97},
 doi          = {10.1109/memcod.2011.5970515},
)
@inproceedings(sol-fgl,
 author       = {Sol Swords},
 year         = {2020},
 title        = {New Rewriter Features in {FGL}},
 editor       = {Grant O. Passmore and Ruben Gamboa},
 booktitle    = {Proceedings of the Sixteenth International Workshop on the {ACL2} Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020},
 series       = {{EPTCS}},
 volume       = {327},
 pages        = {32--46},
 doi          = {10.4204/EPTCS.327.3},
)
@misc(svl-books,
 author       = {Mertcan Temel},
 year         = {2019},
 title        = {{ACL2 SVL Documentation}},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/ manuals/current/manual/?topic=ACL2\_\_\_\_SVL},
)
@misc(tem-genmul,
 author       = {Mertcan Temel},
 year         = {2019},
 title        = {{Fast Multiplier Generator}},
 url          = {https://github.com/temelmertcan/multgen},
)
@article(rp-paper,
 author       = {Mertcan Temel},
 year         = {2020},
 title        = {{RP-Rewriter}: An Optimized Rewriter for Large Terms in {ACL2}},
 volume       = {327},
 doi          = {10.4204/eptcs.327.5},
)
@phdthesis(TemelDissertation,
 author       = {Mertcan Temel},
 year         = {2021},
 title        = {Automated, Efficient, and Sound Verification of Integer Multipliers},
 school       = {The University of Texas at Austin},
)
@inproceedings(fmcad21-paper,
 author       = {Mertcan Temel and Warren A. Hunt},
 year         = {2021},
 title        = {Sound and Automated Verification of Real-World RTL Multipliers},
 booktitle    = {2021 Formal Methods in Computer Aided Design (FMCAD)},
 pages        = {53--62},
 doi          = {10.34727/2021/isbn.978-3-85448-046-4_13},
)
@inproceedings(cav-paper,
 author       = {Mertcan Temel and Anna Slobodova and Warren A. Hunt},
 year         = {2020},
 title        = {Automated and Scalable Verification of Integer Multipliers},
 editor       = {Shuvendu K. Lahiri and Chao Wang},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {485--507},
 doi          = {10.1007/978-3-030-53288-8_23},
)
@article(Yu2018FastAR,
 author       = {Cunxi Yu and Maciej Ciesielski and Alan Mishchenko},
 year         = {2018},
 title        = {{Fast Algebraic Rewriting Based on And-Inverter Graphs}},
 journal      = {{IEEE} Transactions on Computer-Aided Design of Integrated Circuits and Systems},
 volume       = {37},
 number       = {9},
 pages        = {1907--1911},
 doi          = {10.1109/tcad.2017.2772854},
)