The group focuses on efficient and scalable techniques for the formal verification of digital systems. 

Current research themes:

Scalable verification technology at the nanoscale for developing reliable and bug-free designs is a crucial requirement for the growth and impact of digital systems in the nano-era. One of the key optimizations used extensively in digital design is hardware pipelining, which is similar in operation to the pipelined automotive assembly line. Pipeline implementations at the nanoscale are very complex and prone to errors. 

This research seeks to develop solutions to enable efficient and scalable verification of pipelined circuits and systems at the nanoscale. The verification solutions are based on refinement, a notion of equivalence used to compare systems defined at very disparate levels of abstraction. The overall approach is to use high-level refinement-based transformations to reduce the nano-pipelined circuit/system to be verified, in incremental steps, to a functionally equivalent non-pipelined synchronous machine. The non-pipelined machine can then be easily compared with high-level specifications using existing verification techniques.

Group members: Sudarshan Srinivasan