Loading...
Please wait, while we are loading the content...
Similar Documents
Transformations in High-Level Synthesis: Formal Specification and Efficient Mechanical Verification (1994)
| Content Provider | CiteSeerX |
|---|---|
| Author | Rajan, P. Sreeranga |
| Description | Proc. of the IFIP International Conference on CHDL Dependency graphs are used to model data and control flow in hardware and software design. In high-level synthesis of hardware, optimization and refinement transformations are used to transform dependency-graph-based specifications at the behavior level to dependency-graph-based implementations at the register-transfer level. Registertransfer -level implementations are mapped to gate-level hardware designs by low-level logic synthesis. In this work, we investigated the specification and mechanical verification of the correctness of transformations used in high-level synthesis of hardware. We have provided a formal specification of dependency graphs, and verified the correctness of a variety of transformations used in an industrial synthesis framework. Errors have been discovered in the transformations, and modifications have been proposed and incorporated. Further, the formal specification has permitted us to examine the generalization and composition of transformations. In the process... |
| File Format | |
| Language | English |
| Publisher Date | 1994-01-01 |
| Access Restriction | Open |
| Subject Keyword | Mechanical Verification Gate-level Hardware Design Industrial Synthesis Framework Low-level Logic Synthesis Dependency Graph Refinement Transformation Dependency-graph-based Implementation Formal Specification Control Flow Dependency-graph-based Specification High-level Synthesis Behavior Level Efficient Mechanical Verification Registertransfer Level Implementation Software Design Register-transfer Level |
| Content Type | Text |
| Resource Type | Article |