Symbolic simulation as a simplifying strategy for SoC verification with symbolic model checking

被引：0

作者：

Dumitrescu, E ^{[1
]}

Borrione, D ^{[1
]}

机构：

[1] TIMA Lab, Grenoble, France

来源：

3RD IEEE INTERNATIONAL WORKSHOP ON SYSTEM-ON-CHIP FOR REAL-TIME APPLICATIONS, PROCEEDINGS | 2003年

关键词：

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

The successful application of model-checking to industrial designs requires methods for reducing the complexity of the model. This paper presents an original strategy, for a well-identified class of circuit behaviors; by running an appropriate symbolic simulation pattern before the actual proof of a temporal formula, an important FSM model simplification can be obtained The actual model reduction step is formalized and illustrated. This method has been implemented within the CMU version of the SMV model-checking tool and validated on a large industrial design.

引用

页码：378 / 383

页数：6

共 50 条

[21] Sequential equivalence checking by symbolic simulation
Ritter, G
FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2000, 1954 : 423 - 442
[22] Verification of a logically controlled, solids transport system using symbolic model checking
Probst, ST
Powers, GJ
Long, DE
Moon, I
COMPUTERS & CHEMICAL ENGINEERING, 1997, 21 (04) : 417 - 429
[23] RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking
Vakilotojar, V
Beerel, PA
INTEGRATION-THE VLSI JOURNAL, 1997, 24 (01) : 19 - 35
[24] RTL verification of timed asynchronous and heterogeneous systems using symbolic model checking
Vakilotojar, V
Beerel, PA
PROCEEDINGS OF THE ASP-DAC '97 - ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE 1997, 1996, : 181 - 188
[25] Composite model-checking: Verification with type-specific symbolic representations
Bultan, T
Gerber, R
League, C
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2000, 9 (01) : 3 - 50
[26] Coverage estimation using transition perturbation for symbolic model checking in hardware verification
Xu, Xingwen
Kimura, Shinji
Horikawa, Kazunari
Tsuchiya, Takehiko
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2006, E89A (12) : 3451 - 3457
[27] Verification of a logically controlled, solids transport system using symbolic model checking
Probst, S.T.
Powers, G.J.
Long, D.E.
Moon, I.
Computers and Chemical Engineering, 1997, 21 (04): : 417 - 429
[28] VECTORIZED SYMBOLIC MODEL CHECKING OF COMPUTATION TREE LOGIC FOR SEQUENTIAL MACHINE VERIFICATION
HIRAISHI, H
HAMAGUCHI, K
OCHI, H
YAJIMA, S
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 214 - 224
[29] Symbolic model checking for probabilistic processes
Baier, C
Clarke, EM
Hartonas-Garmhausen, V
Kwiatkowska, M
Ryan, M
AUTOMATA, LANGUAGES AND PROGRAMMING, 1997, 1256 : 430 - 440
[30] Eager Abstraction for Symbolic Model Checking
McMillan, Kenneth L.
COMPUTER AIDED VERIFICATION (CAV 2018), PT I, 2018, 10981 : 191 - 208

← 1 2 3 4 5 →