Structured hardware design transformations
Zhu Zheng · 1992
Studies of formal hardware designs are motivated by fast growing complexity of VLSI designs which have outpaced development of methodologies and tools. One area of study in formal methods for VLSI is design transformation. It establishes a design path, using a set of predefined transformations, between a specification and a design description which satisfies certain constraints. This thesis develops three results for design transformations of synchronous circuits. (1) An equational specification of hardware architectures and corresponding characterization of hardware controls extracted from recursive definitions. (2) A specification framework for sequential operations. In this framework, temporal relationship of sequential operations is formulated as a system of inequalities. A solution to inequalities is a synchronization mechanism which coordinates sequential operations to preserve the temporal relationship represented by the system of inequalities. (3) Applications of solving system of inequalities are sequential operation composition and sequential control integration. This allows designer to derive a circuit control from its recursive definition and sequential description of its architecture implementation.