Harmonizing data mining and static analysis to tackle hardware and system level verification

Verification continues to pose one of the greatest challenges for today's chip design. Formal verification and simulation-based verification have been widely adopted. Both of them always rely on assertions (a.k.a. properties) to express a design's intended behaviors. State-of-the-art formal verification suffers from the scalability issue, and the simulation based method does not suffice in covering design behaviors. Moreover, the used assertions are always manually written, which greatly lowers the usability of hardware verification. For complex system on chip (SoC) design, the electronic system level (ESL) methodology creates a high level abstract view of the design, and the model is used for verifying functionality and performance at the early stage. Due to the fast simulation speed and high model complexity, the entire verification methodology is unsystematic and ad hoc, and lacks the support from EDA tools.;In this dissertation, we first present two systematic input stimulus generation methods for simulation based verification of register transfer level (RTL) design. The first method is based on STAR, a technique for generating input vector patterns for all paths of an RTL design using RTL symbolic execution. To attack the path explosion problem in STAR, we present HYBRO and the symbolic state caching method. HYBRO uses branch coverage metric to guide the path exploration. It is a best-effort method that produces excellent coverage for practical designs. Symbolic state caching considers the reachable state space when exploring different paths. It only generates tests for paths leading to previously uncovered state space. As a result, the path explosion problem is mitigated, and the entire method is much more scalable than the original STAR.;Another method for simulation based verification is based on GoldMine, an automatic assertion generation tool that was developed at the University of Illinois. We use the counterexamples generated from formal verification of GoldMine assertions to incrementally refine the internal decision tree. The counterexamples in every iteration can deterministically increase the coverage of the design and eventually cover the whole reachable input space.;To improve the quality of generated assertions, we present a novel technique that combines static and dynamic analysis of RTL source code to discover word level features for assertion mining algorithm. That allows the mined assertions to be at the same level of abstraction as RTL instead of the Boolean bit level. The machine learning algorithm, as such, is thus agnostic to the level of abstraction of its features.;For ESL verification, we present our technique for generating assertions from transaction level models (TLMs) using GoldMine. The generated assertions, which are in the form of frequent patterns in simulation traces of TLMs, are able to express functionality specification as well as performance specification. Our static analysis technology also guides the mining algorithm to generate assertions capturing the data propagation relationships among function parameters and return values in TLMs. We attempt two mining algorithms for TLM assertion generation: sequential pattern mining and episode mining. We demonstrate that episode mining is more scalable and generates higher quality assertions than does sequential pattern mining.;Diagnosing performance violations in ESL verification is still a manual and time-consuming process in industry. We present an intelligent method to localize root causes of performance violations from simulation traces. We propose a concurrent mining method to discover concurrent patterns from the traces, which are potential root causes of the violations. We apply three categories of domain knowledge to increase the effectiveness of the mining results. We show that the concurrent pattern mining with domain knowledge pinpoints the root cause of a violation to a few patterns among transaction traces of massive size.