References

  1. ACL2 System and Community Books. Available at https://github.com/acl2/acl2.
  2. 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.
  3. Randal E. Bryant & Yirng-An Chen (1994): "Verification of Arithmetic Functions with Binary Moment Diagrams". In: DAC 1994, doi:10.21236/ada281028.
  4. 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.
  5. 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.
  6. ACL2 Community (Accessed Jan 1, 2021): ACL2+Books Documentation. Available at http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html.
  7. Naofumi Homma, Yuki Watanabe, Takafumi Aoki & Tatsuo Higuchi (2006): Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Transactions 89-A, pp. 3500–3509, doi:10.1109/ispacs.2006.364918. Available at https://www.ecsis.riec.tohoku.ac.jp/topics/amg/.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. Alireza Mahzoon, Daniel Große & Rolf Drechsler (2019): SCA Multiplier Generator GenMul. Available at http://www.sca-verification.org.
  20. 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.
  21. David M. Russinoff (2019): Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. Springer, doi:10.1007/978-3-319-95513-1.
  22. 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.
  23. 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.
  24. 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.
  25. Mertcan Temel (2019): ACL2 SVL Documentation. Available at http://www.cs.utexas.edu/users/moore/acl2/ manuals/current/manual/?topic=ACL2____SVL.
  26. Mertcan Temel (2019): Fast Multiplier Generator. Available at https://github.com/temelmertcan/multgen.
  27. Mertcan Temel (2020): RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2 327, doi:10.4204/eptcs.327.5.
  28. Mertcan Temel (2021): Automated, Efficient, and Sound Verification of Integer Multipliers. The University of Texas at Austin.
  29. 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.
  30. 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.
  31. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org