Hongce Zhang

Hongce Zhang

Assistant Professor in Microelectronics Thrust, HKUST(GZ)

Hong Kong University of Science and Technology (Guangzhou)

Biography

Hongce Zhang is an Assistant Professor at the Microelectronics Thrust, Function Hub of the Hong Kong University of Science and Technology (Guangzhou). He is also affiliated with the Division of Emerging Interdisciplinary Areas (EMIA) of HKUST. He received his PhD from the Electrical and Computer Engineering Department of Princeton University in 2021, advised by Professor Sharad Malik.

Please note that Hongce is now using the Guangzhou campus e-mail address (hongcezh AT hkust-gz.edu.cn). If you have saved his previous CWB address (hongcezh AT ust.hk), please kindly update your contact list. Thanks!

Interests
  • Hardware Formal Verification
  • Model Checking
  • Logic Design and Verification
Education

  • PhD in Electrical and Computer Engineering, 2021

    Princeton University

  • BSc in Microelectronics, 2015

    Shanghai Jiao Tong University

Open Positions

I’m looking for talented students (PhD/RA) who are interested in exploring topics around hardware verification, firmware and systems-on-chip security. Some of the work in this area is closely related to the electronic design automation (EDA) industry and I expect such topics will receive increasingly more focus and support in the near future. Unlike PhD/RA, MPhil admission is committee-based. For more information regarding the MPhil program at HKUST(GZ), please refer to this webpage.

Current Students

PhD

UG

Past Students

PhD

MPhil

Projects

E-Syn and E-morphic
E-graph for logic optimization.
PDF Code
MasterRTL
Early-stage power performance & area prediction.
PDF Code
NeuroPDR and DeepIC3
Machine-learning-aided hardware model checking algorithms.
PDF Code
WASIM
A word-level abstract symbolic simulator on RTL. We are currently developing the next generation with its core functionalities in C++, based on SMT-Switch framework. Join us if you are interested.
PDF Code
ILAng
Systems-on-Chip specification and verification, part of Upscale. PhD work.

Teaching

MICS5510 Formal Methods and Testing for Electronic System Verification
The course will discuss the application of automated reasoning techniques in the verification of software and hardware components in electronic systems. It will cover basic knowledge of logic, satisfiability solvers, model checking and their applications. This course also includes topics on circuit testing (pre-silicon & post-silicon).
Sep 4, 2024 1:30 PM — Dec 4, 2024 4:20 PM E4-201
MICS6000H Logic Design Automation of Digital Systems
Logic design and physical design are two major steps in the digital design process. This course is an introduction to the automation techniques in the logic design step. It covers the workflow from hardware description languages to gate-level netlists. In this course, we will discuss the theoretic foundations, including the basics of automata theory, lexing, parsing, synthesis and minimization of two-level and multi-level circuits, finite-state machine synthesis and verification, technology mapping, automatic test generation and timing analysis. This course, for the first time, connects frontend techniques of compilers with the introduction of logic synthesis. Compiling techniques and digital logic were typically taught in two separate courses. The combination in this course is intended to provide a more comprehensive view of the underlying techniques of modern logic design automation tools.
Sep 7, 2022 9:00 AM — Dec 7, 2022 11:50 AM Rm 103, E1 Computational Labs (mixed-mode)
FUNH6800A (T1) Function Hub Seminar
N/A
Sep 6, 2021 6:00 PM — Nov 29, 2021 6:00 PM Online

Services

Conference Technical Program Committee

  • Design Automation Conference (DAC) 2022, 2023, 2026
  • Computer-Aided Verification (CAV) 2024
  • International Conference on Computer-Aided Design (ICCAD) 2025, 2026
  • Formal Methods in Computer-Aided Design (FMCAD) 2024, 2025, 2026
  • Asia and South Pacific Design Automation Conference (ASP-DAC) 2026
  • International Conference on Computer Design (ICCD) 2025 (Track Chair)
  • ACM/IEEE International Symposium on Machine Learning for CAD (MLCAD) 2024, 2025, 2026
  • Great Lakes Symposium on VLSI (GLSVLSI) 2025, 2026
  • International Symposium of EDA (ISEDA) 2025, 2026 (Track Chair)

Journal Reviewer

  • IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)
  • ACM Transactions on Design Automation of Electronic Systems (TODAES)
  • IEEE Transactions on Circuits and Systems Part II (TCAS-II)
  • IEEE Journal on Emerging and Selected Topics in Circuits and Systems (JETCAS)
  • Formal Methods in System Design (FMSD)
  • Frontiers of Computer Science
  • Electronics
  • Computer Aided Design (CADJ)

Some Useful Information

How to convert Verilog to btor2 or aiger format
How to find combinational logic loops in iverilog/vvp?
See all posts