This research will apply formal methods in logic, verification and synthesis to digital design engineering. The work centers on the use of applicative notation for system description and functional algebras for design derivation. The general goal is to develop a comprehensive methodology for constructing correct hardware implementations. Specific objectives are to establish a practicable algebraic framework for digital design, to clarify its relationship to conventional design methods, to explore its implications for design automation, and to incorporate contemporary formalisms for hardware verification. The principal investigator will base this research on his previous exploration of functional programming languages in hardware modeling and design-aids automation. His methodology has been demonstrated in a basic transformation system for deriving hardware implementations from higher-level behavioral descriptions. In the period of this research, the system will be refined and oriented toward a programmable technology (e.g. PLA and gate arrays). The emphasis will be on supporting engineering expertise in design derivation. Of particular interest are the problems of descriptive coherence and logical correctness in the presence of orthogonal design decompositions. VLSI (very large scale integration) is a recent field that explores how to design highly complex integrated circuits and related electronic systems. Research is needed because VLSI devices have become increasingly complex and the industry more competitive. Development of the field is important to the nation's competitive lead in electronics. An important research question in this field is that of automatically translating high-level VLSI circuit behavioral descriptions to correct and efficient circuit implementations. Solutions to this problem will permit VLSI design engineers to concentrate on the behavioral and functional aspects of the design without being encumbered with a mass of low level detail. This research addresses the need to apply formal methods to VLSI design engineering in order to bring needed mathematical rigor into the discipline. The formal methods will then become a basis for automating the design process. The principal investigator has made important conceptual advances in this area and will further develop them toward practice in his research.
