Challenges in the formal verification of complete state-of-the-art processors

Research on formal hardware verification has made steady progress in developing methodologies and tools that try to cope with the growing complexities of systems. Despite of case studies that demonstrate the applicability of formal methods to selected contemporary processor designs, the current state in formal hardware verification is far from being considered practical for systems of the complexity of complete contemporary processor designs. It is our goal to improve the practicality of current formal verification methods for complete state-of-the-art processor designs. The recent success in the complete formal verification of the VAMP can be considered pioneering for reaching design complexities close to this range. We dissect the VAMP verification effort in detail with the goal to identify the main technical and organizational challenges and the major productivity bottlenecks of the verification process. This is done in particular to search for opportunities of increased levels of automation. As part of our efforts we are developing the VAMPExplorer, a tool that provides an intuitive interface to the specification, the implementation and the verification of the VAMP. The VAMPExplorer visualizes the general implementation and verification structure and improves accessibility to expert and non-expert users.