Computer-Aided Design, International Conference on (2011)
San Jose, CA, USA
Nov. 7, 2011 to Nov. 10, 2011
Miroslav N. Velev , Aries Design Automation, LLC
Ping Gao , Aries Design Automation, LLC
We present highly automatic techniques for formal verification of pipelined microprocessors with hardware support for multithreading. The processors are modeled at a high level of abstraction, using a subset of Verilog, in a way that allows us to exploit the property of Positive Equality that results in significant simplifications of the solution space, and orders of magnitude speedup relative to previous methods. We propose abstraction techniques that produce at least 3 orders of magnitude speedup, which is increasing with the number of threads implemented in a pipelined processor. To the best of our knowledge, this is the first work on automatic formal verification of pipelined processors with hardware support for multithreading.
M. N. Velev and P. Gao, "Automatic formal verification of multithreaded pipelined microprocessors," Computer-Aided Design, International Conference on(ICCAD), San Jose, CA, USA, 2011, pp. 679-686.