Formal gurantees for stochastic (approximate) and deterministic system

The holy grail of all system building is to have the ability to check that it exhaustively, provably works. However, even a 300 flop design can have more states than the number of protons in the universe! It is therefore impossible to navigate all possible states of a system explicitly. Fortunately, there are much cleverer ways to do this, making it possible to provide guarantees about some critical parts of the system. These could be intelligent partitioning, reasoning with an abstract model, compositional reasoning etc. Many of these methods are geared towards traditional deterministic systems. Our focus has been on stochastic systems that are designed with the intention of not being accurate 100% of the time. In these approximate computing systems, we address the question of what it means to be correct, what can one guarantee in the presence of intentional errors etc. We find ways to reason with these systems in a scalable manner.

In analog and mixed signal systems, we have researched algorithms for reachability analysis and runtime monitoring, using a sampling based method.

Our work has won the ACM student research competition (SRC) at DAC 2011. Our analog reachability work was also nominated for a best paper award in DATE 2013.

For reachability analysis, we use Voronoi diagram based approximate reachability. We use a sampling based method to identify the borders of the various polygons that we draw as part of the Voronoi diagram split of the reachable state space. For runtime monitoring, we develop a methodology to dynamically check assertions in STL. We also developed the early methods for formal verification of large multipliers- an area that is much in demand now, due to the explosion of data intensive designs today.

  1. Jayanand Asok Kumar Lingyi Liu and Shobha Vasudevan, Scaling Probabilistic Timing Verification of Hardware Using Abstractions in Design Source Code, Formal Methods in Computer Aided Design, (FMCAD) 2011: 196-205
  2. Jayanand Asok Kumar and Shobha Vasudevan. Formal performance analysis for faulty MIMO hardware. IEEE Transactions on Very Large Scale Integrated Systems ( IEEE TVLSI) 20(10): 1914-1918 (2012).
  3. Jayanand Asok Kumar and Shobha Vasudevan, SHARPE: Variation-Conscious Formal Timing Analysis, IEEE Transactions on CAD of Integrated Ciruits and Systems (IEEE TCAD), 32 (5): 788-801(2013)
  4. Jayanand Asok Kumar and Shobha Vasudevan Automatic compositional reasoning for probabilistic model checking of hardware designs, International Conference on Quantitative Evaluation of Systems (QEST) 2010
  5. Jayanand Asok Kumar and Shobha Vasudevan Statistical Guarantees of Performance for MIMO Designs, International Conference on Dependable Systems and Networks (DSN) 2010:
  6. Jayanand Asok Kumar and Shobha Vasudevan, Variation-Conscious Formal Timing Verification in RTL, International Conference on VLSI Design (VLSI Design) 2011:58-63
  7. Seyed Nematollah Ahmadyan and Shobha Vasudevan, Reachability Analysis of Nonlinear Analysis through Iterative Reachable Set Reduction, Design Automation and Test in Europe (DATE) 2013: 1436-1441
  8. Seyed Nematollah Ahmadyan and Shobha Vasudevan, Runtime Verification of Nonlinear Analog Circuits Using Incremental Time-Augmented RRT Algorithm, Design Automation and Test in Europe (DATE) 2013: 21-26
Reachability analysis with Voronoi diagrams of Van der pol circuit