Search

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.

Timing speculation is a ‘better-than-worst-case’ design methodology that tunes a digital circuit to its common-case delay. The average throughput of a speculation-based circuit can be estimated using the probability with which input patterns result in timing errors. In this paper, we present a scalable approach to compute the exact probabilities of the occurrence of timing errors at the gate level. We use Timed Characteristic Functions (TCFs) to compute the exact values of the probabilities. In order to improve the scalability, we decompose large circuits into smaller sub-circuits and restrict the TCF computation to these sub-circuits. Instead of substituting the expression for TCF of one sub-circuit into another, we propagate only the computed error probabilities. We demonstrate our technique on gate level combinational circuits from MCNC benchmarks.

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 10x for the CG method and more than 4x for the entire application for very large circuits when compared to a single-threaded CPU implementation.