Bibliography

ACL205
ACL2 home page.
www.cs.utexas.edu/users/moore/acl2/.

algc
Algorithmic C Datatypes, Calypto Design Systems, Inc.
http://www.eit.lth.se/fileadmin/eit/courses/etin45/Lab_Files/ac_datatypes_ref_uv.pdf

BOO51
Booth, A.D., A Signed Binary Multiplication Technique, Quart. J. Mech. Appl. Math. 4, Part 2, 1951.

1
Ercegovac, Milos D. and Tomás Lang, Division and Square Root Digit-Recurrence Algorithms and Implementations, Kluwer Academic Publishers, 1994.

GAM99
Gamboa, Ruben, Mechanically Verifying Real-Valued Algorithms in ACL2, Ph.D. dissertation, Dept. of Computer Sciences, U. of Texas at Austin, May, 1999.

HAR00
Harrison, John, Formal Verification of IA-64 Division Algorithms, Theorem Proving in Higher Order Logics: 13th International Conference, ed. M. Aagaard and J. Harrison, Lecture Notes in Computer Science, Vol. 1869, Springer-Verlag, 2000.

HECTOR
Hector Web site,
www.synopsys.com/Tools/Verification/FunctionalVerification/Pages/hector.aspx.

IEEE85
Institute of Electrical and Electronic Engineers, IEEE Standard for Binary Floating Point Arithmetic, Std. 754-1985, New York, NY, 1985.

IEEE08
Institute of Electrical and Electronic Engineers, IEEE Standard for Floating Point Arithmetic, Std. 754-2008, New York, NY, 2008.

KAU00a
Kaufmann, M., P. Manolios, and J S. Moore, Computer-Aided Reasoning: An Approach. Kluwer Academic Press, 2000.

KAU00b
Kaufmann, M., P. Manolios, and J S. Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, 2000.

KAU00d
Kaufmann, M. and D.M. Russinoff, Verification of Pipeline Circuits, Proceedings ACL2 Workshop 2000, Oct. 2000.
www.cs.utexas.edu/users/moore/acl2/workshop-2000/.

KAU03
Kaufmann, M., A Tool for Simplifying Files of acl2 Definitions, Proceedings ACL2 Workshop 2003, July 2003.
www.cs.utexas.edu/users/moore/acl2/workshop-2003/.

KLI72
Kline, Morris, Mathematical Thought from Ancient to Modern Times, Oxford University Press, 1972.

KOR93
Koren, Israel, Computer Arithmetic Algorithms, 2nd edition, A.K. Peters, 1993.

MAR90
Markstein, Peter W., Computation of Elementary Functions on the IBM RISC System/6000 Processor, IBM Journal of Research and Development, 34:1, Jan. 1990.

MOO98
Moore, J, T. Lynch, and M. Kaufmann, A mechanically checked proof of the correctness of the kernel of the $ AMD5_{K}86$ floating point division algorithm, IEEE Transactions on Computers, 47:9, September, 1998.

OLE14
O'Leary, J.W., and D.M. Russinoff, Modeling Algorithms in SystemC and ACL2, ACL2 2014: 12th International Workshop on the ACL2 Theorem Prover and its Applications, Vienna, July 2014.
www.russinoff.com/papers/masc.html.

ROB58
Robertson, J.E., A New Class of Digital Division Methods, IRE Transactions on Electronic Computers, EC-7, 1958.

RUS98
Russinoff, D.M, A mechanically checked proof of IEEE compliance of the AMD-K7 floating point multiplication, division, and square root instructions, London Mathematical Society Journal of Computation and Mathematics (1), 148-200, December, 1998.
www.russinoff.com/papers/k7-div-sqrt.html.

RUS99
Russinoff, D.M., A mechanically checked proof of IEEE compliance of the AMD-K5 floating point square root microcode, Formal Methods in System Design 14, 75-125 (1999).
www.russinoff.com/papers/fsqrt.html.

RUS00a
Russinoff, D.M., A case study in formal verification of register-transfer logic with ACL2: the floating point adder of the AMD Athlon processor, invited paper, FMCAD 2000.
www.russinoff.com/papers/fadd.html.

RUS00b
Russinoff, D.M. and A. Flatau, RTL verification: a floating-point multiplier, in [KAU00b], pp. 201-232.
www.russinoff.com/papers/acl2.html.

slec
Sequential Logic Equivalence Check, Mentor Graphics Corp.
https://www.mentor.com/products/fv/questa-slec

STE90
Steele, G.L., Jr., Common Lisp The Language, 2nd edition, Digital Press, 1990.

TOC58
Tocher, K.D., Techniques of Multiplication and Division for Automatic Binary Computers, Quarterly Journal of Mechanics and Applied Mathematics, Vol. 2, 1958.



David Russinoff 2017-08-01