| | GSRC Student Profile:
Research Overview: EQ-SHIVA: An SMT-Solver for Equivalency Checking
Further elevating the performance of functional verification, especially of equivalency checking, becomes necessary for addressing hardware systems’ increasing complexity.
In the past few years, SAT solvers have been the main engines for various formal verification tasks. In our research, we try to develop a new SMT-Solver customized with several novel methods that boosts the efficiency of equivalency checking, enabling it to make higher-level decisions and abstractions. including: (1) a new way to manipulate literals within the verification formulas, with which both Boolean and word-level literals can be classified into equality sets; (2) implementing an implicit implication graph for efficient use of memory; (3) combining two of the most powerful abstractions; and (4) embedding new heuristics so that human can better interact with the engine.
| |
