This thesis presents automatic term-level abstraction techniques in the context of formal verification applied to hardware designs. The techniques aim to perform abstraction as automatically as possible, while requiring little to no user guidance. Data abstraction and function abstraction are the foci of this work. The abstraction techniques presented herein rely on combining static analysis, random simulation, machine learning, and abstraction-refinement in novel ways, resulting in more intelligent and scalable formal verification methodologies.
The data abstraction procedure presented in this work uses static analysis to identify portions of a hardware design that can be re-encoded in a theory other than the theory of bit vectors, with the goal of creating an easier to reason about verification model. In addition, the data abstraction procedure can provide feedback that can help the designer create hardware designs that are easier to verify.
The function abstraction procedures described in this work rely on static analysis, random simulation, machine learning, and counterexample-guided abstraction-refinement to identify and abstract functional blocks that are hard for formal tools to reason about. Random simulation is used to identify functional blocks that will likely yield substantial performance increases if they were to be abstracted. A static analysis-based technique, ATLAS, and a separate technique, CAL, based on a combination of machine learning and counterexample-guided abstraction-refinement, are then used to compute conditions under which it is precise to abstract. That is, functional blocks are abstracted in a manner that avoids producing spurious counterexamples.
Experimental evidence is presented that proves the efficacy and efficiency of the data and function abstraction procedures. The experimental benchmarks are drawn from a wide range of hardware designs including network-on-chip routers, low-power circuits, and microprocessor designs.