Leveraging UPF-extracted assertions for modeling and formal verification of architectural power intent

Hazra, Aritra ; Mitra, Srobona ; Dasgupta, Pallab ; Pal, Ajit ; Bagchi, Debabrata ; Guha, Kaustav (2010) Leveraging UPF-extracted assertions for modeling and formal verification of architectural power intent In: 2010 47th ACM/IEEE Design Automation Conference (DAC), 13-18 June 2010, Anaheim, CA, USA.

Full text not available from this repository.

Official URL: http://ieeexplore.ieee.org/document/5523286/

Related URL: http://dx.doi.org/10.1145/1837274.1837469

Abstract

Recent research has indicated ways of using UPF specifications for extracting valid low-level control sequences to express the transitions between the power states of individual domains. Today there is a disconnect between the high-level architectural power management strategy which relates multiple power domains and these low-level assertions for controlling individual power domains. In this paper we attempt to bridge this disconnect by leveraging the low-level per-domain assertions for translating architectural power intent properties into global assertions over low-level signals. We show that the inter-domain properties created in this manner can be formally verified over the global power management logic.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Network Synthesis; Energy Management Systems; Formal Verification; High Level Synthesis; Low-power Electronics
ID Code:101660
Deposited On:12 Dec 2016 10:08
Last Modified:12 Dec 2016 10:08

Repository Staff Only: item control page