Title :
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
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;
Conference_Titel :
Quality Electronic Design (ISQED), 2014 15th International Symposium on
Conference_Location :
Santa Clara, CA
Print_ISBN :
978-1-4799-3945-9
DOI :
10.1109/ISQED.2014.6783382
