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