ACL2 Web site.
http://www.cs.utexas.edu/users/moore/acl2/.
Mark D Aagaard & Carl-Johann H Seger (1995):
The formal verification of a pipelined double-precision IEEE floating-point multiplier.
In: International Conference on Computer Aided Design,
pp. 7–10.
Christoph Berg & Christian Jacobi (2001):
Formal Verification of the VAMP Floating Point Unit.
In: CHARME 2001, volume 2144 of LNCS,
pp. 325–339,
doi:10.1007/3-540-44798-9_26.
Institute of Electrical and Electronics Engineers (1985):
IEEE Standard for Binary Floating-Point Arithmetic.
ANSI/IEEE Standard 754-1985.
IEEE, New York.
Roope Kaivola & Naren Narasimhan (2002):
Formal Verification of the Pentium 4 Floating-Point Multiplier.
In: Conference on Design, Automation and Test in Europe (DATE),
pp. 20–27.
Matt Kaufmann (2003):
A Tool for simplifying files of ACL2 definitions.
In: Proceedings ACL2 Workshop.
Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/.
Matt Kaufmann, David Russinoff, Eric Smith & Rob Sumners (2005):
Formal Verification of Floating-Point RTL at AMD Using the ACL2 Theorem Prover.
In: 17th IMACS World Congress:Scientific Computation, Applied Mathematics and Simulation.
Available at: http://www.russinoff.com/papers/paris.html.
Erik Reeber & Jun Sawada (2006):
Combining ACL2 and an automated verification tool to verify a multiplier.
In: International Workshop on the ACL2 Theorem Prover and its Applications,
pp. 63–70,
doi:10.1145/1217975.1217990.
David M. Russinoff (1998):
A Mechanically Checked Proof of IEEE Compliance of a Register-Transfer-Level Specification of the AMD-K7 Floating-Point Multiplication, Division, and Square Root Instructions.
LMS Journal of Computation and Mathematics 1,
pp. 148–200.
David M. Russinoff (1999):
A Mechanically Checked Proof of IEEE Compliance of the AMD K5 Floating-Point Square Root Microcode.
Formal Methods in System Design 14,
pp. 75–125,
doi:10.1023/A:1008669628911.
David M. Russinoff (2007):
A Mathematical Approach to RTL Verification.
In: 19th International Conference on Computer Aided Verification,
doi:10.1007/978-3-540-73368-3_2.
Available at: http://www.russinoff.com/papers/cav/.
David M. Russinoff (2009):
A Mechanically Verified Commercial SRT Divider.
In: Design and Verification of Microprocessor Systems for High-Assurance Applications.
Springer,
pp. 23–63.
David M. Russinoff & Arthur Flatau (2000):
Mechanical Verification of Register-Transfer Logic: A Floating-Point Multiplier.
In: Computer-Aided Reasoning: ACL2 Case Studies.
Kluwer,
pp. 201–232.
Anna Slobodová, Jared Davis, Sol Swords & Warren Hunt (2011):
A Flexible Formal Verification Framework for Industrial Scale Validation.
In: Formal Methods and Models for Codesign (MEMOCODE),
pp. 89–97,
doi:10.1109/MEMCOD.2011.5970515.
Anna Slobodová & Krishna Nagalla (2004):
Formal verification of floating point multiply add on Itanium processors.
In: Fifth International Workshop on Designing Correct Circuits.
ETAPS,
pp. 144–156.
Dimitri Tan, Carl Lemonds & Michael J. Schulte (2009):
Low-Power Multiple-Precision Iterative Floating-Point Multiplier with SIMD Support.
IEEE Trans. Computers 58(2),
pp. 175–187,
doi:10.1109/TC.2008.203.
eptcs@eptcs.org