"Low Power Hardware Synthesis from Concurrent Action-Oriented Specifications" by Gaurav Singh, Sandeep K. Shukla

This book introduces novel techniques for generating low-power hardware from a high-level description of a design in terms of Concurrent Action-Oriented Specifications (CAOS). It also describes novel techniques for formal verification of such designs.


It will provide the readers with definitions of various power optimization and formal verification problems related to CAOS-based synthesis, necessary background concepts, techniques to generate hardware according to the design’s power requirements, and detailed experimental results obtained by applying the techniques introduced on realistic hardware designs.
Contents
1 Introduction
1.1 Motivation
1.2 High-Level Synthesis
1.3 Low-Power Hardware Designs
1.4 Verification of Power-Optimized Hardware Designs
1.5 Problems Addressed
1.6 Organization
2 Related Work
2.1 High-Level Synthesis
2.2 Low-Power High-Level Synthesis
2.3 Power Estimation Using High-Level Models
2.4 Verification of High-Level Models
3 Background
3.1 CDFG-Based High-Level Synthesis
3.2 Concurrent Action-Oriented Specifications
3.3 Power Components
3.4 Complexity Analysis of Algorithms
3.5 Formal Methods for Verification
4 Low-Power Problem Formalization
4.1 Definitions
4.2 Other Details
4.3 Formalization of Low-Power Problems
5 Heuristics for Power Savings
5.1 Basic Heuristics
5.2 Refinements of Above Heuristics
6 Complexity Analysis of Scheduling in CAOS-Based Synthesis
6.1 Related Background
6.2 Scheduling Problems Without a Peak Power Constraint
6.3 Scheduling Problems Involving a Power Constraint
7 Dynamic Power Optimizations
7.1 Related Background
7.2 Clock-Gating of Registers
7.3 Insertion of Gating Logic
7.4 Experiment and Results
7.5 Summary
8 Peak Power Optimizations
8.1 Related Background
8.2 Formalization of Peak Power Problem
8.3 Peak Power Reduction Algorithm
8.3.1 Handling Combinational Path Dependencies
8.4 Experiments and Results
8.5 Summary
8.6 Issues Related to Proposed Algorithm
9 Verifying Peak Power Optimizations Using SPIN Model Checker
9.1 Related Background
9.2 Formal Description of CAOS-Based High-Level Synthesis
9.3 Correctness Requirements for CAOS Designs
9.4 Converting CAOS Model to PROMELA Model
9.5 Formal Verification Using SPIN
9.6 Summary
10 Epilogue
References
Index