US PATENT No: US 7,797,123 Sep 14, 2010

  • Method and Apparatus for Extracting Assume Properties from a Constrained Random Test Bench,
    Inventors: K.Dey, E.Cerny, Pallab Dasgupta, B.Pal, P.P.Chakrabarti.

    This patent describes a technique for automatically extracting formal logical constraints on the environment of a circuit, where the environment is described by means of a test-bench developed in SystemVerilog. Developing environment constraints (called assume properties) is a non-trivial task and is one of the main concerns in formal verification of reactive systems. The patented technique automated this problem. The patent was jointly obtained with collaborators from Synopsys Inc, and is assigned to Synopsys.

US PATENT No: US 8,082,140, Dec 20, 2011

  • Parametric Analysis of Real Time Response Guarantees on Interacting Software Components,
    Inventors: M.Dixit, S.Ramesh, Pallab Dasgupta.

    This patent describes a technique for automatic extraction of linear constraints on the timing of constraint behaviors that are obtained by formally comparing the conjunction of component specifications with formal time-critical end-to-end behaviors in automotive features. The patented technique enables early timing analysis with the help of formal specifications in the development of automotive control features and sub-system technical specifications. The patent was jointly obtained with collaborators from General Motors, and is assigned to General Motors.

Tools Developed And Maintained by The Research Group


This is a first of its kind tool for finding temporal causal relations for explaining events in time series data. Developed under a Intel CAD-SRS research grant, this tool is available in the public domain: GitHub Link


This is a SMT-based verification tool to formally guarantee the performance and safety of an embedded control software under the influence of process or measurement noises and timing uncertainties (delay, jitters), before implementing them in real-time systems. Support for non-linearities in the controlled plant and the controller software, real-valued constraints and control software code as input, make this tool-chain ideal for verifying real-world hybrid systems. Our tool incorporates semantic support for capturing plant specifications, timing and value-based uncertainties (noise, precision errors), and the control software code. GitHub Link


This tool suite enables any standard AMS circuit simulator to monitor analog time domain properties and features. These were developed under a recent project sponsored by the Semiconductor Research Corporation (SRC) which is a consortium of semiconductor and EDA companies. One version of this tool has been adopted by Freescale Semiconductors (now NXP). The ForFET tool is now available in the public domain: GitHub Link


This tool has been developed for Texas Instruments under a research contract from Semiconductor Research Corporation. This is a coverage management tool for large analog and mixed signal integrated circuits. The tool has been integrated into TI’s verification environment.


Verification tool for integrated power management chips. This tool was developed under a collaboration with National Semiconductor Corp, UK for verifying integrated PMUs, which are large scale analog-mixed circuits consisting of linear drop-out regulators, buck regulators and battery chargers. The tool introduced the use of behavioral models based on hybrid automata into the design validation flow of National semiconductors.


Formal verification tool for verifying the architectural power management strategy in large digital integrated circuits. This tool has been developed under the Synopsys CAD Laboratory at IIT Kharagpur.


This tool suite proves the correctness of signaling logic developed for electronic signaling and interlocking systems using formal methods. The tool has been tested on several railway yards in India and is now being considered by RDSO for widespread adoption in the Indian Railways.

Past Tools – Not Maintained Anymore


This tool was developed for generating minimum length stimulus patterns for custom cell characterization. Adopted by National Semiconductors, this tool uses formal state space analysis to find the shortest stimuli for characterization tests like setup and hold.


Formal verification coverage analysis tool. This tool has been integrated with the Forspec/Forecast tool suite of Intel with collaboration with the electronic design automation group at Intel, Haifa. The development of this tool was sponsored by the chipset design group at Intel, Folsom, USA.


Formal design intent verification tool for digital integrated circuits. This tool was also developed under the research collaboration with Intel. These contributions have been noted in the article, Fifteen Years of Formal Property Verification at Intel by Dr Limor Fix, Director, Intel Research Lab, Pittsburgh, in the book, 25 Years of Model Checking, Springer, 2008, ISBN: 978-3-540-69849-4.