Simulation remains the dominant approach in pre-silicon verification due to its ease of deployment and intuitive workflow. However, as simulation only explores a limited subset of possible execution traces within feasible time budgets, it often fails …
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 …
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 development time and greater flexibility in design space exploration. …
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 …
Modern circuit design process increasingly adopts high-level hardware construction languages and parameterized design methodologies to shorten development cycles and maintain high reusability, in contrast to traditional hardware description …
Functional verification is critical in ensuring the correctness of register transfer level (RTL) models. Formal methods, such as model checkers, are powerful tools that help achieve high coverage in functional validation by transforming the coverage …
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. …