5 papers
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…
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…
FPPS: An FPGA-Based Point Cloud Processing System
Xiaofeng Zhou, Linfeng Du, Hanwei Fan +1
Point cloud processing is a computational bottleneck in autonomous driving systems, especially for real-time applications, while energy efficiency remains a critical system constra…
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,…
FORWORD: Accelerating Formal Datapath Verification via Word-Level Sweeping
Ziyi Yang, Guangyu Hu, Xiaofeng Zhou +4
Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high…