Presentation
Parallel Combinational Equivalence Checking Through Factored Form Sharing
DescriptionCombinational equivalence checking (CEC) is a key and often time-critical step in the IC design flow for verifying functional equivalence after synthesis and technology mapping. As designs scale, improving CEC efficiency has become a major challenge with wide-ranging consequences for the entire flow. In this paper, we propose a novel parallel CEC approach through factored form sharing. In particular, the factored form literal count (FFLC) closely reflects both the amount of shareable literal/CNF-encoding and the branching complexity encountered during satisfiability (SAT)-based verification. Therefore, FFLC, together with a lightweight branching complexity proxy, guides a sharing-aware seed-and-grow partitioning algorithm that exploits literal and CNF-encoding reuse while balancing estimated SAT-solving complexity. Implemented in ABC and evaluated on large-scale benchmarks with 40 physical CPU cores, our implementation delivers geometric-mean speedups of 45.57× (max. 6,595×) over single-threaded ABC, 1.53× (max. 17×) over a state-of-the-art (SOTA) CPU-parallel method, and 5.52× (max. 382×) over a SOTA GPU-parallel method.
Event Type
Research Manuscript
TimeWednesday, July 2911:42am - 11:54am PDT
LocationMtg Room 202AB