2507.02008

Total: 1

#1 SMT-Sweep: Word-Level Representation Unification for Hardware Verification [PDF] [Copy] [Kimi] [REL]

Authors: Ziyi Yang, Guangyu Hu, Mingkai Miao, Changyuan Yu, Hongce Zhang

SAT sweeping has long been a cornerstone technique in logic simplification and equivalence checking at the bit level, leveraging structural hashing, simulation and SAT solving to prune redundant logic. However, with the growing adoption of word-level constructs in hardware verification, such as bit-vector operations, arithmetics and arrays, there lacks a counterpart of SAT sweeping at the word level. In this paper, we introduce SMT-Sweep, a novel extension of SAT sweeping into the word level, grounded in Satisfiability Modulo Theories (SMT). SMT-Sweep takes advantage of simulation and equivalence detection to handle SMT terms with rich bit-vector operations and array semantics. Our framework incorporates both randomized and constraint-driven word-level simulation tailored to symbolic expressions and operator semantics beyond pure Boolean logic. Experimental results show that SMT-Sweep achieves significant speed-up compared to state-of-the-art bit-level SAT sweeping and word-level monolithic SMT solving (averaging around 44x and 69x, respectively).To the best of our knowledge, this is the first work that brings sweeping techniques to SMT-based hardware verification. The implementation is open-sourced at: https://github.com/yangziyiiii/SMT-Sweep.

Subject: Logic in Computer Science

Publish: 2025-07-02 03:34:36 UTC