5 papers
Enhancing Word-Level Property Directed Reachability with LLM-Driven Semantic Guidance
Guangyu Hu, Mingkai Miao, Zhiyuan Yan +3
Property Directed Reachability (PDR) is a prominent algorithm for hardware formal verification. However, bit-level PDR often struggles with datapath-heavy designs because bit-blast…
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…
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…
BDD2Seq: Enabling Scalable Reversible-Circuit Synthesis via Graph-to-Sequence Learning
Mingkai Miao, Jianheng Tang, Guangyu Hu +1
Binary Decision Diagrams (BDDs) are instrumental in many electronic design automation (EDA) tasks thanks to their compact representation of Boolean functions. In BDD-based reversib…
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…