The group's work on logics for expressing quantitative artifacts is path-breaking and separates this work from the classical body of logic dealing with Boolean propositions and predicates. We introduced logics like Min-Max Computation Tree Logic, Quantified Computation Tree Logic, Fuzzy Real Time Temporal Logic, which have been extensively studied by other researchers. Very recently we have shown for the first time that reliability annotations on temporal logics can be used to obtain provable guarantees on reliability of component based dynamical systems.

• Min-max Computation Tree Logic. P.Dasgupta, Jatindra K. Deka, P.P.Chakrabarti and S. Sriram. Artificial Intelligence, 127 (2001), 137-162.
• Quantified Computation Tree Logic. A.C.Patthak, I.Bhattacharya, A.Dasgupta, P.Dasgupta, P.P.Chakrabarti. Information Processing Letters, 82(3): 123-129, 2002
• A Fuzzy Real Time Temporal Logic. Subhankar Mukherjee, P. Dasgupta. International Journal of Approximate Reasoning, 54(9): 1452-1470, 2013.
• Formal Assessment of Reliability Specifications in Embedded Cyber-Physical Systems. Aritra Hazra, Palab Dasgupta and Partha Pratim Chakrabarti. Accepted for Publication in the Journal of Applied Logic (JAL), Elsevier, 2016.

Temporal logic based specifications are widely used in formal verification; however in practice, the task of developing formal specifications is greatly facilitated by using auxiliary formalisms. The group's work on auxiliary state machines is widely adopted in industrial practice. More recently we have shown that auxiliary automata and auxiliary functions can significantly enhance the expressive power of analog extensions of assertion languages. Our work has been used as one of the primary references in the Accellera Verilog-AMS subcommittee working towards introducing AMS assertions in Verilog-AMS standards.

• Auxiliary state machines + context triggered properties in verification. Ansuman Banerjee, Pallab Dasgupta, P.P. Chakrabarti. ACM Transactions on Design Automation of Electronic Systems, 13 (4), 2008, 62:1 - 62:31.
• Auxiliary Specifications for Context-Sensitive Monitoring of AMS assertions. Subhankar Mukherjee, P. Dasgupta, S. Mukhopadhyay. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 30(10): 1446-1457, 2011.
• 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

Model checking techniques for formal verification primarily aim to prove formal properties on state machine representations of the design under test. Scalability is a major concern here since the state machines of real world systems are huge and (typically) do not fit in memory. In a seminal collaboration with Intel researchers, the group developed a reasoning framework, where coverage gaps between system-level properties and proven properties of components can be evaluated, thereby targeting the verification effort on specific component level properties, as opposed to the whole system. This design intent coverage methodology, was integrated into Intel's formal verification tool flow, has been jointly published, and also articulated in the monograph, "A Roadmap for Formal Property Verification", published by Springer in 2006. Later the methodology was extended to parametric reasoning for early time budgeting in component based real time automotive control systems and patented for that domain with General Motors.

• Design Intent Coverage – A New Paradigm for Formal Property Verification. P.Basu, S.Das, A.Banerjee, P. Dasgupta, P.P. Chakrabarti, C.R. Mohan, L.Fix, R.Armoni. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, 25 (10) 1922-1934,2006.
• Design Intent Coverage Revisited. Arnab Sinha, Pallab Dasgupta, Bhaskar Pal, Sayantan Das, Prasenjit Basu, P.P. Chakrabarti. ACM Transactions on Design Automation of Electronic Systems, 14 (1) 2009, 9:1—9:32.
• Time-Budgeting: A Component Based Development Methodology for Real-time Embedded Systems. Manoj Dixit, S.Ramesh and Pallab Dasgupta. Formal Aspects of Computing (FAOC), Springer, 26(3), 591-621, 2014.

In a recent work sponsored by the prestigious Semiconductor Research Corporation (SRC), the group has introduced a path-breaking concept called formal features. As opposed to assertions which have a Boolean outcome, features are real valued. Our language formalism for features enables the use of un-interpreted variables (called local variables) for computing real valued artifacts over matches of an underlying Boolean assertion. We have shown that features can express a wide range of properties in the control domain and the analog circuit domain.

• Formal Interpretation of Assertion Based Features on AMS Designs. Antonio A Bruto Da Costa, Pallab Dasgupta. IEEE Design and Test, 32(1), 9-17 (2015).
• Feature Indented Assertions for Analog and Mixed-Signal Validation. Antara Ain, Antonio A Bruto Da Costa, Pallab Dasgupta. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, (to appear).

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.

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.

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.

In a recent work sponsored by the prestigious Semiconductor Research Corporation (SRC), the group has introduced a path-breaking concept called formal features. As opposed to assertions which have a Boolean outcome, features are real valued. Our language formalism for features enables the use of un-interpreted variables (called local variables) for computing real valued artifacts over matches of an underlying Boolean assertion. We have shown that features can express a wide range of properties in the control domain and the analog circuit domain.

• Formal Interpretation of Assertion Based Features on AMS Designs. Antonio A Bruto Da Costa, Pallab Dasgupta. IEEE Design and Test, 32(1), 9-17 (2015).
• Feature Indented Assertions for Analog and Mixed-Signal Validation. Antara Ain, Antonio A Bruto Da Costa, Pallab Dasgupta. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, (to appear).