My research area is design verification. I am currently investigating how the design decisions affect verification effort. It is a very important and complex task to do functional verification on modern microprocessors. With the increasing demand of fast computation, a lot of design decisions have been made on the general purpose processors to make them solving specific problems, such as image processing, cryptography, etc. Some decisions make the processors more efficient, however, sometimes they also involve more verification effort. There exist several metrics to measure how much the performance gained by some design decisions, but there is no method to objectively demonstrate how the design decisions affect verification effort.
The design under verification is a Cryptographic processor, whose ISA has four sources and two destinations, and uses look up table doing logic operations. During my first year PhD study, I did some simulation-based experiments on the innovative processor and traditional processor. I measured the code coverage and the branch coverage under the tests with the same functionality. The result showed that the traditional processor had higher coverage under the same functionality tests. However, high coverage does not always mean good quality of verification. Verification also includes bug detection, etc. Now, I have been looking from the formal side to model the processor from specification to each bit pattern of the instructions by refinements.
Recently, I have just finished an Event-B processor model. The model is developed on RODIN platform, which is an Eclipse based development environment. In addition to the model itself, I also extended the RODIN with an Event-B to report plug-in (source .zip (Rodin Version 1.0 compatible) and plug-in .jar).