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 条

[31] Modeling and verification of out-of-order microprocessors in UCLID
Lahiri, SK
Seshia, SA
Bryant, RE
FORMAL METHODS IN COMPUTER-AIDED DESIGN, PROCEEDINGS, 2002, 2517 : 142 - 159
[32] MU-SPEED - A SYSTEM FOR THE SPECIFICATION AND VERIFICATION OF MICROPROCESSORS
COLLAVIZZA, H
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 577 : 607 - 608
[33] Automated Debugging of Counterexamples in Formal Verification of Pipelined Microprocessors
Velev, Miroslav N.
Gao, Ping
2012 17TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE (ASP-DAC), 2012, : 689 - 694
[34] Deductive verification of advanced out-of-order microprocessors
Lahiri, SK
Bryant, RE
COMPUTER AIDED VERIFICATION, 2003, 2725 : 341 - 354
[35] Directed-logical testing for functional verification of microprocessors
Katelman, Michael
Meseguer, Jose
Escobar, Santiago
MEMOCODE'08: SIXTH ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2008, : 89 - +
[36] A methodology for the formal verification of RISC microprocessors - A functional approach
Merniz, S.
Benmohammed, M.
2007 IEEE/ACS INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS, VOLS 1 AND 2, 2007, : 492 - +
[37] PROGRAM VERIFICATION FOR MICROPROCESSORS THROUGH PETRI NET MODELING
HURA, GS
ATWOOD, JW
MICROELECTRONICS AND RELIABILITY, 1985, 25 (05): : 1001 - 1010
[38] An efficient verification method for microprocessors based on the virtual machine
An, JF
Fan, XY
Zhang, SB
Wang, DH
EMBEDDED SOFTWARE AND SYSTEMS, 2005, 3605 : 514 - 521
[39] Fast and Scalable Hybrid Functional Verification and Debug with Dynamically Reconfigurable Co-simulation
Banerjee, Somnath
Gupta, Tushar
2012 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2012, : 115 - 122
[40] A hybrid simulation platform for learning microprocessors
Papazoglou, Panayotis M.
COMPUTER APPLICATIONS IN ENGINEERING EDUCATION, 2018, 26 (03) : 655 - 674

← 1 2 3 4 5 →