• Home
  • Formal Verification Research
    • Language Formalisms And Decision Procedures
    • Verification Methodologies For The Circuit Domain
    • Verification of Automated Systems
  • Tool Developed
  • Group Members
  • Contact
  • Photo Gallery

The group's work on design automation methodologies for verification of digital and analog integrated circuits is recognized worldwide. Our research has been funded by Intel for more than 10 years, by Synopsys for more than 15 years, by National Semiconductor Corp for more than 10 years, and by Semiconductor Research Corporation (SRC) for more than 7 years. Dr Dasgupta's research in this domain has been recognized by the prestigious Technomentor Award from the Indian Electronics and Semiconductor Association (IESA), and the IBM Faculty award. Dr Dasgupta is the Vice Chair of the India Chapter of the IEEE Council on Electronic Design Automation, and an Associate Editor of the IEEE Transactions on Design Automation of Electronic Circuits and Systems. The most significant contributions in this domain are highlighted below.

  • Methodologies for Analog and Mixed-signal Assertion-based verification

    • Assertions or formal properties are extensively used in the verification of digital integrated circuits. With the wide proliferation of analog components in system-on-chip designs, the requirement for assertions describing analog and mixed-signal (AMS) behaviors has become very significant. The group has developed the foundations of AMS assertions and their integration with industrial simulators and formal engines. We have done ground-breaking research on synchronizing AMS assertions with AMS simulation, trace debugging, and sampling refinement. Our AMS assertion tool developed under the SRC contract is the first industrially accepted tool in the domain and has been adopted by Freescale Semiconductors (a member of SRC). We have also contributed extensively in the past on methods for automatic generation of AMS behavioral models from hybrid automata skeletons in collaboration with National Semiconductor Corp, leading to the tool called CHASSIS. In another collaboration with POSOCO (the national power grid operators), our methods for AMS assertion monitoring are being re-engineered for monitoring phasor measurement data in electrical power grids.

    • Instrumenting AMS Assertion Verification on Commercial Platforms. Rajdeep Mukhopadhyay, S K Panda, Pallab Dasgupta, John Gough. ACM Transactions on Design Automation of Electronic Systems, 14 (2), 2009, 21:1 - 21:47.
    • Synchronizing AMS Assertions with AMS Simulation: From Theory to Practice. Subhankar Mukherjee, Pallab Dasgupta, Siddhartha Mukhopadhyay, Scott Little, John Havlicek, Srikanth Chandrasekaran. ACM Transactions on Design Automation of Electronic Systems 17(4): 38 (2012).
    • Computing Minimal Debugging Windows in Failure Traces of AMS Assertions. Subhankar Mukherjee, Pallab Dasgupta. IEEE Trans. on CAD of Integrated Circuits and Systems 31(11): 1776-1781 (2012).
    • Assertion Aware Sampling Refinement: A Mixed-Signal Perspective. Subhankar Mukherjee, Pallab Dasgupta. IEEE Trans. on CAD of Integrated Circuits and Systems 31(11): 1772-1776 (2012).
    • Chassis: A Platform for Verifying PMU Integration using Auto-Generated Behavioral Models. Antara Ain, Debjit Pal, Pallab Dasgupta, S. Mukhopadhyay, R. Mukhopadhyay, John Gough. ACM Transactions on Design Automation of Electronic Systems, 16(3), June 2011.

  • Formal verification methods for on-chip power management

    • Large scale circuits use complex power management strategies that dynamically regulate the operating voltage and clock frequencies of on-chip components. Bugs in the power management logic manifest themselves in form of data corruption (due to power droop and glitch related problems) and are among the hardest to debug. In collaboration with researchers from Synopsys we developed the first formal methodologies for verifying on-chip power management logic against formally specified architectural power management strategies. The PhD thesis of Aritra Hazra, won the prestigious ACM Best Dissertation Award (India) for this work. Currently Intel is collaborating with the group to expand the solution to mixed-signal power management logic.

    • Formal Verification of Architectural Power Intent. Aritra Hazra, Sahil Goyal, Pallab Dasgupta and Ajit Pal. IEEE Transactions on VLSI Systems (TVLSI), vol. 21, no. 3, pp. 78-91, 2013.
    • POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent. Aritra Hazra, Rajdeep Mukherjee, Pallab Dasgupta, Ajit Pal, Kevin Harer, Ansuman Banerjee, Subhankar Mukherjee. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 32(11): 1801-1813, 2013.
    • Formal Hardware/Software Co-Verification of Embedded Power Controllers. Pallab Dasgupta, M.K. Srivas, Rajdeep Mukherjee. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 33(12), 2025-2029, 2014.

  • Methods for getting around the state-explosion problem

    • Post-silicon bugs are often fixed by local patches deep inside the glue logic, but it is notoriously difficult to guarantee that the fix eliminates the bug and all its variants. The group was challenged by Intel to develop a methodology for analyzing the quality of the bug fix. We developed a taxonomy of bug fixes and a formal methodology for classifying bug fixes into this taxonomy, thereby enabling the designer to focus verification effort as required. We also developed the first of its kind methodology for learning assertions on the interface of the patched portion of the logic and using the assertions to rank potential counter-example scenarios in terms of their probability of being real. These methods reported outstanding correlation with real bug scenarios. Dr Srobona Mitra won the Google Women in Engineering Award in 2012 for this work. In collaborations with Synopsys, we have developed techniques for formal verification in a wide variety of domains, including industrial architectures and bus-functional models. Our work on the extraction of formal assumptions from constrained random test benches resulted in a joint US patent with Synopsys. In recognition of the expanding relationship with our institute, Synopsys awarded the Charles Babbage grant to IIT Kharagpur (first time in India) and set up the Synopsys CAD Lab at IIT Kharagpur (first of its kind).

    • Formal Guarantees for Localized Bug Fixes. Srobona Mitra, Ansuman Banerjee, Pallab Dasgupta, Priyankar Ghosh, Harish Kumar. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(8): 1274-1287, 2013.
    • Counterexample Ranking Using Mined Invariants. Srobona Mitra, Ansuman Banerjee, Pallab Dasgupta and Harish Kumar. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32(12), 1978-1991, 2013.
FV Group