1 citations · 2 across the 15 of their papers we have counts for
9 papers · 1 filter
NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng +5
Formal verification is a crucial technique for ensuring the functional correctness of hardware designs. In the context of property checking, a key challenge is how to efficiently p…
Forbench: Symbolic Simulation Helps Make Your Testbench More Formal
Ziyi Yang, Wenbin Che, Ziyue Zheng +2
Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of…
Inverter Redistribution through Self-Dual and Self-Anti-Dual Function Transformation
Jingren Wang, Guangyu Hu, Shiju Lin +1
And-Inverter Graph (AIG)-based logic synthesis has been a cornerstone of digital design automation for several decades. While numerous optimization techniques have been developed f…
AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
Xiaofeng Zhou, Linfeng Du, Guangyu Hu +3
High-level synthesis (HLS) transforms an algorithmic description of hardware from a higher abstraction (e.g., C/C++) into a register-transfer level (RTL) design, offering reduced d…
A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
Xiaofeng Zhou, Guangyu Hu, Hongce Zhang +1
The IC3 algorithm represents the state-of-the-art (SOTA) hardware model checking technique, owing to its robust performance and scalability. A significant body of research has focu…
IC3-Evolve: Proof-/Witness-Gated Offline LLM-Driven Heuristic Evolution for IC3 Hardware Model Checking
Mingkai Miao, Guangyu Hu, Ziyi Yang +1
IC3, also known as property-directed reachability (PDR), is a commonly-used algorithm for hardware safety model checking. It checks if a state transition system complies with a giv…
AutoPDR: Circuit-Aware Solver Configuration Prediction for Hardware Model Checking
Guangyu Hu, Chen Chen, Xiaofeng Zhou +3
Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configur…
LeGend: A Data-Driven Framework for Lemma Generation in Hardware Model Checking
Mingkai Miao, Guangyu Hu, Wei Zhang +1
Property checking of RTL designs is a central task in formal verification. Among available engines, IC3/PDR is a widely used backbone whose performance critically depends on induct…
EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Guangyu Hu, Xiaofeng Zhou, Wei Zhang +1
Progress in hardware model checking depends critically on high-quality benchmarks. However, the community faces a significant benchmark gap: existing suites are limited in number,…