Meta-functions for Synthesizing Correct Arithmetic Hardware

本项目的目标是开发硬件生成 正确合成硬件的功能。 存在这种 函数将大大节省设计时间，因为 验证工作仅发生一次。 只有生成函数 需要被证明是正确的 候选技术将是 扩展到生产实际设计是：（1）使用证明 （2）编译， 指定和验证定时和控制硬件， 使用时态逻辑或Hoare的符号编写的规范 通信顺序进程（CSP）;（3）应用 等价转换，将高级规范重写为 硬件生成功能，生成实用且正确的 算术硬件 候选算术函数包括 基于所用算法计算的超越函数 坐标旋转数字计算机（CORDIC） 硬件元函数是管理复杂性的一类工具 VLSI设计。 与超大规模集成电路有关的大门数 技术使不切实际的希望，正确的详细 互连列表和框图可以手动合成。 正确和自动化的合成方法，如硬件元函数 提供了从设计中创建正确设计的有吸引力的可能性 start.因此，验证大型设计越来越不切实际， 避免使用模拟。

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.