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