Automatic generation of assertions for formal verification of PowerPC™ microprocessor arrays using symbolic trajectory evaluation

被引：0

作者：

Wang, LC ^{[1
]}

Abadir, MS ^{[1
]}

Krishnamurthy, N ^{[1
]}

机构：

[1] Motorola Inc, Somerset PowerPC Design Ctr, Austin, TX USA

来源：

1998 DESIGN AUTOMATION CONFERENCE, PROCEEDINGS | 1998年

关键词：

D O I：

暂无

中图分类号：

T [工业技术];

学科分类号：

08 ;

摘要：

For verifying complex sequential blocks such as microprocessor embedded arrays, the formal method of symbolic trajectory evaluation (STE) has achieved great success in the past [[3], [5], [6]]. Past STE methodology for arrays requires manual creation of "assertions" to which both RTL view and the actual design should be equivalent. In this paper, we describe a novel method to automate the assertion creation process which improves the efficiency and the quality of array verification. Encouraging results on recent PowerPC arrays will be presented.

引用

页码：534 / 537

页数：4

共 50 条

[41] Next-Generation Automatic Human-Readable Proofs Enabling Polynomial Formal Verification
Drechsler, Rolf
Schnieber, Martha
[J]. 2023 21ST ACM-IEEE INTERNATIONAL SYMPOSIUM ON FORMAL METHODS AND MODELS FOR SYSTEM DESIGN, MEMOCODE, 2023, : 122 - 125
[42] Test Image Generation using Segmental Symbolic Evaluation
Jameel, Tahir
Lin, Mengxiang
[J]. INTERNATIONAL JOURNAL OF NETWORKED AND DISTRIBUTED COMPUTING, 2014, 2 (03) : 135 - 147
[43] DSP core verification using automatic test case generation
Glökler, T
Bitterlich, S
Meyr, H
[J]. 2000 IEEE INTERNATIONAL CONFERENCE ON ACOUSTICS, SPEECH, AND SIGNAL PROCESSING, PROCEEDINGS, VOLS I-VI, 2000, : 3271 - 3274
[44] Formal verification of a snoop-based cache coherence protocol using symbolic model checking
Srinivasan, S
Chhabra, PS
Jaini, PK
Aziz, A
John, L
[J]. TWELFTH INTERNATIONAL CONFERENCE ON VLSI DESIGN, PROCEEDINGS, 1999, : 288 - 293
[45] Automatic support for verification of secure transactions in distributed environment using symbolic model checking
Di Sciascio, E
Donini, FM
Mongiello, M
Piscitelli, G
[J]. ITI 2001: PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY INTERFACES, 2001, : 447 - 454
[46] A Candid Industrial Evaluation of Formal Software Verification using Model Checking
Bennion, Matthew
Habli, Ibrahim
[J]. 36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE COMPANION 2014), 2014, : 175 - 184
[47] Symbolic Trajectory Evaluation: The Primary Validation Vehicle for Next Generation Intel® Processor Graphics FPU
KiranKumar, M. Achutha, V
Gupta, Aarti
Ghughal, Rajnish
[J]. PROCEEDINGS OF THE 12TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD 2012), 2012, : 149 - 156
[48] Automatic Generation of Simulation Workflows for System Verification using XDSM Representation
Hammadi, Moncef
Patalano, Stanislao
[J]. 2017 IEEE INTERNATIONAL SYMPOSIUM ON SYSTEMS ENGINEERING (ISSE 2017), 2017, : 347 - 352
[49] Automatic Generation of Test Cases from Formal Specifications using Mutation Testing
Jaramillo Cajica, Roman
Gonzalez Torres, Raul Ernesto
Mejia Alvarez, Pedro
[J]. 2021 18TH INTERNATIONAL CONFERENCE ON ELECTRICAL ENGINEERING, COMPUTING SCIENCE AND AUTOMATIC CONTROL (CCE 2021), 2021,
[50] Automatic test generation from semi-formal specifications for functional verification of System-on-Chip designs
Kirchsteiger, Christoph M.
Grinschgl, Johannes
Trummer, Christoph
Steger, Christian
Weiss, Reinhold
Pistauer, Markus
[J]. 2008 2ND ANNUAL IEEE SYSTEMS CONFERENCE, 2008, : 260 - +

← 1 2 3 4 5 →