Ming-Kai Miao

Enhancing Word-Level Property Directed Reachability with LLM-Driven Semantic Guidance

Property Directed Reachability (PDR) is a prominent algorithm for hardware formal verification. However, bit-level PDR often struggles with datapath-heavy designs because bit-blasting obscures high-level semantics. While word-level PDR addresses this by reasoning over bit-vector and array theories, its performance rema...