<bold>Refinement Strategies for Verification Methods Based on Datapath Abstraction</bold>

被引：13

作者：

Andraus, Zaher S. ^{[1
]}

Liffiton, Mark H. ^{[1
]}

Sakallah, Karem A. ^{[1
]}

机构：

[1] Univ Michigan, Dept Elect Engn & Comp Sci, Ann Arbor, MI 48109 USA

来源：

ASP-DAC 2006: 11TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, PROCEEDINGS | 2006年

基金：

美国国家科学基金会;

关键词：

D O I：

10.1109/ASPDAC.2006.1594639

中图分类号：

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

学科分类号：

0812 ;

摘要：

In this paper we explore the application of Counter-example-Guided Abstraction Refinement (CEGAR) in the context of microprocessor correspondence checking. The approach utilizes automatic datapath abstraction augmented with automatic refinement based on 1) localization, 2) generalization, and 3) minimal unsatisfiable subset (MUS) extraction. We introduce several refinement strategies and empirically evaluate their effectiveness on a set of microprocessor benchmarks. The data suggest that localization, generalization, and MUS extraction from both the abstract and concrete models are essential for effective verification. Additionally, refinement tends to converge faster when multiple MUses are extracted in each iteration.

引用

页码：19 / 24

页数：6

共 23 条

[1]

ACKERMAN W, 1954, SOLVABLE CASES DECIS

[2] Automatic abstraction and verification of Verilog models [J].

Andraus, ZS ;

Sakallah, KA .

41ST DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2004, 2004, :218-223

[3]

[Anonymous], LNCS

[4]

Barrett C, 1996, LECT NOTES COMPUT SC, V1166, P187, DOI 10.1007/BFb0031808

[5]

Bryant R.E, 2001, ACM Trans. Comput. Logic (TOCL), V2, P93

[6]

BRYANT RE, 2002, P CAV JUL

[7]

CHAUHAN P, FMCAD02

[8]

CLARKE EM, 2000, COMPUTER AIDED VERIF, P154, DOI DOI 10.1007/10722167_15

[9]

DAS S, 2001, 16 ANN IEEE S LOG CO

[10]

EEN N, 2005, SAT

← 1 2 3 →