Automatic Formal Verification of Control Logic in Hardware Designs

[摘要] Our work addresses the challenge of scaling pre-silicon functional verification of hardwaredesigns such as microprocessors and microcontrollers. These designs employ widedatapaths and complex control logic, resulting in an enormous state space withvast room for design errors.In particular, control optimizations are extremely error-prone and harder to verify locally. Toremedy that, a design implementation can be verified against its full specification modelwhich has a much simpler control logic. Then, a formal proof of equivalence exhaustivelychecks the state space for potential control bugs. Formal equivalence is hindered by the exponential state explosion. To overcome that, previous approachesabstract datapath components away in order to eliminate their complexity, and to gear the verification towards the control logic. Due to the loose separation between datapath and control, naive abstraction results in compromising the accuracy of the verification, and in generating spuriousbehavior that does not exist in the original design, or masking real behavior frombeing represented in the abstract model.Our work presents a systematic and fully automatic method to overcomethese issues. A sound abstraction to fragments of first-order logic is coupled withrefinement mechanisms that adjust the abstract model and prevent false alarms arising dueto spurious behavior. Our approach includes novel techniques for analyzing abstract counterexamples,generalizing them to represent families of counterexamples, checking theirfeasibility on the original design, and analyzing the infeasibility in order to learn facts thataugment the abstraction in an iterative process. The full automation of the process gives our approach a clear advantage over systems that require laborious manual reasoning, and allows it to be used directly by designers. Additionally, our approach leverages the advantages of efficient reasoning engines forBoolean and first-order logic, including satisfiability (modulo theories) solvers.An implementation of the approach allows us to verify designs whose RTL Verilog descriptions have hundreds to thousands ofsource lines, in a scalable and efficient manner. The results show promisingcapability in exposing implementation and specification errors, or, alternatively, provingcorrectness of both. We believe that this brings formal verification one step closer to hardwaredesigners.

[发布机构] University of Michigan

[效力级别] Counterexample-Guided Abstraction Refinement

[关键词] Microprocessor Verification;Counterexample-Guided Abstraction Refinement;Science;Computer Science & Engineering