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…
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,…
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…