This Article 
 Bibliographic References 
 Add to: 
Functional Equivalence Verification Tools in High-Level Synthesis Flows
July/August 2009 (vol. 26 no. 4)
pp. 88-95
Anmol Mathur, Calypto Design Systems
Masahiro Fujita, University of Tokyo
Edmund Clarke, Carnegie Mellon University
Pascal Urard, STMicroelectronics

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

1. P. Coussy and A. Morawiec eds., High-Level Synthesis: From Algorithm to Digital Circuit, Springer, 2008.
2. D. Engler et al., "Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code," Proc. ACM SIGOPS Operating Systems Rev., vol. 35, no. 5, 2001, pp. 57-72.
3. C. Cadar, D. Dunbar, and D. Engler Klee, "Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs," Proc. Operating System Design and Implementation (OSDI 08), Usenix Assoc., 2008, pp. 209-224.
4. E.M. Clarke, D. Kroening, and F. Lerda, "A Tool for Checking ANSI-C Programs," Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 04), LNCS 2988, Springer-Verlag, 2004, pp. 168-176.
5. M. Moskewicz et al., "Chaff: Engineering an Efficient SAT Solver," Proc. 39th Design Automation Conf. (DAC 01), ACM Press, 2001, pp. 530-535.
6. C. Barrett and C. Tinelli, "CVC3," Proc. 19th Int'l Conf. Computer Aided Verification (CAV 07), LNCS 4590, Springer-Verlag, 2007, pp. 298-302.
7. E.M. Clarke et al., "Counterexample-Guided Abstraction Refinement for Symbolic Model Checking," J. ACM, vol. 50, no. 5, 2003, pp. 752-794.
8. P. Georgelin and V. Krishnaswamy, "Towards a C++-Based Design Methodology Facilitating Sequential Equivalence Checking," Proc. 43rd Design Automation Conf. (DAC 06), ACM Press, 2006, pp. 93-96.
9. D. Kroening, E. Clarke, and K. Yorav, "Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking," Proc. 40th Design Automation Conf. (DAC 03), ACM Press, 2003, pp. 368-371.
10. E.M. Clarke, H. Jain, and D. Kroening, "Verification of SpecC Using Predicate Abstraction," Formal Methods in System Design, vol. 30, no. 1, 2007, pp. 5-28.
11. A. Mathur and V. Krishnaswamy, "Design for Verification in System Level Models and RTL," Proc. 44th Design Automation Conf. (DAC 07), ACM Press, 2007, pp. 193-198.
12. T. Matsumoto, H. Saito, and M. Fujita, "Equivalence Checking of C Programs by Locally Performing Symbolic Simulation on Dependence Graphs," Proc. 7th Int'l Symp. Quality Electronic Design (ISQED 06), IEEE CS Press, 2006, pp. 370-375.

Index Terms:
system-level model, sequential equivalence, functional equivalence, design and test, formal analysis, correctness
Anmol Mathur, Masahiro Fujita, Edmund Clarke, Pascal Urard, "Functional Equivalence Verification Tools in High-Level Synthesis Flows," IEEE Design & Test of Computers, vol. 26, no. 4, pp. 88-95, July-Aug. 2009, doi:10.1109/MDT.2009.79
Usage of this product signifies your acceptance of the Terms of Use.