A Comparison of SAT-based and SMT-based Frameworks for X-value Combinational Equivalence Checking

X-value combinational equivalence checking (XCEC) is a critical problem in verifying refinement-based logic optimizations and ensuring the correctness of low power design methodologies. The critical challenge in XCEC is to establish equivalence in a dramatically expanded search space. We can modify the traditional SAT-based Boolean combinational equivalence checking (CEC) methods to handle X-valued logic by adding an extra bit. However, the XCEC problem becomes more challenging when the two models are X-value equivalent because it involves considering the entire search space to prove the equivalence. Therefore, as an alternative, we propose to use SMT-based frameworks for XCEC by devising appropriate transformations. The proposed formulation allows the SMT solver to pre-process and simplify the encoded satisfiability problem internally. As a result, the SMT-based framework for XCEC is more efficient than a pure SAT-based XCEC, especially for cases in which the revised model is a valid refinement of the given golden model. We have used Cryptominisat5 to implement SAT-based XCEC and STP (with Cryptominisat5 as an internal SAT solver) to implement SMT-based XCEC. Using ICCAD 2020 benchmark suite, we demonstrate that, on an average SMT-based approach is 2.5 x faster than the SAT-based approach for X-value equivalent cases.