Technical Report No. 206 - Abstract

Marc Herbstritt, Thomas Kmieciak, Bernd Becker
Circuit Partitioning for SAT-based Combinational Circuit Verification --- A Case Study

Hardware verification is nowadays one of the most time-consuming tasks during chip design. In the last few years SAT-based methods have become a core technology in hardware design, especially for the verification of combinational parts of the circuits. Verifying the equivalence of some specification and a corresponding implementation is typically done by building a so-called miter. In practice this miter is often build for each pair of primary outputs or for all primary outputs at once. In this work we have a closer look on partitioning the primary outpouts of the circuit and how structural partitionings can speed-up the verification process when SAT-based methods are used.