Functional Equivalence Verification Tools in High-Level Synthesis Flows

被引：21

作者：

Mathur, Anmol ^{[1
]}

Clarke, Edmund ^{[2
]}

Fujita, Masahiro ^{[3
]}

Urard, Pascal ^{[4
]}

机构：

[1] Calypto Design Syst, Santa Clara, CA 95054 USA

[2] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

[3] Univ Tokyo, Tokyo 1138654, Japan

[4] STMicroelectronics, Analog & Mixed Signals Grp, ST Technol R&D, Geneva, Switzerland

来源：

IEEE DESIGN & TEST OF COMPUTERS | 2009年 / 26卷 / 04期

关键词：

Algorithm design and analysis; Analytical models; Arrays; Computational modeling; Computer bugs; Correctness; Data mining; Design and test; Formal analysis; Functional equivalence; Logic gates; Sequential equivalence; System-level model;

D O I：

10.1109/MDT.2009.79

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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 © 2009 IEEE.

引用

页码：88 / 95

页数：8

共 12 条

[1]

Barrett C, 2007, LECT NOTES COMPUT SC, V4590, P298

[2]

Cadar Cristian, 2008, 8 USENIX OSDI SAN DI, P209

[3] A tool for checking ANSI-C programs [J].

Clarke, E ;

Kroening, D ;

Lerda, F .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2004, 2988 :168-176

[4] Counterexample-guided abstraction refinement for symbolic model checking [J].

Clarke, E ;

Grumberg, O ;

Jha, S ;

Lu, Y ;

Veith, H .

JOURNAL OF THE ACM, 2003, 50 (05) :752-794

[5] Verification of SpecC using predicate abstraction [J].

Clarke, Edmund ;

Jain, Himanshu ;

Kroening, Daniel .

FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (01) :5-28

[6] MultipleWord-Length High-Level Synthesis [J].

Coussy, Philippe ;

Lhairech-Lebreton, Ghizlane ;

Heller, Dominique .

EURASIP JOURNAL ON EMBEDDED SYSTEMS, 2008, (01)

[7]

Engler D., 2001, Operating Systems Review, V35, P57, DOI 10.1145/502059.502041

[8] Towards a C plus plus -based design methodology facilitating sequential equivalence checking [J].

Georgelin, Philippe ;

Krishnaswamy, Venkat .

43RD DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2006, 2006, :93-+

[9]

KROENING D, 2003, P DAC 2003, P368

[10]

Mathivanan Rangasamy, 2007, Journal of Poultry Science, V44, P198, DOI 10.2141/jpsa.44.198

← 1 2 →