Ching-Tsun Chou

Web:  http://home.pacbell.net/ctchou

Cell:  (650) 283-4894
chingtsun_chou@yahoo.com

Work:  (408) 765-5468
ching-tsun.chou@intel.com

Summary

Dr Ching-Tsun Chou brings an uncommon combination of experiences.  First and foremost, he has hands-on experience with all aspects of applying formal methods to real-world verification problems in industry.  In terms of application areas, he has worked on RTL designs, complex hardware and distributed protocols, software algorithms, architectural specifications, and even the search for deadlock-free wormhole routing.  In terms of techniques, he has extensive experience in model checking, mechanical theorem proving, and symbolic trajectory evaluation and has published on some aspects of these topics in respected journals and conferences.  Second, his experience is by no means limited to formal methods.  Among other things, he has participated in the design and specification of complex cache coherence protocols and error recovery protocols, performed hardware verification using traditional simulation-based techniques, implemented nontrivial verification tool chains, analyzed the error-control performance of error detection and correction codes, and investigated the automatic generation of hardware from synchronous languages.  Third, having worked in hardware design teams, he has intimate and personal knowledge of the enormous complexities of industrial hardware designs, of the kind of time and resource pressures under which design teams operate, and of the team-oriented collaborative nature of such endeavors.  Last but not least, he enjoys programming very much and would not let go any opportunities where his programming skills can be put to good use.

Education

University of California, Los Angeles - Los Angeles, CA
Ph.D. in Computer Science -1995

University of California, Los Angeles - Los Angeles, CA
M.S. in Computer Science - 1986

National Taiwan University - Taipei, Taiwan
B.S. in Electrical Engineering - 1983

Industry Experience

Senior Platform Architect and Verification Engineer
Intel Corporation - Santa Clara, CA.  August 1999 to Present.

·         Technical lead of the verification of several protocols for distributed shared memory systems, including directory-based cache coherence protocols, shared bus protocols, link layer protocols, and error recovery protocols (see paper 3 below).  Contributed significantly to the design and specification of some of these protocols.

·         Designed and implemented a verification tool chain that automatically generates both formal and simulation models from table-based specifications, including translators from SMV and Murphi to C reference models.

·         Worked closely with design teams to implement the protocols.  Helped to integrate C reference models into RTL validation environment.  Reviewed RTL code and advised and helped with verification efforts.

·         Reviewed and participated in the design of cyclic redundancy checks (CRC) and error correction codes (ECC).

·         Managed academic relations with faculties at Stanford University and University of Utah (see paper 2 and paper 4 below).

Senior Verification Engineer
Intel Corporation - Santa Clara, CA.  March 1997 to August 1999.

·         Did both formal and simulation-based verification of RTL design from the Itanium™ microprocessor, with special emphasis on memory subsystem and system bus interface.  Found numerous bugs.  Did extensive script coding to automate many tasks.

·         Wrote a well-regarded paper on the mathematical foundation of symbolic trajectory evaluation (see paper 5 below).

VLSI CAD Researcher
Fujitsu Laboratories of America - Sunnyvale, CA.  October 1995 to March 1997.

·         Designed an Esterel-like synchronous programming language for use in hardware design (see paper 7 below).

·         Investigated the feasibility of doing synchronous programming in Verilog HDL (see paper 16 below).

Postgraduate Researcher
AT&T (later Lucent) Bell Laboratories - Murray Hill, NJ.  June 1995 to October 1995.

·         Did formal verification by mechanical theorem proving of a partial-order reduction technique for model checking (see paper 6 below).

Summer Intern
IBM T.J. Watson Research Center - Yorktown Heights, NY.  June 1986 to October 1986.

·         Designed and analyzed distributed algorithms for a high-performance voice/data integrated network architecture (see paper 13 and paper 14 below).

Summer Intern
IBM T.J. Watson Research Center - Yorktown Heights, NY.  June 1985 to October 1985.

·         Designed a procedure call mechanism for an expert system language.

Summer Intern
Silogic, Inc. - Los Angeles, CA.  June 1984 to October 1984.

·         Did extensive Prolog programming.

Teaching Experience

Part-Time Faculty
Loyola Marymount University - Los Angeles, CA.  Fall 1993.

·        Taught courses on automata, formal languages, and computability theory at both undergraduate and graduate level.

Teaching Assistant
University of California, Los Angeles - Los Angeles, CA.  Spring 1987.

·        Prepared homework problems, conducted discussion sessions, and graded students’ answers for a graduate course on probability and queuing theories.

Programming Experience

  • Some programming projects undertaken (in no particular order):
    1. Machine-assisted checking of mathematical theories (e.g., see paper 6 below for substantial sample code).
    2. Language processing (e.g., SMV®C and Murphi®C translations, sophisticated abstract syntax tree manipulation, Prolog type inference).
    3. Automation scripts (e.g., wrapper file generation for linking HDL units, extraction and manipulation of signal traces from trace files, extraction and flattening of tables from HTML).
    4. Numerical programs (e.g., learning algorithms for neural networks and classification trees, soft k-means clustering, sequence alignments by dynamic programming, heuristic progressive multiple sequence alignments, profile hidden Markov models).
    5. Run-time interfacing of different languages (e.g., driving a protocol simulator in C from Caml and using the garbage collector of the latter to manage the data structures used by the former).
  • Some programming languages used:  C, Fortran, Lisp, Prolog, Caml (http://caml.inria.fr/), Java, Perl, Verilog, VHDL.

Selected Publications (for a more complete list, see: http://dblp.uni-trier.de/db/indices/a-tree/c/Chou@Ching=Tsun.html)

  1. Ching-Tsun Chou, Phanindra K. Mannava, and Seungjoon Park, “A Simple Method for Parameterized Verification of Cache Coherence Protocols”, Formal Methods in Computer-Aided Design (FMCAD’04), Austin, Texas, 14-17 November 2004.
  2. Ganesh Gopalakrishnan and Ching-Tsun Chou, “The Post-Silicon Verification Problem: Designing Limited Observability Checkers for Shared Memory Processors”, Designing Correct Circuits (DCC’04), Barcelona, Spain, 27-28 March 2004.
  3. Mani Azimi, Ching-Tsun Chou, Akhilesh Kumar, Victor W. Lee, Phanindra K. Mannava, and Seungjoon Park, “Experience with Applying Formal Methods to Protocol Specification and System Architecture”, Formal Methods in System Design, Vol. 22, pp. 109-116, 2003.
  4. Kanna Shimizu, David L. Dill, and Ching-Tsun Chou, “A Specification Methodology by a Collection of Compact Properties as Applied to the Intel Itanium Processor Bus Protocol”, Proceedings of Conference on Correct Hardware Design and Verification Methods (CHARME’01), Livingston, Scotland, 4-7 September 2001.
  5. Ching-Tsun Chou, "The Mathematical Foundation of Symbolic Trajectory Evaluation", pp. 196-207 of Lecture Notes in Computer Science 1633: Proceedings of 11th Int. Conf. on Computer-Aided Verification (CAV'99), Trento, Italy, July 1999.
  6. Ching-Tsun Chou and Doron Peled, "Formal Verification of a Partial-Order Reduction Technique for Model Checking", Journal of Automated Reasoning, 23(3-4):265-298, 1999.
  7. Ching-Tsun Chou, Jiun-Lang Huang, and Masahiro Fujita, "A High-Level Language for Programming Complex Temporal Behaviors and Its Translation into Synchronous Circuits", pp. 74-76 of Proceedings of  IFIP Conf. on Hardware Description Languages and Their Applications (CHDL'97), Toledo, Spain, April 1997.
  8. Ching-Tsun Chou, "Simple Proof Techniques for Property Preservation via Simulation", Information Processing Letters, Vol. 60, pp. 129-134, 1996.
  9. Ching-Tsun Chou, "Mechanical Verification of Distributed Algorithms in Higher-Order Logic", The Computer Journal, Vol. 38, No. 2, pp. 152-161, 1995.
  10. Ching-Tsun Chou, "A Formal Theory of Undirected Graphs in Higher-Order Logic", pp. 144-157 of Lecture Notes in Computer Science 859: 7th Int. Workshop on Higher Order Logic Theorem Proving and Its Applications (HOL'94), Valletta, Malta, September 1994.
  11. Ching-Tsun Chou, "A Note on Interactive Theorem Proving with Theorem Continuation Functions", pp. 59-70 of 5th Int. Workshop on Higher Order Logic Theorem Proving and Its Applications (HOL'92), Leuven, Belgium, September 1992.
  12. Ching-Tsun Chou, "A Sequent Formulation of a Logic of Predicates in HOL", pp. 71-80 of 5th Int. Workshop on Higher Order Logic Theorem Proving and Its Applications (HOL'92), Leuven, Belgium, September 1992.
  13. Ching-Tsun Chou, Israel Cidon, Inder S. Gopal, and Shmuel Zaks, "Synchronizing Asynchronous Bounded Delay Networks", IEEE Trans. on Communications, Vol. 38, No. 2, pp. 144-147, February 1990.
  14. Ching-Tsun Chou and Inder S. Gopal, "Linear Broadcast Routing", Journal of Algorithms, Vol. 10, No. 4, pp. 490-517, December 1989.
  15. Ching-Tsun Chou and Eli Gafni, "Understanding and Verifying Distributed Algorithms Using Stratified Decomposition", 7th ACM Symp. on Principles of Distributed Computing (PODC'88), pp. 44--65, August 1988.

Unpublished Manuscripts

  1. Ching-Tsun Chou, "Synchronous Verilog: A Proposal", 1997.
  2. Ching-Tsun Chou, "Using Operational Intuition about Events and Causality in Assertional Proofs", 1995.
  3. Ching-Tsun Chou, "A Bug in the Distributed Minimum Spanning Tree Algorithms of Gallager, Humblet, and Spira", 1988.

Invited Talks

  1. Ching-Tsun Chou, Steven German, and Ganesh Gopalakrishnan, “Specification and Verification of Shared Memory Protocols and Consistency Models”,Formal Methods in Computer-Aided Design (FMCAD’04), Austin, Texas, 14-17 November 2004.
  2. Ching-Tsun Chou, “A Taste of Formal Verification and Its Industrial Applications”, Santa Clara University, 20 February 2003.
  3. Ching-Tsun Chou, “Formal Verification of an Industrial Cache Coherence Protocol”, San Jose State University, 14 November 2002.

Member of Conference Program Committees

Member of Professional Societies

Patents:  One pending.

Miscellaneous

 

This page was last updated on 20 June 2005.