Specification and Formal Verification of Power Gating in Processors

被引：0

作者：

Gharehbaghi, Amir Masoud ^{[1
]}

Fujita, Masahiro ^{[2
]}

机构：

[1] Univ Tokyo, Dept Elect Engn & Informat Syst, Tokyo, Japan

[2] Univ Tokyo, VLSI Design & Educ Ctr, Tokyo, Japan

来源：

PROCEEDINGS OF THE FIFTEENTH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN (ISQED 2014) | 2015年

关键词：

Processor Verification; Power Gating Verification; Formal Verification; MICROPROCESSORS;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a method for specification as well as efficient formal verification of power gating feature of processors. Given an instruction-set architecture model of a processor, as the golden model, and a detailed processor model with power gating feature, we propose an efficient method for equivalence checking of the two models using symbolic simulation and property checking. Our experimental results on a MIPS processor shows that our method reduces the verification time compared to the correspondence checking method at least by 3.4x.

引用

页码：604 / +

页数：2

共 50 条

[1] Error-Tolerant Processors: Formal Specification and Verification
Golnari, Ameneh
Vizel, Yakir
Malik, Sharad
[J]. 2015 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2015, : 286 - 293
[2] Formal verification of pipelined processors
Bryant, RE
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 1 - 4
[3] Selective State Retention Power Gating Based on Formal Verification
Greenberg, Shlomo
Rabinowicz, Joseph
Manor, Erez
[J]. IEEE TRANSACTIONS ON CIRCUITS AND SYSTEMS I-REGULAR PAPERS, 2015, 62 (03) : 807 - 815
[4] Formal specification and verification of VHDL
Bickford, M
Jamsek, D
[J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 310 - 326
[5] Formal Specification and Verification of CRDTs
Zeller, Peter
Bieniusa, Annette
Poetzsch-Heffter, Arnd
[J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, 2014, 8461 : 33 - 48
[6] FORMAL FOUNDATION FOR SPECIFICATION AND VERIFICATION
LAMPORT, L
SCHNEIDER, FB
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 190 : 203 - 285
[7] Formal verification system for pipelined processors
Shonai, T
Shimizu, T
[J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1996, E79A (06) : 883 - 891
[8] RTL formal verification of embedded processors
Bavonparadon, P
Chongstitvatana, P
[J]. IEEE ICIT' 02: 2002 IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL TECHNOLOGY, VOLS I AND II, PROCEEDINGS, 2002, : 667 - 672
[9] A FORMAL VERIFICATION ALGORITHM FOR PIPELINED PROCESSORS
SHONAI, T
SHIMIZU, T
[J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1995, E78A (05) : 618 - 631
[10] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
JOYCE, JJ
[J]. MICROPROCESSING AND MICROPROGRAMMING, 1988, 24 (1-5): : 371 - 378

← 1 2 3 4 5 →