1

NeuroAbs: LLM-Guided Neuro-Symbolic RTL Abstraction for Property Checking Acceleration
RTL Abstraction, Property Checking, Neuro-Symbolic Methods
Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang
Cite
Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement
RTL Assertion Generation, Formal Exploration, Neuro-Symbolic Refinement
Zhiyuan Yan, Ziyue Zheng, Hongce Zhang
Cite
Hot-FV: A Semi-Formal Test Generation Framework for RTL Functional Coverage using Warm Starting States
Hardware Model Checking, Counterexample Reduction, Counterexample Reduction Applications
Ziyue Zheng, Zhiyuan Yan, Xiangchen Meng, Guangyu Hu, Hongce Zhang, Yangdi Lyu
Cite
Word-Level Counterexample Reduction Methods for Hardware Verification
Hardware Model Checking, Counterexample Reduction, Counterexample Reduction Applications
Zhiyuan Yan, Hongce Zhang
Cite
AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs
Assertion-based verification (ABV) is a critical method to ensure logic designs comply with their architectural specifications. ABV …
Zhiyuan Yan, Wenji Fang, Mengming Li, Min Li, Shang Liu, Zhiyao Xie, Hongce Zhang
Cite
Word-Level Augmentation of Formal Proof by Learning from Simulation Traces
Hardware Model Checking, Property Augmentation, Machine Learning
Zhiyuan Yan, Hongce Zhang
Cite
AsymSAT: Accelerating SAT Solving with Asymmetric Graph-based Model Prediction
Boolean Satisfiability Problem, Machine Learning
Zhiyuan Yan, Min Li, Zhengyuan Shi, Wenjie Zhang, Ying-Cong Chen, Hongce Zhang
PDF Cite Poster