The development of the signaling logic used in electronic interlocking equipment used in railways around the world follows a predominantly manual process, resulting in human errors which are extremely difficult to debug, but may have catastrophic consequences. In collaboration with RDSO, Indian Railways, a software has been developed for mathematically proving the correctness of the signaling logic as per the EN50128 railway safety standards. The methodology and tool details are presented in the following paper:

• S.Ghosh, A.Das, N.Basak, Pallab Dasgupta, A.Katiyar. Formal Methods for Validation and Test Point Prioritization in Railway Signaling Logic. IEEE Transactions on Intelligent Transportation Systems, 2016.
  DOI: 10.1109/TITS.2016.2586512

Modern large scale digital integrated circuits use complex power management logic for dynamically operating parts of the chip in various combinations of voltages and clock frequencies. Bugs in this logic are among the hardest to catch and is a major irritant in the chip design industry. In collaboration with Synopsys, the world leader in Electronic Design Automation, a software called POWER-TRUCTOR was developed under the Synopsys CAD Labs for mathematically proving the validity of power management logic. The details of the POWER-TRUCTOR tool can be found in the following paper:

• A.Hazra, R.Mukherjee, Pallab Dasgupta, A.Pal, K.Harer, A.Banerjee, S.Mukherjee. POWER-TRUCTOR: An Integrated Tool Flow for Formal Verification and Coverage of Architectural Power Intent. IEEE Transactions on CAD of Integrated Circuits and Systems 32(11): 1801-1813, 2013.

Portable power electronic devices use customized power supplies in the form of low dropout regulators and buck regulators, and battery chargers. In order to achieve simulation speeds equivalent to digital simulation, these analog components are replaced with behavioral models. In collaboration with National Semiconductor Corp, one of the world leaders in analog electronic chips prior to its acquisition by Texas Instruments, a tool called CHASSIS was developed for automatically generating behavioral models of such DC-DC regulators from hybrid automata skeletons. The details of the CHASSIS tool can be found in the following paper:

• A. Ain, D.Pal, Pallab Dasgupta, S. Mukhopadhyay, R. Mukhopadhyay, John Gough. CHASSIS: A Platform for Verifying PMU Integration using Auto-Generated Behavioral Models, ACM Transactions on Design Automation of Electronic Systems, 16(3), June 2011.

This tool suite enables any standard AMS circuit simulator to monitor analog time domain properties and features. The development of this tool suite has been funded by Semiconductor Research Corporation (SRC) which is a consortium of semiconductor and EDA companies (including Intel, IBM, Texas Instruments, NXP, AMD and Mentor Graphics). The details of this tool suite can be found in the following papers:

• A.A. Bruto Da Costa, Pallab Dasgupta, Formal Interpretation of Assertion Based Features on AMS Designs, IEEE Design and Test, 32(1), 9-17 (2015).
• A. Ain, A.A. Bruto Da Costa, Pallab Dasgupta, Feature Indented Assertions for Analog and Mixed-Signal Validation, IEEE Transactions on CAD of Integrated Circuits and Systems, 2016. DOI: 10.1109/TCAD.2016.2525798

An important requirement in any form of verification is in assessing the completeness of the specification. Incomplete specifications can cause bugs to be missed in verification. In collaboration with Intel the tools SPEC-MATCHER and COV-ANALYZER were developed for formal analysis of completeness of formal specifications and integrated with Intel’s Forspec/Forecast tool suite. The details of these tools are reported in the following:

• Pallab Dasgupta, A Roadmap for Formal Property Verification, Springer, 2006.
• P. Basu, S. Das, A. Banerjee, Pallab Dasgupta, P.P. Chakrabarti, C.R. Mohan, L. Fix, R. Armoni. Design Intent Coverage – A New Paradigm for Formal Property Verification. IEEE Transactions on CAD of Integrated Circuits and Systems, 25 (10) 1922-1934,2006.