US PATENT No: US 11,620,424. Apr 4, 2023

• Transistor-level defect coverage and defect simulation,
  Inventors: Mayukh Bhattacharya, Sayandeep Sanyal, Amit Patra, Pallab Dasgupta.
  
  

  This patent describes a technique that identifies a small well-chosen subset of internal nets which, when probed, can increase the coverage of analog defects. Further, it describes a methodology to identify independent sub-circuits in Channel Connected Graph based abstraction of a netlist. Identification of such independent sub-circuits enables one to cover multiple defects in one simulation of the design. Thus, further reducing the time taken to reach a target percentage defect coverage.

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.

PSI-MINER

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

SaVerECS

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

CHAMS, DYFET AND FORFET: AMS ASSERTION AND FEATURE EVALUATION TOOLS

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

CoverT

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.

CHASSIS

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.

POWER-TRUCTOR

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.

RAILTOOLS FOR SIGNALING VALIDATION

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

GEN-STIMULI

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.

COV-ANALYZER

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.

SPEC-MATCHER

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.