Formally Verified, Efficient Tools for High-Level Synthesis and Hardware-Software Codesign

这是一个研究和教育计划，重点是开发高效，正式验证的CAD工具，用于数字系统的高级综合和协同设计。 这里的概念是开发CAD工具，这些工具本身经过正式验证并保证合成正确的设计。 这消除了设计人员掌握形式方法应用的需要。 目标是在嵌入式处理器和现场可编程门阵列上生成运行的代码。 这些工具的目的是将设计划分为硬件和软件组件，生成微处理器代码，并进行高级综合。 通过为系统中使用的表示语言（行为规范、寄存器传输级描述、门级电路、机器代码）提供语义模型，并证明工具产生的设计的含义是其规范含义的细化，来进行验证。 目前正在开发补充这项研究的理论和实践课堂课程。

This is a program of research and education centered on development of efficient, formally verified CAD tools for high-level synthesis and codesign of digital systems. The notion here is to develop CAD tools which are, themselves, formally verified and guaranteed to synthesize correct designs. This eliminates the need for designers to master application of formal methods. The aim is to produce code running on an embedded processor and custom hardware on field programmable gate arrays. The tools are designed to partition a design into hardware and software components, to generate microprocessor code, and to do high-level synthesis. Verification is done by providing semantic models for the representation languages used in the system (behavioral specification, register- transfer level description, gate-level circuit, machine code) and proving that the tools produce designs whose meanings are refinements of the meanings of their specifications. Theoretical and practical classroom courses which compliment this research are being developed.