Majority-Inverter Graph (MIG) emerges as a promising data structure for logic optimization and synthesis, offering a more compact representation for logic functions compared to traditional AND/OR-Inverter graphs. Consequently, the MIG finds …
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 …
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 …
Binary Decision Diagrams (BDDs) are instrumental in many electronic design automation (EDA) tasks thanks to their compact representation of Boolean functions. In BDD-based reversible-circuit synthesis, which is critical for quantum computing, the …
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 technology mapping, the quality of the final implementation heavily relies on the circuit structure after technology-independent optimization. Recent studies have introduced equality saturation as a novel optimization approach. However, its …
Logic synthesis plays a crucial role in the digital design flow. It has a decisive influence on the final Quality of Results (QoR) of the circuit implementations. However, existing multi-level logic optimization algorithms often employ greedy …
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. …