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. ***