Specification and formal verification of power gating in processors

Author

Gharehbaghi, Amir Masoud ; Fujita, Masayuki

Author_Institution

Dept. of Electr. Eng. & Inf. Syst., Univ. of Tokyo, Tokyo, Japan

fYear

2014

fDate

3-5 March 2014

Firstpage

604

Lastpage

610

Abstract

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.

Keywords

formal specification; formal verification; instruction sets; microprocessor chips; MIPS processor; correspondence checking method; equivalence checking; formal verification; instruction-set architecture model; power gating feature; processor model; property checking; symbolic simulation; verification time reduction; Formal verification; Latches; Load modeling; Logic gates; Power demand; Program processors; Registers; Formal Verification; Power Gating Verification; Processor Verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Quality Electronic Design (ISQED), 2014 15th International Symposium on

Conference_Location

Santa Clara, CA

Print_ISBN

978-1-4799-3945-9

Type

conf

DOI

10.1109/ISQED.2014.6783382

Filename

6783382