Introduction | p. 1 |
Motivation | p. 1 |
High-Level Synthesis | p. 2 |
CDFG-Based High-Level Synthesis | p. 3 |
Esterel-Based High-Level Synthesis | p. 5 |
CAOS-Based High-Level Synthesis | p. 5 |
Low-Power Hardware Designs | p. 6 |
Power-Aware High-Level Synthesis | p. 7 |
Verification of Power-Optimized Hardware Designs | p. 9 |
Verification Using CAOS | p. 9 |
Problems Addressed | p. 10 |
Organization | p. 11 |
Related Work | p. 13 |
High-Level Synthesis | p. 13 |
C-Based Languages and Tools | p. 13 |
Other Languages and Tools | p. 14 |
Low-Power High-Level Synthesis | p. 14 |
Dynamic Power Reduction | p. 14 |
Peak Power Reduction | p. 17 |
Summary - Low-Power High-Level Synthesis Work | p. 18 |
Power Estimation Using High-Level Models | p. 18 |
Verification of High-Level Models | p. 21 |
SpecC | p. 21 |
SystemC | p. 22 |
Other Work | p. 23 |
Summary - High - Level Verification Work | p. 23 |
Background | p. 25 |
CDFG-Based High-Level Synthesis | p. 25 |
Concurrent Action-Oriented Specifications | p. 26 |
Concurrent Execution of Actions | p. 26 |
Mutual Exclusion and Conflicts | p. 27 |
Hardware Synthesis | p. 27 |
Example | p. 28 |
Power Components | p. 29 |
Average Power | p. 29 |
Transient Characteristics of Power | p. 30 |
Low-Power High-Level Synthesis | p. 30 |
Complexity Analysis of Algorithms | p. 31 |
NP-Completeness | p. 31 |
Approximation Algorithm | p. 31 |
Formal Methods for Verification | p. 32 |
Model Checking | p. 33 |
Low-Power Problem Formalization | p. 35 |
Definitions | p. 35 |
Other Details | p. 38 |
Schedule of a Design | p. 38 |
Re-scheduling of Actions | p. 39 |
Cost of a Schedule | p. 39 |
Low-Power Goal | p. 40 |
Factorizing an Action | p. 40 |
Formalization of Low-Power Problems | p. 41 |
Peak Power Problem | p. 41 |
Dynamic Power Problem | p. 41 |
Peak Power Problem is NP-Complete | p. 42 |
Dynamic Power Problem is NP-Complete | p. 42 |
Heuristics for Power Savings | p. 45 |
Basic Heuristics | p. 46 |
Peak Power Reduction | p. 46 |
Dynamic Power Reduction | p. 48 |
Example Applications | p. 50 |
Refinements of Above Heuristics | p. 53 |
Re-scheduling of Actions | p. 53 |
Factorizing and Re-scheduling of Actions | p. 57 |
Functional Equivalence | p. 59 |
Example Applications | p. 62 |
Complexity Analysis of Scheduling in CAOS-Based Synthesis | p. 65 |
Related Background | p. 66 |
Confluent Set of Actions | p. 66 |
Peak Power Constraint | p. 66 |
Scheduling Problems Without a Peak Power Constraint | p. 66 |
Selecting a Largest Non-conflicting Subset of Actions | p. 66 |
Constructing Minimum Length Schedules | p. 70 |
Scheduling Problems Involving a Power Constraint | p. 72 |
Packing Actions in a Time Slot Under Peak Power Constraint | p. 73 |
Maximizing Utility Subject to a Power Constraint | p. 75 |
Combination of Makespan and Power Constraint | p. 76 |
Approximation Algorithms for MM-PP | p. 79 |
Approximation Algorithms for MPP-M | p. 81 |
Dynamic Power Optimizations | p. 83 |
Related Background | p. 83 |
Clock-Gating of Registers | p. 83 |
Operand Isolation | p. 83 |
Clock-Gating of Registers | p. 84 |
Insertion of Gating Logic | p. 86 |
Other Versions of Algorithm 2 | p. 90 |
Experiment and Results | p. 91 |
Algorithm 1 | p. 91 |
Algorithm 2 | p. 93 |
RTL Power Estimation | p. 98 |
Summary | p. 100 |
Peak Power Optimizations | p. 103 |
Related Background | p. 104 |
Formalization of Peak Power Problem | p. 106 |
Peak Power Reduction Algorithm | p. 107 |
Handling Combinational Path Dependencies | p. 108 |
Experiments and Results | p. 110 |
Designs | p. 110 |
Gate-Level Average Power and Peak Power Comparisons | p. 111 |
Effects on Latency, Area, and Energy | p. 111 |
RTL Activity Reduction | p. 112 |
Summary | p. 113 |
Issues Related to Proposed Algorithm | p. 113 |
Verifying Peak Power Optimizations Using SPIN Model Checker | p. 115 |
Related Background | p. 116 |
Formal Description of CAOS-Based High-Level Synthesis | p. 118 |
Hardware Description | p. 118 |
Scheduling of Actions | p. 119 |
Correctness Requirements for CAOS Designs | p. 122 |
AOA Semantics | p. 122 |
Concurrent Semantics | p. 122 |
Comparing Two Implementations | p. 123 |
Converting CAOS Model to PROMELA Model | p. 124 |
Why SPIN? | p. 124 |
Generating PROMELA Variables and Processes | p. 124 |
Adding Scheduling Information to PROMELA Model | p. 124 |
Sample PROMELA Models | p. 126 |
Formal Verification Using SPIN | p. 128 |
Verifying Correctness Requirement 1 (CR-1) | p. 128 |
Verifying Correctness Requirement 2 (CR-2) | p. 128 |
Verifying Correctness Requirement 3 (CR-3) | p. 129 |
Sample Experiments | p. 130 |
Summary | p. 131 |
Epilogue | p. 141 |
References | p. 145 |
Index | p. 151 |
Table of Contents provided by Ingram. All Rights Reserved. |