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 条

[1] A practical approach to the formal verification of SoC's with symbolic model-checking
Dumitrescu, E
SYSTEM-ON-CHIP FOR REAL-TIME APPLICATIONS, 2003, : 98 - 110
[2] Verification of CTLBDI Properties by Symbolic Model Checking
Chen, Ran
Zhang, Wenhui
2019 26TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), 2019, : 102 - 109
[3] Symbolic Model Checking Epistemic Strategy Logic
Huang, Xiaowei
Van der Meyden, Ron
PROCEEDINGS OF THE TWENTY-EIGHTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2014, : 1426 - 1432
[4] Formal Verification of SDG via Symbolic Model Checking
Ning, Ning
Zhang, Jun
Gao, Xiang-Yang
Xue, Jing
ICICTA: 2009 SECOND INTERNATIONAL CONFERENCE ON INTELLIGENT COMPUTATION TECHNOLOGY AND AUTOMATION, VOL IV, PROCEEDINGS, 2009, : 521 - 524
[5] SYMBOLIC MODEL CHECKING FOR SEQUENTIAL-CIRCUIT VERIFICATION
BURCH, JR
CLARKE, EM
LONG, DE
MCMILLAN, KL
DILL, DL
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1994, 13 (04) : 401 - 424
[6] Symbolic model checking and simulation with temporal assertions
Weiss, RJ
Ruf, J
Kropf, T
Rosenstiel, W
ADVANCES IN DESIGN AND SPECIFICATION LANGUAGES FOR SOCS: SELECTED CONTRIBUTIONS FROM FDL'04, 2005, : 275 - 291
[7] Verification of pipelined microprocessors by correspondence checking in symbolic ternary simulation
Velev, MN
Bryant, RE
1998 INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 1998, : 200 - 212
[8] Symbolic model checking
McMillan, KL
VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
[9] A symbolic model checking approach in formal verification of distributed systems
Souri, Alireza
Rahmani, Amir Masoud
Navimipour, Nima Jafari
Rezaei, Reza
HUMAN-CENTRIC COMPUTING AND INFORMATION SCIENCES, 2019, 9 (01):
[10] Design verification of Web Applications using symbolic model checking
Di Sciascio, E
Donini, FM
Mongiello, M
Totaro, R
Castelluccia, D
WEB ENGINEERING, PROCEEDINGS, 2005, 3579 : 69 - 74

← 1 2 3 4 5 →