An RTL abstraction technique for processor microarchitecture validation and test generation

Design validation is becoming more and more a bottleneck in the microproces sor design process. The difficulty of validation stems from the complexity of the design, which requires searching an enormous space to check correctn ess. This is exacerbated by features for enhancing performance, such as pip elines, which are becoming common in most microprocessors. This paper descr ibes a new abstraction technique to handle this problem. Our solution is a novel method to identify the control states automatically from the processo r HDL description and to extract an abstract finite state machine model whi ch preserves the behaviors of the design accurate to the clock cycle, so th at the state space to be analyzed is drastically reduced. This model is used to evaluate microarchitecture-level coverage of validati on tests. We also present validation test generation algorithm for traversi ng state transition paths and covering snapshot and temporal events. These abstract paths with a finite length, along with information about the instr uction set, are used to generate system-level tests. Results on example mic roprocessor models show the technique is efficient in finding bugs that oth er verification methods miss.