1. Robert K. Brayton, Gary D. Hachtel & Alberto L. Sangiovanni-Vincentelli (1990): Multilevel logic Synthesis. Proceedings of the IEEE 78(2), pp. 264–300, doi:10.1109/5.52213.
  2. Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel & Vadim Ryvchin (2010): Designers Work Less with Quality Formal Equivalence Checking. In: DVCon. ACM.
  3. C. A. J. van Eijk (1998): Sequential Equivalence Checking without State Space Traversal. In: DATE. IEEE Computer Society, pp. 618–623, doi:10.1109/Date.1998.655922.
  4. Evgueni I. Goldberg, Mukul R. Prasad & Robert K. Brayton (2001): Using SAT for Combinational Equivalence Checking. In: DATE, pp. 114–121, doi:10.1145/367072.367111.
  5. Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss & Ziyad Hanna (2004): Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. In: ICCAD. IEEE Computer Society / ACM, pp. 58–65, doi:10.1145/1112239.1112255.
  6. V. M. Achutha KiranKumar, Aarti Gupta & Rajnish Ghughal (2012): Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation IntelProcessor Graphics FPU. In: FMCAD. IEEE, pp. 149–156. Available at
  7. Carlos Ivan Castro Marquez, Marius Strum & Wang Jiang Chau (2013): Formal equivalence checking between high-level and RTL hardware designs. In: LATW. IEEE, pp. 1–6, doi:10.1109/LATW.2013.6562666.
  8. Alan Mishchenko, Satrajit Chatterjee, Robert K. Brayton & Niklas Eén (2006): Improvements to combinational equivalence checking. In: ICCAD. ACM, pp. 836–843, doi:10.1145/1233501.1233679.
  9. Marios C. Papaefthymiou & Kumar N. Lalgudi (1996): Fixed-phase retiming for low power design. In: ISLPED. IEEE, pp. 259–264, doi:10.1145/252493.252615.
  10. Carl Pixley (1992): A theory and implementation of sequential hardware equivalence. IEEE Trans. on CAD of Integrated Circuits and Systems 11(12), pp. 1469–1478, doi:10.1109/43.180261.
  11. Sherief Reda & A. Salem (2001): Combinational equivalence checking using Boolean satisfiability and binary decision diagrams. In: DATE, pp. 122–126, doi:10.1145/367072.367113.
  12. Nikhil Sharma, Gagan Hasteer & Venkat Krishnaswamy (2006): Sequential Equivalence Checking for RTL models. EETimes Now. Available at

Comments and questions to:
For website issues: