Florian K Krohm

US Patent:

6473884, Oct 29, 2002

Filed:

Mar 14, 2000

Appl. No.:

09/524890

Inventors:

Malay Kumar Ganai - Austin TX
Geert Janssen - Putnam Valley NY
Florian Karl Krohm - Red Hook NY
Andreas Kuehlmann - Austin TX
Viresh Paruthi - Austin TX

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 1750

US Classification:

716 3, 716 2, 716 5, 716 6, 716 17, 716 19

Abstract:

A method and system for equivalence checking of logical circuits using iterative circuit reduction and satisfiability techniques provide improved performance in computer-based verification and design tools. By intertwining a structural satisfiability solver and binary decision diagram functional circuit reduction method, computer-based tools can make more efficient use of memory and decrease computation time required to equivalence check large logical networks. Using the circuit reduction technique back-to-back with the simulation technique, optimum local and global circuit reduction are simultaneously achieved. By iterating between the structural and functional techniques, and adjusting the size of sub-networks being analyzed within a larger network, sub-networks can be reduced or eliminated, decreasing the amount of memory required to represent the next larger inclusive network.

US Patent:

7089542, Aug 8, 2006

Filed:

Dec 13, 2002

Appl. No.:

10/318823

Inventors:

Daniel Brand - Millwood NY, US
John A. Darringer - Mahopac NY, US
Florian Krohm - Hyde Park NY, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 9/45
G06F 9/44

US Classification:

717143, 717155, 717156

Abstract:

A method and apparatus are provided for analyzing software programs. The invention combines data flow analysis and symbolic execution with a new constraint solver to create a more efficient and accurate static software analysis tool. The disclosed constraint solver combines rewrite rules with arithmetic constraint solving to provide a constraint solver that is efficient, flexible and capable of satisfactorily expressing semantics and handling arithmetic constraints. The disclosed constraint solver comprises a number of data structures to remember existing range, equivalence and inequality constraints and incrementally add new constraints. The constraint solver returns an inconsistent indication only if the range constraints, equivalence constraints, and inequality constraints are mutually inconsistent.

US Patent:

7168009, Jan 23, 2007

Filed:

Sep 24, 2003

Appl. No.:

10/669306

Inventors:

John A. Darringer - Mahopac NY, US
Daniel Brand - Millwood NY, US
Florian Krohm - Hyde Park NY, US

Assignee:

International Business Machines Corporation - Armonk NY

International Classification:

G06F 11/00

US Classification:

714 38, 714 35, 714 37, 717124, 717126

Abstract:

Disclosed are a method and system for analyzing a computer program. The method comprises the steps of analyzing the program to generate an initial error report and a list of suspected error conditions, and generating a set of assertions and inserting the assertions into the program to determine if the suspected error conditions are valid. Preferably, a strong static analysis method is used to identify an initial set of error reports. When this analysis fails to determine if the condition is true or false, the condition along with the potential program error is captured to form a suspected error. Suspected errors are directed to an assertion generator to produce a monitor—that is, source code modification that is integrated with the original program. This and other inserted monitors check the conditions for the suspected error during the program execution.

US Patent:

60351071, Mar 7, 2000

Filed:

Aug 28, 1997

Appl. No.:

8/919736

Inventors:

Andreas Kuehlmann - Poughkeepsie NY
Florian Karl Krohm - Millbrook NY

Assignee:

International Bunsiness Machines Corporation - Armonk NY

International Classification:

G06F 1750

US Classification:

39550002

Abstract:

A verification technique which is specifically adapted for formally comparing large combinational circuits with some structural similarities. The approach combines the application of Binary Decision Diagrams (BDDs) with circuit graph hashing, automatic insertion of multiple cut frontiers, and a controlled elimination of false negative verification results caused by the cuts. Multiple BDDs are computed for the internal nets of the circuit, originating from the cut frontiers, and the BDD propagation is prioritized by size and discontinued once a given limit is exceeded. The resulting verification engine is reliably accurate and efficient for a wide variety of practical hardware designs ranging from identical circuits to designs with very few similarities.