Compatible Equivalence Checking of X-valued Circuits
- Duration: July 2020 – July 2021.
- The project originated from the problem A of the ICCAD 2020 CAD Contest.
- The goal of the contest is to verify the combinational equivalence of 2 x-valued (or ternary logic) netlists, with the X-values serving as dont cares.
- Ternary logic, consisting of 0, 1 and X, arises in various contexts of system design, where the X-value often represents an unknown value or a don’t-care value depending on the application.
- We construct the circuits with X-value preserved dual-rail encoding, and apply various optimization techniques.
- We identify the compatible equivalence relations of internal signals, and utilize such information to guide the SAT oracle for more efficient solving.
- Experiments on industrial designs have demonstrated the superiority of our method to other competitive methods.
- The research work was presented in the IWLS 2021. Click the links to view the paper [PDF] and the presentation [slides | video].
- The research paper is accepted by the ICCAD 2021.
