Scalable hybrid verification of complex microprocessors

被引：0

作者：

Mneimneh, M ^{[1
]}

Aloul, F ^{[1
]}

Weaver, C ^{[1
]}

Chatterjee, S ^{[1
]}

Sakallah, K ^{[1
]}

Austin, T ^{[1
]}

机构：

[1] Univ Michigan, Ann Arbor, MI 48109 USA

来源：

38TH DESIGN AUTOMATION CONFERENCE PROCEEDINGS 2001 | 2001年

关键词：

D O I：

暂无

中图分类号：

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

学科分类号：

0812 ;

摘要：

We introduce a new verification methodology for modem microprocessors that uses a simple checker processor to validate the execution of a companion high-performance processor. The checker can be viewed as an at-speed emulator that is formally verified to be compliant to an ISA specification. This verification approach enables the practical deployment of formal methods without impacting overall performance.

引用

页码：41 / 46

页数：6

共 50 条

[41] Extraction of hybrid complex wavelet features for the verification of handwritten numerals
Zhang, P
Bui, TD
Suen, CY
NINTH INTERNATIONAL WORKSHOP ON FRONTIERS IN HANDWRITING RECOGNITION, PROCEEDINGS, 2004, : 347 - 352
[42] Scalable Verification of Probabilistic Networks
Smolka, Steffen
Kumar, Praveen
Kahn, David M.
Foster, Nate
Hsu, Justin
Kozen, Dexter
Silva, Alexandra
PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 190 - 203
[43] ADVANCED MICROPROCESSORS REQUIRE COMPLEX APPROACH
BLAKEMORE, D
COMPUTER DESIGN, 1987, 26 (11): : 85 - 90
[44] Microprocessors lead the way in complex design
Levitt, ME
IEEE DESIGN & TEST OF COMPUTERS, 1997, 14 (01): : 8 - 9
[45] Divide and conquer approach to functional verification of PowerPC(TM) microprocessors
Roth, C
Tyler, J
Jagodik, P
Nguyen, H
8TH IEEE INTERNATIONAL WORKSHOP ON RAPID SYSTEM PROTOTYPING, PROCEEDINGS: SHORTENING THE PATH FROM SPECIFICATION TO PROTOTYPE, 1997, : 128 - 133
[46] 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
[47] Functional formal verification on designs of pSeries microprocessors and communication subsystems
Gott, RM
Baumgartner, JR
Roessler, P
Joe, SI
IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 2005, 49 (4-5) : 565 - 580
[48] High level formal verification of next-generation microprocessors
Schubert, T
40TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2003, 2003, : 1 - 6
[49] Efficient translation of boolean formulas to CNF in formal verification of microprocessors
Velev, MN
ASP-DAC 2004: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2004, : 310 - 315
[50] PROGRAM VERIFICATION FOR MICROPROCESSORS THROUGH PETRI NET MODELING.
Hura, G.S.
Atwood, J.W.
Microelectronics Reliability, 1985, 25 (05): : 1001 - 1010

← 1 2 3 4 5 →