Combining simulation and formal verification for integrated circuit design validation

被引：0

作者：

Li, Lun ^{[1
]}

Szygenda, Stephen A. ^{[1
]}

Thornton, Mitchell A. ^{[1
]}

机构：

[1] So Methodist Univ, Dept Comp Sci & Engn, Dallas, TX 75206 USA

来源：

WMSCI 2005: 9TH WORLD MULTI-CONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL 4 | 2005年

关键词：

simulation; formal verification; circuit design; validation;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

The correct design of complex hardware continues to challenge engineers. Bugs in a design that are not uncovered in early design stage can be extremely expensive. Simulation is a predominantly used tool to validate a design in industry. Formal verification overcomes the weakness of exhaustive simulation by applying mathematical methodologies to validate a design. The work described here focuses upon a combinational technique that integrates the best characteristics of both simulation and formal verification methods to provide an effective design validation tool, referred as IDV. The novelty in this approach consists of three components, a circuit complexity analyzer, a partitioning tool and a coverage analysis unit. The circuit complexity analyzer and partitioning tool partition a large design and feed sub-components to different verification and/or simulation tools based upon known existing strengths of modem verification and simulation tools. The coverage analysis unit computes the coverage rate of design validation and improves the coverage by further partitioning. Various tools comprising IDV are evaluated and an example is used to illustrate the overall validation process. The overall process successfully validates the example to a high coverage rate within a short time. The experimental result shows that our approach is a very promising design validation method.

引用

页码：92 / 97

页数：6

共 24 条

[1]

ALUR R, 2001, P IEEE INT C SOFTW E

[2]

Aziz A, 1998, 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS, P615, DOI 10.1109/DAC.1998.724545

[3]

BLOEM R, 2000, P DAC

[4]

BRAYTON RK, VIS SYSTEM VERIFICAT

[5]

BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819

[6]

BURCH J, 2000, P ICCAD, P570

[7]

CHANDRA A, 1995, IEEE T VLSI, V3

[8] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].

CLARKE, EM ;

EMERSON, EA ;

SISTLA, AP .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263

[9]

Govindaraju S. G., 1999, Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), P312, DOI 10.1109/DAC.1999.781332

[10]

Hazelhurst S., 1997, Formal hardware verification. Methods and systems in comparison, P3

← 1 2 3 →