Meta-functions for Synthesizing Correct Arithmetic Hardware

点击翻译按钮获取中文摘要

The objective of this project is to develop hardware generation functions that synthesize hardware correctly. The existence of such functions would result in a significant savings in design time because the validation effort occurs only once. Only the generating function needs to be proven correct. The candidate techniques which will be extended to produce practical designs are: (1) the use of proven correct recursive functions to generate Boolean logic; (2) compiling, specifying, and verifying timing and control hardware from specifications written using temporal logic or the notation of Hoare's Communicating Sequential Processes (CSP); and (3) the application of equivalence transformations to rewrite high-level specifications into hardware generation functions which produce practical and correct arithmetic hardware. Candidate arithmetic functions include transcendental functions that are calculated based on the algorithm used by the coordinate rotation digital computer (CORDIC). Hardware meta-functions are one class of tool to manage the complexity of VLSI design. The large gate counts associated with VLSI circuit technology makes unrealistic the hope that correct detailed interconnection lists and block diagrams can be synthesized manually. Correct and automated synthesis methods like hardware meta-functions offer the attractive possibility of creating correct designs from the start. Thus, the growing impracticality of validating large designs using simulation is avoided.