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 given safety property. IC3 either returns UNSAFE (indicating property …
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 focused on enhancing the solving efficiency of the IC3 algorithm, with …
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 inductive generalization, the step that generalizes a concrete …
Property Directed Reachability (PDR) is a powerful algorithm for formal verification of hardware and software systems, but its performance is highly sensitive to parameter configurations. Manual parameter tuning is time-consuming and requires domain …
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, often distributed only in representations such as BTOR2 without access …
In recent years, machine learning has demonstrated its potential in many challenging problems. In this paper, we extend its use to hardware formal property verification and propose DeepIC3, a method that takes advantage of graph learning in the …
The property-directed reachability (PDR) algorithm has been one of the most successful hardware model checking algorithms powering modern formal property verification tools. Inductive generalization is the key to the efficiency of the PDR algorithm. …