Page archived courtesy of the Geocities Archive Project https://www.geocitiesarchive.org
Please help us spread the word by liking or sharing the Facebook link below :-)


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