Christian Jacobi

IBM Development Germany
Dept. 3245 / Processor Development
Schoenaicherstr. 220
D-71032 Boeblingen, Germany

Tel: +49 7031 16-3538
Fax: +49 7031 16-2829
email: cjacobi at de.ibm.com
Privat:
Lange Str. 19
D-71101 Schönaich
Germany



Education and Research and Development Interests

  • I studied Computer Science at Saarland University, Germany. I received a degree as "Diplom Informatiker" (Master Computer Science) in 1999.
  • From 1999 to 2002, I was affiliated with Saarland University, Institute for Computer Architecture, as a Research Assistant; in 2002 I finished my doctoral thesis "Formal Verification of a Fully IEEE Compliant Floating Point Unit" and received a doctoral degree in computer science.
  • My current interests are microprocessor design and (formal) verification, in particular in the area of memory caches; previously I have worked on floating point units, automatic formal verification, theorem proving, and logic and physical design.
In 2002, I joined IBM Germany. Currently, I am working in the area of logic design and verification for upcoming high-performance processors.


Thesis

  • Master thesis: Ein relationales Datenbanksystem für die SB-PRAM; Concurrency Control und der TPC-B-Benchmark (in German; A relational database system for the SB-PRAM; concurrency control and the TPC-B Benchmark)
    (pdf) (bibtex)
  • Doctoral thesis: Formal Verification of a Fully IEEE Compliant Floating Point Unit
    (abstract) (pdf) (bibtex)



Publications

Journal Papers

  • Formal Verification of the VAMP Floating Point Unit
    Christian Jacobi, Christoph Berg
    Formal Methods in System Design, Vol 26:3, pg 227-266, Springer, 2005
    (abstract) (pdf) (bibtex)

  • Putting it all together – Formal verification of the VAMP
    Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul
    International Journal on Software Tools for Technology Transfer (STTT), Vol 8:4-5, Springer, 2006
    (abstract) (pdf)

  • A fully pipelined single-precision floating-point unit in the synergistic processor element of a CELL processor
    Hwa-Joon Oh, Silvia M. Mueller, Christian Jacobi, Kevin D. Tran, Scott R. Cottier, Brad W. Michael, Hiroo Nishikawa, Yonetaro Totsuka, Tatsuya Namatame, Naoka Yano, Takashi Machida, Sang H. Dhong
    IEEE Journal of Solid-State Circuits, Vol. 41:4, pg 759-771, IEEE, 2006
    (abstract) (pdf)

  • IBM POWER6 accelerators: VMX and DFU
    Lee Eisen, J. J. Wes Ward III, Hans-Werner Tast, Nicolas Mäding, Jens Leenstra, Silvia M. Mueller, Christian Jacobi, Jochen Preiss, Eric M. Schwarz, Steven R. Carlough
    IBM Journal of Research and Development, Vol. 51:6, IBM, 2007
    (abstract) (pdf)

Conference Papers

  • Highly concurrent locking in shared memory database systems
    Christian Jacobi, Cédric Lichtenau
    Proceedings of EUROPAR '99, Springer LNCS 1685, pg 477, 1999
    (abstract) (pdf) (bibtex)

  • Proving the Correctness of a Complete Microprocessor
    Christian Jacobi, Daniel Kröning
    Informatik 2000, 30. Jahrestagung der Gesellschaft für Informatik, Springer-Verlag Informatik aktuell, 2000
    (abstract) (pdf) (bibtex)

  • Formal Verification of a Basic Circuits Library
    Christoph Berg, Christian Jacobi, Daniel Kröning
    Proceedings of the IASTED International Conference on Applied Informatics, Innsbruck (AI 2001), ACTA Press, 2001
    (abstract) (pdf) (bibtex)

  • Formal Verification of the VAMP Floating Point Unit
    Christoph Berg, Christian Jacobi
    Proceedings of 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Springer LNCS 2144, pg 325, 2001
    (abstract) (pdf) (bibtex)

  • Formal Verification of Complex Out-of-order Pipelines by Combining Model-Checking and Theorem-Proving
    Christian Jacobi
    Proceedings of Computer Aided Verification, 14th International Conference (CAV 2002), Springer LNCS 2404, pg 309, 2002
    (abstract) (pdf) (bibtex)

  • Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation
    Michael Backes, Christian Jacobi, Birgit Pfitzmann
    Proceedings of FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe (FME 2002), Springer LNCS 2391, pg 310, 2002
    (abstract) (pdf) (bibtex)

  • Cryptographically Sound and Machine-Assisted Verification of Security Protocols
    Michael Backes, Christian Jacobi
    Proceedings of STACS 2003, 20th Annual Symposium on Theoretical Aspects of Computer Science, Springer LNCS 2607, pg 675, 2003
    (abstract) (pdf) (bibtex)

  • Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP Processor
    Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul
    Proceedings of 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Springer LNCS 2860, pg 51, 2003
    (abstract) (pdf) (bibtex)

  • Efficient Symbolic Simulation via Dynamic Scheduling, Don’t Caring, and Case Splitting
    Viresh Paruthi, Christian Jacobi, Kai Weber
    Proceedings of 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Springer LNCS 3725, pg 114, 2005
    (abstract) (pdf)

  • Automatic Formal Verification of Fused-Multiply-Add FPUs
    Christian Jacobi, Kai Weber, Viresh Paruthi, Jason Baumgartner
    Proceedings of Design, Automation and Test in Europe (DATE'05), IEEE, 2005
    (abstract) (pdf)

  • The vector floating-point unit in a synergistic processor element of a CELL processor Silvia Mueller, Christian Jacobi, Hwa-Joon Oh, Kevin D. Tran, Scott R. Cottier, Brad W. Michael, Hiroo Nishikawa, Yonetaro Totsuka, Tatsuya Namatame, Naoka Yano, Takashi Machida, Sang H. Dhong
    Proceedings of the 17th IEEE Symposium on Computer Arithmetic (ARITH 05), IEEE, 2005
    (abstract) (pdf)

  • A fully-pipelined single-precision floating point unit in the synergistic processor element of a CELL processor
    Hwa-Joon Oh, Silvia M. Mueller, Christian Jacobi, Kevin D. Tran, Scott R. Cottier, Brad W. Michael, Hiroo Nishikawa, Yonetaro Totsuka, Tatsuya Namatame, Naoka Yano, Takashi Machida, Sang H. Dhong
    IEEE Symposium on VLSI Circuits (VLSI'05), IEEE, 2005
    (abstract) (pdf)

  • Evaluating Coverage of Error Detection Logic for Soft Errors using Formal Methods
    Udo Krautz, Matthias Pflanz, Christian Jacobi, Hans-Werner Tast, Kai Weber, Heinrich T. Vierhaus
    Proceedings of Design, Automation and Test in Europe (DATE'06), IEEE, 2006
    (abstract) (pdf)

  • Verifying full-custom multipliers by Boolean equivalence checking and an arithmetic bit level proof
    Udo Krautz, Markus Wedler, Wolfgang Kunz, Kai Weber, Christian Jacobi, Matthias Pflanz
    Proceedings of Asia and South Pacific Design Automation Conference (ASPDAC 2008), IEEE, 2008
    (abstract) (pdf)

Invited Talks

  • Formal Verification in Industry -- Current State and Future Directions
    Presented at FMCAD Workshop 2006, San Jose, CA.
    (Powerpoint)

Workshop Papers / Posters / Technical Reports

  • Formal Verification of a Theory of IEEE Rounding
    Christian Jacobi
    Theorem Proving in Higher-Order Logics (TPHOLs) 2001: Supplemental Proceedings; Informatics Research Report EDI-INF-RR-0046, Univ. Edinburgh, UK, 2001
    (abstract) (pdf) (bibtex)

  • Formal Verification of the VAMP processor (Project Status)
    Christoph Berg, Sven Beyer, Christian Jacobi, Daniel Kröning, Dirk Leinenbach
    Symposium on the Effectiveness of Logic in Computer Science (ELICS02), Technical Report MPI-I-2002-2-007, Max-Planck-Institut für Informatik, Saarbruecken, Germany, 2002
    (abstract) (pdf) (bibtex)

1