Assertions are gaining importance in pre-silicon hardware verification to ensure expected design behavior. Coverage of an assertion in terms of statements of a Register Transfer Level (RTL) source code is a very accessible metric for understanding the scope of assertions and for debug. However, few methods to report it currently exist. We present a methodology to define and compute code coverage of an assertion. Our method is based on static and dynamic analysis of the RTL source code. We demonstrate the scalability and effectiveness of our approach with experimental results on real designs for both manual and automatically generated assertions.

We propose PRECIS, a methodology for automatically generating invariants at function and loop boundaries through program path guided clustering. We instrument function inputs and outputs together with predicates for branch conditions and record their values during each execution. Program runs that share the same path are grouped together based on predicate words. For each group with sufficient data we use linear regression to express the output as a function of the inputs. Groups with insufficient data are examined as candidates for clustering with neighboring groups. Candidates that share the same output function are merged into a cluster. For each cluster, we write an invariant that summarizes the behavior of the corresponding set of paths. We evaluate our technique using Siemens benchmarks. When compared to Daikon, we find that our method has significant advantages.

System level modeling is widely employed at early stages of system development for simplifying design verification and architectural exploration. Assertion based verification has become a well established part of RTL verification methodology. In the traditional assertion based verification flow, assertions are manually written. In this paper, we generate assertions from system level designs using GoldMine, an automatic assertion generation engine that uses data mining and static analysis. Candidate assertions are mined in the form of frequent patterns in the simulation traces of the system level designs. We consider both cycle accurate and transaction level designs and develop a methodology for the mining of each. For cycle accurate designs, we use both a decision tree based supervised learning algorithms as well as a coverage guided association mining algorithm to search for correlations in the simulation trace. For transaction level designs, sequential pattern mining is applied to generate frequent sequences of function calls and events from traces. We also use a symbolic execution engine to generalize the parameters and return values of the functions to help the data miner find relevant behavior. We show that our technique generates meaningful assertions on both a cycle accurate RISC CPU design and a transaction level AMBA-based DMA controller.

The Conjugate Gradient method is a popular iterative method to solve a system of linear equations and is used in a variety of applications. The DC Analyser is a circuit simulator built at IIT Bombay to solve large circuits containing resistances, voltage and current sources and which employs the conjugate gradient method. Current generation of graphics cards offer extremely high raw processing power and memory bandwidths compared to conventional CPUs. We have accelerated the conjugate gradient part of the DC Analyser using an Nvidia GTX 280 GPU and the new CUDA technology and successfully obtained a speedup of over 10× for the CG method and more than 4× for the entire application for very large circuits when compared to a single-threaded CPU implementation.