@article(paper7,
 author       = "Robert K. Brayton and Gary D. Hachtel and Alberto L. Sangiovanni-Vincentelli",
 year         = "1990",
 title        = "Multilevel logic Synthesis",
 journal      = "Proceedings of the IEEE",
 volume       = "78",
 number       = "2",
 pages        = "264--300",
 doi          = "10.1109/5.52213",
)
@inproceedings(paper4,
 author       = "Orly Cohen and Moran Gordon and Michael Lifshits and Alexander Nadel and Vadim Ryvchin",
 year         = "2010",
 title        = "Designers Work Less with Quality Formal Equivalence Checking",
 booktitle    = "DVCon",
 publisher    = "ACM",
)
@inproceedings(paper8,
 author       = "C. A. J. van Eijk",
 year         = "1998",
 title        = "Sequential Equivalence Checking without State Space Traversal",
 booktitle    = "DATE",
 publisher    = "IEEE Computer Society",
 pages        = "618--623",
 doi          = "10.1109/Date.1998.655922",
)
@inproceedings(paper12,
 author       = "Evgueni I. Goldberg and Mukul R. Prasad and Robert K. Brayton",
 year         = "2001",
 title        = "Using SAT for Combinational Equivalence Checking",
 booktitle    = "DATE",
 pages        = "114--121",
 doi          = "10.1145/367072.367111",
)
@inproceedings(paper3,
 author       = "Zurab Khasidashvili and Marcelo Skaba and Daher Kaiss and Ziyad Hanna",
 year         = "2004",
 title        = "Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints",
 booktitle    = "ICCAD",
 publisher    = "IEEE Computer Society / ACM",
 pages        = "58--65",
 doi          = "10.1145/1112239.1112255",
)
@inproceedings(paper9,
 author       = "V. M. Achutha KiranKumar and Aarti Gupta and Rajnish Ghughal",
 year         = "2012",
 title        = "Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel{\textregistered } Processor Graphics FPU",
 booktitle    = "FMCAD",
 publisher    = "IEEE",
 pages        = "149--156",
 url          = "http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6462567",
)
@inproceedings(paper6,
 author       = "Carlos Ivan Castro Marquez and Marius Strum and Wang Jiang Chau",
 year         = "2013",
 title        = "Formal equivalence checking between high-level and RTL hardware designs",
 booktitle    = "LATW",
 publisher    = "IEEE",
 pages        = "1--6",
 doi          = "10.1109/LATW.2013.6562666",
)
@inproceedings(paper11,
 author       = "Alan Mishchenko and Satrajit Chatterjee and Robert K. Brayton and Niklas E{\'e}n",
 year         = "2006",
 title        = "Improvements to combinational equivalence checking",
 booktitle    = "ICCAD",
 publisher    = "ACM",
 pages        = "836--843",
 doi          = "10.1145/1233501.1233679",
)
@inproceedings(paper2,
 author       = "Marios C. Papaefthymiou and Kumar N. Lalgudi",
 year         = "1996",
 title        = "Fixed-phase retiming for low power design",
 booktitle    = "ISLPED",
 publisher    = "IEEE",
 pages        = "259--264",
 doi          = "10.1145/252493.252615",
)
@article(paper1,
 author       = "Carl Pixley",
 year         = "1992",
 title        = "A theory and implementation of sequential hardware equivalence",
 journal      = "IEEE Trans. on CAD of Integrated Circuits and Systems",
 volume       = "11",
 number       = "12",
 pages        = "1469--1478",
 doi          = "10.1109/43.180261",
)
@inproceedings(paper10,
 author       = "Sherief Reda and A. Salem",
 year         = "2001",
 title        = "Combinational equivalence checking using Boolean satisfiability and binary decision diagrams",
 booktitle    = "DATE",
 pages        = "122--126",
 doi          = "10.1145/367072.367113",
)
@misc(paper5,
 author       = "Nikhil Sharma and Gagan Hasteer and Venkat Krishnaswamy",
 year         = "2006",
 title        = "Sequential Equivalence Checking for {RTL} models",
 howpublished = "EETimes Now",
 url          = "http://www.eetimes.com/document.asp?doc_id=1271433",
)