Robert S. Boyer & Warren A. Hunt (2006):
Function Memoization and Unique Object Representation for ACL2 Functions.
In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications,
ACL2 '06.
Association for Computing Machinery,
New York, NY, USA,
pp. 8189,
doi:10.1145/1217975.1217992.
Randal E. Bryant & Yirng-An Chen (1994):
"Verification of Arithmetic Functions with Binary Moment Diagrams".
In: DAC 1994,
doi:10.21236/ada281028.
Jerry R. Burch (1991):
Using BDDs to Verify Multipliers.
In: Proceedings of the 28th ACM/IEEE Design Automation Conference,
DAC 91.
Association for Computing Machinery,
New York, NY, USA,
pp. 408412,
doi:10.1145/127601.127703.
Maciej Ciesielski, Tiankai Su, Atif Yasin & Cunxi Yu (2019):
Understanding Algebraic Rewriting for Arithmetic Circuit Verification: a Bit-Flow Model.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems,
doi:10.1109/tcad.2019.2912944.
Warren A. Hunt, Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore & Eric Whitman Smith (2005):
Meta Reasoning in ACL2.
In: Joe Hurd & Tom Melham: Theorem Proving in Higher Order Logics.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 163–178,
doi:10.1007/11541868_11.
Warren A. Hunt, Matt Kaufmann, Moore, J S. & Anna Slobodova (2017):
Industrial Hardware and Software Verification with ACL2.
Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 375(2104),
pp. 20150399,
doi:10.1098/rsta.2015.0399.
Warren A. Hunt, Sol Swords, Jared Davis & Anna Slobodova (2010):
Use of Formal Verification at Centaur Technology.
In: David Hardin: Design and Verification of Microprocessor Systems for High-Assurance Applications.
Springer,
pp. 65–88,
doi:10.1007/978-1-4419-1539-9_3.
Christian Jacobi, Kai Weber, Viresh Paruthi & Jason Baumgartner (2005):
Automatic Formal Verification of Fused-Multiply-Add FPUs.
In: Proceedings of the Conference on Design, Automation and Test in Europe - Volume 2,
DATE 05.
IEEE Computer Society,
USA,
pp. 12981303,
doi:10.1109/DATE.2005.75.
Roope Kaivola & Naren Narasimhan (2002):
Formal Verification of the Pentium 4 Floating-Point Multiplier.
In: 2002 Design, Automation and Test in Europe Conference and Exposition (DATE 2002), 4-8 March 2002, Paris, France,
pp. 20–27,
doi:10.1109/DATE.2002.998245.
D. Kaufmann, A. Biere & M. Kauers (2019):
Verifying Large Multipliers by Combining SAT and Computer Algebra.
In: 2019 Formal Methods in Computer Aided Design (FMCAD),
pp. 28–36,
doi:10.23919/FMCAD.2019.8894250.
Matt Kaufmann & J. Strother Moore (2010):
ACL2 and Its Applications to Digital System Verification.
In: David S. Hardin: Design and Verification of Microprocessor Systems for High-Assurance Applications.
Springer,
pp. 1–21,
doi:10.1007/978-1-4419-1539-9_1.
Matt Kaufmann & J. Strother Moore (2010):
ACL2 and Its Applications to Digital System Verification.
In: David S. Hardin: Design and Verification of Microprocessor Systems for High-Assurance Applications.
Springer,
pp. 1–21,
doi:10.1007/978-1-4419-1539-9_1.
Matt Kaufmann, Jstrother Moore, Sandip Ray & Erik Reeber (2009):
Integrating External Deduction Tools with ACL2.
J. Applied Logic 7,
pp. 3–25,
doi:10.1016/j.jal.2007.07.002.
Alireza Mahzoon, Daniel Große & Rolf Drechsler (2018):
PolyCleaner: Clean your Polynomials before Backward Rewriting to verify Million-gate Multipliers.
2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD),
pp. 1–8,
doi:10.1145/3240765.3240837.
Alireza Mahzoon, Daniel Große & Rolf Drechsler (2019):
RevSCA: Using Reverse Engineering to Bring Light into Backward Rewriting for Big and Dirty Multipliers.
In: Proceedings of the 56th Annual Design Automation Conference 2019,
DAC '19.
ACM,
New York, NY, USA,
pp. 185:1–185:6,
doi:10.1145/3316781.3317898.
Alireza Mahzoon, Daniel Große & Rolf Drechsler (2019):
SCA Multiplier Generator GenMul.
Available at http://www.sca-verification.org.
J. Strother Moore & Marijn J. H. Heule (2017):
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions.
In: Giles Reger & Dmitriy Traytel: ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017,
EPiC Series in Computing 51.
EasyChair,
pp. 42–45,
doi:10.29007/dh3f.
David M. Russinoff (2019):
Formal Verification of Floating-Point Hardware Design: A Mathematical Approach.
Springer,
doi:10.1007/978-3-319-95513-1.
Amr Sayed-Ahmed, Daniel Große, Ulrich Kühne, Mathias Soeken & Rolf Drechsler (2016):
Formal Verification of Integer Multipliers by Combining Gröbner Basis with Logic Reduction.
In: Proceedings of the 2016 Design, Automation & Test in Europe Conference & Exhibition (DATE).
Research Publishing Services,
pp. 1048–1053,
doi:10.3850/9783981537079_0248.
Anna Slobodova, Jared Davis, Sol Swords & Warren A. Hunt (2011):
A Flexible Formal Verification Framework for Industrial Scale Validation.
In: Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE).
IEEE/ACM,
Cambridge, UK,
pp. 89–97,
doi:10.1109/memcod.2011.5970515.
Sol Swords (2020):
New Rewriter Features in FGL.
In: Grant O. Passmore & Ruben Gamboa: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, Worldwide, Planet Earth, May 28-29, 2020,
EPTCS 327,
pp. 32–46,
doi:10.4204/EPTCS.327.3.
Mertcan Temel (2020):
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2 327,
doi:10.4204/eptcs.327.5.
Mertcan Temel (2021):
Automated, Efficient, and Sound Verification of Integer Multipliers.
The University of Texas at Austin.
Mertcan Temel & Warren A. Hunt (2021):
Sound and Automated Verification of Real-World RTL Multipliers.
In: 2021 Formal Methods in Computer Aided Design (FMCAD),
pp. 53–62,
doi:10.34727/2021/isbn.978-3-85448-046-4_13.
Mertcan Temel, Anna Slobodova & Warren A. Hunt (2020):
Automated and Scalable Verification of Integer Multipliers.
In: Shuvendu K. Lahiri & Chao Wang: Computer Aided Verification.
Springer International Publishing,
Cham,
pp. 485–507,
doi:10.1007/978-3-030-53288-8_23.
Cunxi Yu, Maciej Ciesielski & Alan Mishchenko (2018):
Fast Algebraic Rewriting Based on And-Inverter Graphs.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 37(9),
pp. 1907–1911,
doi:10.1109/tcad.2017.2772854.