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