Efficient control state-space search

被引：1

作者：

Aziz, A ^{[1
]}

Kukula, J

Shiple, T

Yuan, J

机构：

[1] Univ Texas, Dept Elect & Comp Engn, Austin, TX 78712 USA

[2] Synopsys Inc, Adv Technol Grp, Mountain View, CA 94043 USA

[3] Motorola Inc, Austin, TX 78729 USA

来源：

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS | 2001年 / 20卷 / 02期

基金：

美国国家科学基金会;

关键词：

BDDs; coverage; digital hardware; reachability analysis; verification;

D O I：

10.1109/43.908475

中图分类号：

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

学科分类号：

0812 ;

摘要：

We develop algorithms for exploring the reachable State-space of hardware designs that can be partitioned into control and data. The core procedure is a symbolic algorithm that tries to visit as many controller states as is computationally feasible. Here, we describe heuristics for making this traversal efficient. Experiments demonstrate that our approach is capable of achieving significantly greater coverage of the control state-space than conventional symbolic reachability analysis.

引用

页码：332 / 336

页数：5

共 10 条

[1]

BRAYTON RK, 1996, P 8 INT C COMP AID V, P428

[2]

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

[3]

CHO HW, 1994, PR IEEE COMP DESIGN, P236, DOI 10.1109/ICCD.1994.331896

[4]

Ganai M. K., 1999, Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361), P385, DOI 10.1109/DAC.1999.781346

[5]

LIN B, 1991, P INT C COMP DES CAM

[6]

MCMILLAN KL, 1993, SYMBOLIC MODEL CHECK

[7]

Ravi K, 1998, 1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS, P445, DOI 10.1109/DAC.1998.724513

[8]

YUAN J, 1999, P INT C COMP AID DES, P584

[9]

[No title captured]

[10]

[No title captured]

← 1 →