Our work addresses the challenge of scaling pre-silicon functional verification of hardware designs such as microprocessors and microcontrollers. These designs employ wide datapaths with arithmetic, logical, and memory units, and complex control logic that coordinates their functionality. This overall complexity results in an enormous state space with vast room for design errors, and prevents designers from being able to comprehensively reason about the correctness of digital systems deployed in numerous devices, whose failure causes serious losses, monetary and otherwise.

In particular, control optimizations play a global role in coordinating the functionality and data flow. This makes them extremely error-prone and harder to verify locally. To remedy that, a design implementation can be verified against its full specification model which has a much simpler control logic. Then, a formal proof of equivalence exhaustively checks the state space for potential control bugs, or proves the lack thereof. Contrary to simulation-based approaches, which compromises completeness for speed, formal equivalence is hindered by the exponential state explosion. To overcome that, previous approaches abstract datapath components away in order to eliminate the complexity introduced by them, and to gear the verification towards the control logic. Due to the loose separation between datapath and control in most designs and hardware description languages, naïve abstraction results in compromising the accuracy of the verification, and in generating spurious behavior that does not exist in the original design, or masking real behavior from being represented in the abstract model.

Our work presents a systematic and fully automatic abstraction-based method to overcome these issues. A sound abstraction to fragments of first-order logic is coupled with refinement mechanisms that adjust the abstract model and prevent false alarms arising due to spurious behavior. Our approach includes novel techniques for analyzing abstract counterexamples, generalizing them to represent families of counterexamples, checking their feasibility on the original design, and analyzing the infeasibility in order to learn facts that augment the abstraction in an iterative process. Automating both the abstraction and refinement steps without compromising scalability gives our approach a clear advantage over systems that require laborious manual reasoning. In turn, the approach can be easily embedded in typical verification flows, where designers apply it on original descriptions used for synthesis and traditional simulation.

Additionally, our approach leverages the advantages of efficient reasoning engines for Boolean and first-order logic, including satisfiability (modulo theories) solvers and algorithms for minimal explanation of constraint infeasibility.

An implementation of the approach allows us to verify microcontrollers, microprocessors, and memory systems whose RTL Verilog descriptions have hundreds to thousands of source lines and variables, in a scalable and efficient manner. The results show promising capability in exposing implementation and specification errors, or, alternatively, proving correctness of both. We believe that this brings formal verification one step closer to hardware designers.