A hardware-based technique for efficient implicit information flow tracking. - Jangseop Shin; Hongce Zhang; Jinyong Lee; Ingoo Heo; Yu-Yuan Chen; Ruby B. Lee; Yunheung Paek (ICCAD, 2016)

ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. - Hongce Zhang; Caroline Trippel; Yatin A. Manerkar; Aarti Gupta; Margaret Martonosi; Sharad Malik (FMCAD, 2018)

ILAng: A Modeling and Verification Platform for SoCs Using Instruction-Level Abstractions. - Bo-Yuan Huang 001; Hongce Zhang; Aarti Gupta; Sharad Malik (TACAS (1), 2019)

Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. - Bo-Yuan Huang 001; Hongce Zhang; Pramod Subramanyan; Yakir Vizel; Aarti Gupta; Sharad Malik (ACM Trans. Design Autom. Electr. Syst., 2019)

Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. - Hongce Zhang; Maxwell Shinn; Aarti Gupta; Arie Gurfinkel; Nham Le; Nina Narodytska (ECAI, 2020)

In Search for a SAT-friendly Binarized Neural Network Architecture. - Nina Narodytska; Hongce Zhang; Aarti Gupta; Toby Walsh (ICLR, 2020)

Synthesizing Environment Invariants for Modular Hardware Verification. - Hongce Zhang; Weikun Yang; Grigory Fedyukovich; Aarti Gupta; Sharad Malik (VMCAI, 2020)

Pono: A Flexible and Extensible SMT-Based Model Checker. - Makai Mann; Ahmed Irfan; Florian Lonsing; Yahan Yang; Hongce Zhang; Kristopher Brown; Aarti Gupta; Clark W. Barrett (CAV (2), 2021)

Generating Architecture-Level Abstractions from RTL Designs for Processors and Accelerators Part I: Determining Architectural State Variables. - Yu Zeng; Bo-Yuan Huang 001; Hongce Zhang; Aarti Gupta; Sharad Malik (ICCAD, 2021)

Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking. - Hongce Zhang; Aarti Gupta; Sharad Malik (VMCAI, 2021)

INVITED: Generalizing the ISA to the ILA: A Software/Hardware Interface for Accelerator-rich Platforms. - Bo-Yuan Huang 001; Hongce Zhang; Aarti Gupta; Sharad Malik (DAC, 2023)

MasterRTL: A Pre-Synthesis PPA Estimation Framework for Any RTL Design. - Wenji Fang; Yao Lu; Shang Liu 006; Qijun Zhang; Ceyu Xu; Lisa Wu Wills; Hongce Zhang; Zhiyao Xie (ICCAD, 2023)

NeuroPDR: Integrating Neural Networks in the PDR Algorithm for Hardware Model Checking. - Guangyu Hu; Wei Zhang 012; Hongce Zhang (MLCAD, 2023)

WASIM: A Word-level Abstract Symbolic Simulation Framework for Hardware Formal Verification. - Wenji Fang; Hongce Zhang (TACAS (2), 2023)

Addressing Variable Dependency in GNN-based SAT Solving. - Zhiyuan Yan 003; Min Li 019; Zhengyuan Shi; Wenjie Zhang; Yingcong Chen; Hongce Zhang (CoRR, 2023)

RTLCoder: Outperforming GPT-3.5 in Design RTL Generation with Our Open-Source Dataset and Lightweight Solution. - Shang Liu 006; Wenji Fang; Yao Lu; Qijun Zhang; Hongce Zhang; Zhiyao Xie (CoRR, 2023)

r-map: Relating Implementation and Specification in Hardware Refinement Checking. - Wenji Fang; Guangyu Hu; Hongce Zhang (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2023)

DeepIC3: Guiding IC3 Algorithms by Graph Neural Network Clause Prediction. - Guangyu Hu; Jianheng Tang; Changyuan Yu; Wei Zhang 012; Hongce Zhang (ASPDAC, 2024)

E-Syn: E-Graph Rewriting with Technology-Aware Cost Functions for Logic Synthesis. - Chen Chen; Guangyu Hu; Dongsheng Zuo; Cunxi Yu; Yuzhe Ma; Hongce Zhang (DAC, 2024)

Annotating Slack Directly on Your Verilog: Fine-Grained RTL Timing Evaluation for Early Optimization. - Wenji Fang; Shang Liu 006; Hongce Zhang; Zhiyao Xie (DAC, 2024)

AsymSAT: Accelerating SAT Solving with Asymmetric Graph-Based Model Prediction. - Zhiyuan Yan 003; Min Li 019; Zhengyuan Shi; Wenjie Zhang; Yingcong Chen; Hongce Zhang (DATE, 2024)

Word-Level Augmentation of Formal Proof by Learning from Simulation Traces. - Zhiyuan Yan 003; Hongce Zhang (ICCAD, 2024)

AssertLLM: Generating and Evaluating Hardware Verification Assertions from Design Specifications via Multi-LLMs. - Wenji Fang; Mengming Li; Min Li 019; Zhiyuan Yan 003; Shang Liu 006; Hongce Zhang; Zhiyao Xie (CoRR, 2024)

AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs. - Zhiyuan Yan 003; Wenji Fang; Mengming Li; Min Li 019; Shang Liu 006; Zhiyao Xie; Hongce Zhang (ASP-DAC, 2025)

A Self-Supervised, Pre-Trained, and Cross-Stage-Aligned Circuit Encoder Provides a Foundation for Various Design Tasks. - Wenji Fang; Shang Liu 006; Hongce Zhang; Zhiyao Xie (ASP-DAC, 2025)

Word-Level Counterexample Reduction Methods for Hardware Verification. - Zhiyuan Yan 003; Hongce Zhang (DATE, 2025)

Transferable Presynthesis PPA Estimation for RTL Designs With Data Augmentation Techniques. - Wenji Fang; Yao Lu; Shang Liu 006; Qijun Zhang; Ceyu Xu; Lisa Wu Wills; Hongce Zhang; Zhiyao Xie (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2025)

NetTAG: A Multimodal RTL-and-Layout-Aligned Netlist Foundation Model via Text-Attributed Graph. - Wenji Fang; Wenkai Li; Shang Liu 006; Yao Lu; Hongce Zhang; Zhiyao Xie (CoRR, 2025)

E-morphic: Scalable Equality Saturation for Structural Exploration in Logic Synthesis. - Chen Chen; Guangyu Hu; Cunxi Yu; Yuzhe Ma; Hongce Zhang (CoRR, 2025)

RTLCoder: Fully Open-Source and Efficient LLM-Assisted RTL Code Generation Technique. - Shang Liu 006; Wenji Fang; Yao Lu; Jing Wang 171; Qijun Zhang; Hongce Zhang; Zhiyao Xie (IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2025)

SMT-Sweep: Word-Level Representation Unification for Hardware Verification. - Ziyi Yang; Guangyu Hu; Mingkai Miao; Changyuan Yu; Hongce Zhang (CoRR, 2025)