James H. Kukula

Employment

from October 2012

Principal Scientist, 1EnergySystems. Developing software for real time management of electric power utility resources.

March 2008 to October 2012

self-employed provider of software development services

August 1996 to June 2007

Synopsys Scientist, Synopsys. Advancing CAD technology in verification and implementation tools.

• Investigated opportunities in clock tree synthesis and placement-oriented logic structuring.
• Led initial development of a hybrid verification system, combining multiple reachability engines to increase capacity of reachability algorithms. Developed initial system architecture, techniques for step-wise refinement of approximations, and heuristics for BDD-based image computation by early quantification. Managed four person research team.
• Developed automata-based decision procedure for Presburger arithmetic, applied to reachability on Extended Finite State Machines.
• Served as Associate Editor for IEEE Transactions on Computer-Aided Design

June 1982 - July 1992

Advisory Engineer, IBM Corp. CAD development.

• Boolean equivalence checking.
• State encoding algorithms for FSMs.
• Databases and schemas for CAD frameworks.
• Parallel processor hardware development.
• Operating system for object oriented parallel programs.
• Parallel algorithms: BDDs, event-driven simulation.
• Interactive schematic editor
• VHDL compiler

My roles included

• Visiting Scientist at MIT
• IBM representative at industry consortium, CFI
• corporate standards committee chairman
• project leader

Education

• M.S. Physics, University of Pennsylvania, 1981
• A.B. Physics summa cum laude, Princeton University, 1977

Personal

• Critical Reading: 800
• Mathematics: 780
• Writing: 770

August 1992 - May 1996

Religious training in a traditional monastic retreat.

Publications

Patents

• Phase abstraction for formal verification, #7,343,575, March 2008
• Method and apparatus for solving constraints, #7,257,786, August 2007
• Latch modeling technique for formal verification, #7,254,793, August 2007
• Method and apparatus for performing generator-based verification, #7,149,987, December 2006
• Method and apparatus for solving constraints, #7,107,553, August 2006
• Method and apparatus for formally constraining random simulation, #7,092,858, August 2006
• Method and System for Automata-Based Approach to State Reachability of Interacting Extended Finite State Machines, #6,059,837, May 2000
• Parallel Tables for Data Model with Inheritance, #5,418,961, May 1995
• Interrupt Mechanism for Multiprocessing System Having a Plurality of Interrupt Lines in Both a Global Bus and Cell Buses, #4,736,319, April 1988

Conference Proceedings

• Per Bjesse, James Kukula, "Using Counter Example Guided Abstraction Refinement to Find Complex Bugs", DATE 2004
• Yunshan Zhu, James H. Kukula, "Generator-Based Verification" ICCAD 2003
• Robert Damiano, James Kukula, "Checking Satisfiability of a Conjunction of BDDs" DAC 2003
• Per Bjesse, James Kukula, Robert Damiano, Ted Stanion, Yunshan Zhu, "Guiding SAT Diagnosis with Tree Decompositions", SAT 2003 (LNCS 2919)
• Hee H. Kwak, In-Ho Moon, James H. Kukula, Thomas R. Shiple, "Combinational Equivalence Checking through Function Transformation" ICCAD 2002
• In-Ho Moon, Hee Hwan Kwak, James Kukula, Thomas Shiple, Carl Pixley, "Simplifying Circuits for Formal Verification using Parametric Representation" FMCAD 2002
• Pankaj Chauhan, Edmund Clarke, James Kukula, Samir Sapra, Helmut Veith, Dong Wang, "Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis" FMCAD 2002
• Edmund M. Clarke, Anubhav Gupta, James Kukula, Ofer Strichman, "SAT based abstraction-refinement using ILP and machine learning techniques", CAV 2002
• A. Koelbl, J. Kukula, K. Antreich, R. Damiano, "Handling Special Constructs in Symbolic Simulation", DAC 2002
• P. Chauhan, E. Clarke, S. Jha, J. Kukula, T. Shiple, H. Veith, and D. Wang, "Non-linear Quantification Scheduling in Image Computation", ICCAD 2001
• D. Wang, E. Clarke, Y. Zhu, and J. Kukula, "Using Cutwidth to Improve Symbolic Simulation and Boolean Satisfiability", HLDVT 2001
• P. Chauhan, E. Clarke, S. Jha, J. Kukula, H. Veith, and D. Wang, "Using Combinatorial Optimization Methods for Quantification Scheduling", CHARME 2001 (LNCS 2144)
• Dong Wang, Pei-Hsin Ho, Jiang Long, James Kukula, Yunshan Zhu, Tony Ma, and Robert Damiano, "Formal Property Verification by Abstraction Refinement with Formal, Simulation, and Hybrid Engines" DAC 2001
• Alfred Koelbl, James Kukula, and Robert Damiano, "Symbolic RTL Simulation" DAC 2001
• Aziz, A.; Kukula, J.; Shiple, T.; Jun Yuan; "Efficient control state-space search", IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume: 20 Issue: 2, Feb 2001, Page(s): 332 -336
• Pei-Hsin Ho, Thomas R. Shiple, Kevin Harer, James H. Kukula, Robert Damiano, Valeria M. Bertacco, Jerry Taylor, John Elliott, and Jiang Long, "Smart Simulation Using Collaborative Formal and Simulation Engines" ICCAD 2000
• James H. Kukula and Thomas R. Shiple, "Building Circuits from Relations" CAV 2000
• In-Ho Moon, James Kukula, Kavita Ravi, and Fabio Somenzi, "To Split or to Conjoin: The Question in Image Computation" DAC 2000 Best Paper Award
• In-Ho Moon, James Kukula, Tom Shiple, and Fabio Somenzi, "Least Fixpoint Approximations for Reachability Analysis", ICCAD 1999
• James H. Kukula, Thomas R. Shiple, and Adnan Aziz, "Techniques for Implicit State Enumeration of EFSMs", FMCAD 1998
• Thomas R. Shiple, James H. Kukula, and Rajeev K. Ranjan, "A Comparison of Presburger Engines for EFSM Reachability", CAV 1998
• Adnan Aziz, Jim Kukula, and Tom Shiple, "Hybrid Verification Using Saturated Simulation", DAC 1998
• Jose Monteiro, James Kukula, Srinivas Devadas, and Horacio Neto, "Bitwise Encoding of Finite State Machines", Int'l Conf. on VLSI Design, 1994
• James Kukula and Srinivas Devadas, "Finite State Machine Decomposition by Transition Pairing", ICCAD 1991
• James H. Kukula, "Object Relocation in OX", ICCD 1988
• J. H. Kukula and S. Dasgupta, "Object-Oriented Programming with Speculative Parallelism for Parallel Processing", ICCD 1987

Conference Panel Presentations

• "How to Break the Verification Bottleneck? Simulation vs. Emulation vs. ????ation?", VLSI Circuits Symposium, 1999
• Industrial Formal Methods Panel, High Level Design Verification and Test Workshop, San Diego, November 1998

Published Technical Disclosures

• Parallel Event-Driven Simulation, August 1990
• Transform System for Boolean Comparison, March 1990
• Limiting Timing Analysis to Logically Consistent Paths, January 1990
• Use of Relocatable Objects to Facilitate Storage of Large Data Structures on Parallel Processors with Distributed Memory, January 1990
• Technique for Verifying Finite State Machines, August 1989
• Message Passing between Dynamically Relocatable Tasks, January 1988
• Building Block Multiprocessor Architecture, January 1988
• Dynamically Reconfigurable Microprocessing System, November 1986