Joint Research in Hardware Synthesis and Verification

9224575 Brown这是康奈尔大学和牛津大学之间关于验证硬件合成的合作研究。 康奈尔大学和牛津大学的项目旨在合成正确的硬件。 这些项目各自使用不同的（尽管相关）语言和不同的目标体系结构。 通过结合两个小组的专业知识，将开发一套工具和方法，使设计师有很大的灵活性。 该项目的主要任务是： 共享工具主要的好处是共享工具，以便每个小组都可以利用其他项目的开发成果。 为了便利工具的共享，将开发一个通用中间表格。 验证技术的比较这两个小组都致力于证明他们的编译器的正确性，并且正在研究的语言非常相似。 然而，所使用的证明技术有很大的不同。 目标实现的比较这两个组可以访问不同的目标硬件集。 针对不同应用程序的开发虽然开发的编译系统相似，但目标应用程序不同。 ***

9224575 Brown This is a collaborative research on verified hardware synthesis between Cornell University and Oxford University. The projects at Cornell and at Oxford are aimed at synthesizing correct hardware. These projects each use different (though related) languages and different target architectures. By combining expertise of the two groups a set of tools and methodologies will be developed which allows the designer a great deal of flexibility. The primary tasks of the project are: Sharing Tools The main benefit will be to share tools so that each group can take advantage of developments from other projects. Development of Common Intermediate Form In order to facilitate sharing of tools a common intermediate form will be developed. Comparison of Verification Techniques Both groups are working on proofs of correctness for their compilers and the languages being studied are quite similar. However, the proof techniques being used are substantially different. Comparison of Target Implementations The two groups have access to different sets of target hardware. Development for Different Applications While the compilation systems developed are similar the target applications are different. ***