Automatic Abstraction Of Microprocessors For Verification CS252 Final Project

Abstract—This paper describes the motivation for hy-brid term- and word- level verification models. In addition, we provide evidence that using abstraction in the right places can dramatically reduce runtime. With the ever-increasing complexity of processor designs, we need to automate as much of the verification process as possible. We describe a method to automate the abstraction and translation process from a hardware description language to our formal verification language. I