The goal this research is to make sharing of verified hardware designs more practical. First, a model for describing and verifying type-based abstract modules, which can be used and reused in different HDL's and proof systems, is being developed. This model provides a methodological approach to verification. It is based on work in generic interpreters and micro-processor verification. Second, a model for interchange and sharing library components is being developed. This is to enable designers to effectively develop and use module libraries in a distributed manner. The module libraries being developed are publicly available so that the ideas about reuse can be tested on a large scale.
