@inproceedings(boulton,
 author       = {R. Boulton and A. Gordon and M. Gordon and J. Harrison and J. Herbert and J. Van Tassel},
 year         = {1992},
 title        = {Experience with Embedding Hardware Description Languages},
 booktitle    = {International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience},
 publisher    = {North-Holland/Elsevier},
 pages        = {129--156},
)
@inproceedings(dh,
 author       = {D. Hardin},
 year         = {2020},
 title        = {Put Me on the RAC},
 booktitle    = {ACL2 2020: 16th International Workshop on the ACL2 Theorem Prover and its Applications},
 address      = {Virtual Conference},
)
@incollection(centaur,
 author       = {W. Hunt and S. Swords and J. Davis and A. Slobadova},
 year         = {2010},
 title        = {Use of Formal Verification at Centaur Technology},
 editor       = {David S. Hardin},
 booktitle    = {Design and Verification of Microprocessor Systems for High-Assurance Applications},
 publisher    = {Springer},
 pages        = {65--88},
 doi          = {10.1007/978-1-4419-1539-9_3},
)
@book(flex,
 author       = {J. Levine},
 year         = {2009},
 title        = {Flex and Bison},
 publisher    = {O'Reilly Media},
)
@misc(ac,
 author       = {{Mentor Graphics Corp.}},
 title        = {Algorithmic {C} Datatypes},
 note         = {Available at \url{https://www.mentor.com/hls-lp/downloads/ac-datatypes}},
)
@misc(slec,
 author       = {{Mentor Graphics Corp.}},
 title        = {Sequential Logic Equivalence Checker},
 note         = {\url{https://www.mentor.com/products/fv/questa-slec}},
)
@inproceedings(oleary,
 author       = {J. O'Leary and D. Russinoff},
 year         = {2014},
 title        = {Modeling Algorithms in {SystemC} and {ACL2}},
 booktitle    = {ACL2 2014: 12th International Workshop on the ACL2 Theorem Prover and its Applications},
 address      = {Vienna},
 doi          = {10.4204/EPTCS.152.12},
 note         = {Available at \url{http://www.russinoff.com/papers/masc.html}},
)
@book(book,
 author       = {D. Russinoff},
 year         = {2018},
 title        = {Formal Verification of Floating-Point Hardware Design: A Mathematical Approach},
 publisher    = {Springer},
)
@inproceedings(amd,
 author       = {D. Russinoff and M. Kaufmann and E. Smith and R. 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},
 address      = {Paris},
)
@misc(hector,
 author       = {{Synopsys, Inc.}},
 title        = {Hector},
 note         = {\url{https://research.ibm.com/haifa/conferences/hvc2008/present/CarlPixleyHVC08.pdf}},
)