Formal verification of architectural power intent

Hazra, Aritra ; Goyal, Sahil ; Dasgupta, Pallab ; Pal, Ajit (2013) Formal verification of architectural power intent IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 21 (1). pp. 78-91. ISSN 1063-8210

Full text not available from this repository.

Official URL:

Related URL:


This paper presents a verification framework that attempts to bridge the disconnect between high-level properties capturing the architectural power management strategy and the implementation of the power management control logic using low-level per-domain control signals. The novelty of the proposed framework is in demonstrating that the architectural power intent properties developed using high-level artifacts can be automatically translated into properties over low-level control sequences gleaned from UPF specifications of power domains, and that the resulting properties can be used to formally verify the global on-chip power management logic. The proposed translation uses a considerable amount of domain knowledge and is also not purely syntactic, because it requires formal extraction of timing information for the low-level control sequences. We present a tool, called POWER-TRUCTOR which enables the proposed framework, and several test cases of significant complexity to demonstrate the feasibility of the proposed framework.

Item Type:Article
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Power Intent Verification, Assertion, Formal Verification, Low-power Verification
ID Code:100850
Deposited On:09 Mar 2018 10:15
Last Modified:09 Mar 2018 10:15

Repository Staff Only: item control page