The objective of this proposal is to develop a formal refinement-based methodology for term-level microprocessor verification and to apply it to complex designs. State-of-the-art microprocessors are extremely complex and industry estimates of validation costs, as a percentage of the engineering effort required to develop a new product, range from 30% to as high as 70%. Even with such resources allocated to validation, bugs are common and the trend toward more complex designs will exacerbate the problem. Current validation efforts focus on checking low-level properties of small components. However, it is difficult to imagine a set of properties that captures system-level correctness, which is why the project advocates a refinement-based approach, where the instruction set architecture is the specification. This means that to an external observer, the processor behaves in a fashion that is consistent with the instruction set architecture, with respect to both safety and liveness properties. The project proposes to develop a theory of refinement for system-level verification and to apply it to complex term-level designs. The refinement-based approach will be part of a design-for-verification methodology that complements the design cycle, that can be automated in a compositional, scalable way, and that is generally applicable across a wide spectrum of designs.
