Selective State Retention Power-Gating based on Complete Property Checking

Abstract

I den nåværende tiden av Dark Silicon, må visse regioner i Systems-on-Chip (SoC) være inaktive på et bestemt tidspunkt for å sikre systemdrift innenfor strømbudsjettet. Følgelig brukes effektive teknikker for strømsparing som Power-Gating (PG). Imidlertid, ved å bruke denne teknikken, går systemtilstanden tapt i standby-modus, slik at tilstandsretensjon kreves for systemgjenopptak. State Retention Power-Gating (SRPG) er en effektiv teknikk for å implementere retensjon, der registre blir drevet selv i standby-modus for å tillate rask systemgjenopptakelse. Likevel skal retensjon brukes selektivt, dvs. bare på de essensielle registerene som er nødvendige for å bestemme systemtilstanden, for å redusere den totale innførte overhead av areal, kraft og ledninger. Teknikker for Selective State Retention Power-Gating (SSRPG) er fortsatt et spørsmål om forskning, og så langt er det ingen standardteknikker. Complete Property Checking (CPC) er en formell verifiseringsteknikk for å bevise at et system fullt ut oppfyller den nødvendige oppførselen ved å formelt trekke ut atferdsmodusene og operasjonene fra systemspesifikasjonene. I dette arbeidet foreslås en ny tilnærming for SSRPG basert på CPC. I denne teknikken analyseres hvert register i systemet gjennom den formelle abstraksjonen, med tanke på forholdene der systemet får lov til å gå i standby-modus. Da krever ikke alle registre som ikke er vesentlige, dvs. registre som aldri blir lest eller skrevet før de er lest etter at de har forlatt standby-modus, oppbevaring. Den foreslåtte metoden ble opprinnelig brukt på to timer-IPer og en Fist In First Out (FIFO ) IP med et parallelt / serielt grensesnitt som er designet for formålene med denne undersøkelsen. Deretter har den blitt brukt på en Direct Memory Access (DMA) Channel Peripheral Controller IP som eies av Nordic Semiconductor ASA for å evaluere metodens skalerbarhet ytterligere. Dessuten er alle egenskaper beskrevet ved hjelp av det industrielle standardspråket SystemVerilog Assertions (SVA), og alle formelle analyser er utført ved hjelp av vcFormal, et kommersielt Electronic Design Automation (EDA) verktøy fra Synopsys. Årsaken til dette er å lette den potensielle anvendelsen av den foreslåtte teknikken i utviklingen av industrielle applikasjoner, spesielt der CPC allerede er brukt som en del av verifiseringsstrømmen. Samlet sett viser resultatene av dette forskningsarbeidet at den foreslåtte teknikken med hell har identifisert registrene som krever oppbevaring for alle de analyserte systemene. Også de oppnådde utførelsestidene for de formelle analysene per enhet og viser i gjennomsnitt en logaritmisk vekst med hensyn til økningen i størrelse og kompleksitet av de forskjellige analyserte systemene.

In the current era of the Dark Silicon, certain regions of the Systems-on-Chip (SoC) need to be inactive at a certain point in time to ensure system operation within the power budget. Consequently, efficient techniques for power saving such as Power-Gating (PG) are used. However, by using this technique the system state is lost during standby mode, thus State retention is required for system resumption. State Retention Power-Gating (SRPG) is an efficient technique to implement retention, where registers are powered even during standby mode in order to allow fast system resumption. Nevertheless, retention is to be applied selectively, i.e., only to the essential registers which are required to determine the system state, to reduce the total introduced overhead of area, power and wiring. Techniques for Selective State Retention Power-Gating (SSRPG) are still a matter of research and so far there is no standard techniques. Complete Property Checking (CPC) is a formal verification technique to prove that a system fully fulfills the required behavior by formally abstracting the behavioral modes and operations from the system specifications. In the present work, a new approach for SSRPG based on CPC is proposed. In this technique, each register of the system is analyzed throughout the formal abstraction, considering the conditions in which the system is allowed to enter standby mode. Then, all registers that are not essential, i.e., registers that are never read or written before read after leaving the standby mode, do not require retention.The proposed method has been initially applied to two Timer IPs and a Fist In First Out (FIFO) IP with a Parallel/Serial interface which have been designed for the purposes of this research. Subsequently, it has been applied to a Direct Memory Access (DMA) Channel Peripheral Controller IP owned by Nordic Semiconductor ASA to further evaluate the scalability of the method. Besides, all properties have been described using the industrial standard language SystemVerilog Assertions (SVA) and all formal analyses have been carried out using vcFormal, a commercial Electronic Design Automation (EDA) tool from Synopsys. The reason for this is to ease the potential adoption of the proposed technique in the development of industrial applications specially where CPC is already used as part of the verification flow. Overall, the results of this research work show that the proposed technique has successfully identified the registers that require retention for all the analyzed systems. Also, the obtained execution times of the formal analyses per unit and on average depict a logarithmic growth with respect to the increase in size and complexity of the different analyzed systems.