Editor's note: High-level synthesis facilitates the use of formal verification methodologies that
check the equivalence of the generated RTL model against the original source specification.
The article provides an overview of sequential equivalence checking techniques, its
challenges, and successes in real-world designs.—Andres Takach, Mentor Graphics