James H. Kukula
(Jim's website: http://www.interdependentscience.com/kukula.html)
- starting March 2008
- 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
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
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.
My roles included
- 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
- Visiting Scientist at MIT
- IBM representative at industry consortium, CFI
- corporate standards committee chairman
- project leader
- M.S. Physics, University of Pennsylvania, 1981
- A.B. Physics summa cum laude, Princeton University, 1977
Scores on SAT test taken June 4, 2011:
- Critical Reading: 800
- Mathematics: 780
- Writing: 770
- August 1992 - May 1996
- Religious training in a traditional monastic retreat.
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
Per Bjesse, James Kukula,
"Using Counter Example Guided Abstraction Refinement to Find Complex Bugs",
Yunshan Zhu, James H. Kukula,
Robert Damiano, James Kukula,
"Checking Satisfiability of a Conjunction of BDDs"
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"
In-Ho Moon, Hee Hwan Kwak, James Kukula, Thomas Shiple, Carl Pixley,
"Simplifying Circuits for Formal Verification using Parametric Representation"
Pankaj Chauhan, Edmund Clarke, James Kukula, Samir Sapra, Helmut Veith,
"Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis"
Edmund M. Clarke, Anubhav Gupta, James Kukula, Ofer Strichman,
"SAT based abstraction-refinement using ILP and machine learning techniques",
A. Koelbl, J. Kukula, K. Antreich, R. Damiano,
"Handling Special Constructs in Symbolic Simulation",
P. Chauhan, E. Clarke, S. Jha, J. Kukula, T. Shiple, H. Veith, and D. Wang,
"Non-linear Quantification Scheduling in Image Computation",
D. Wang, E. Clarke, Y. Zhu, and J. Kukula,
"Using Cutwidth to Improve Symbolic Simulation and Boolean Satisfiability",
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"
Alfred Koelbl, James Kukula, and Robert Damiano,
"Symbolic RTL Simulation"
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,
Page(s): 332 -336
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"
James H. Kukula and Thomas R. Shiple,
"Building Circuits from Relations"
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",
James H. Kukula, Thomas R. Shiple, and Adnan Aziz,
"Techniques for Implicit State Enumeration of EFSMs",
Thomas R. Shiple, James H. Kukula, and Rajeev K. Ranjan,
"A Comparison of Presburger Engines for EFSM Reachability",
Adnan Aziz, Jim Kukula, and Tom Shiple,
"Hybrid Verification Using Saturated Simulation",
- 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",
James H. Kukula,
"Object Relocation in OX",
J. H. Kukula and S. Dasgupta,
"Object-Oriented Programming with Speculative Parallelism for Parallel
Conference Panel Presentations
"How to Break the Verification Bottleneck? Simulation vs. Emulation vs.
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