Meta-functions for Synthesizing Correct Arithmetic Hardware

本课题的目标是开发硬件生成功能，实现硬件的正确合成。这些函数的存在将大大节省设计时间，因为验证工作只发生一次。只需要证明生成函数是正确的。将扩展到产生实际设计的候选技术是：(1)使用已证明正确的递归函数来生成布尔逻辑；(2)从使用时序逻辑或Hoare的通信顺序过程（CSP）符号编写的规范中编译、指定和验证时序和控制硬件；(3)应用等价变换将高级规范改写为硬件生成函数，生成实用、正确的算术硬件。候选算法函数包括基于坐标旋转数字计算机（CORDIC）算法计算的超越函数。硬件元函数是管理超大规模集成电路设计复杂性的一类工具。与VLSI电路技术相关的大量门数使得人工合成正确详细的互连表和框图的希望变得不现实。像硬件元函数这样的正确和自动化的合成方法提供了从一开始就创建正确设计的诱人可能性。因此，使用仿真来验证大型设计的日益不现实的情况是可以避免的。

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.