In recent years, circuit simulators and Boolean satisfiability (SAT) solvers have been tightly integrated to provide efficient logic synthesis and verification. Circuit simulation can generate highly expressive simulation patterns that can either enumerate or filter out most candidates for synthesis. Subsequently, SAT solvers are employed to check those that remain, thereby making the logic synthesis process more efficient. This paper introduces a novel circuit simulator of k-input lookup table (k-LUT) networks, based on semi-tensor product (STP). STP-based simulators use computation of logic matrices, the primitives of logic networks, as opposed to relying on bitwise logic operations for simulation of k-LUT networks. Experimental results show that our STP-based simulator reduces the runtime by an average of 7.2x. Furthermore, we integrate this proposed simulator into a SAT-sweeping engine known as SAT sweeper. Through a combination of structural hashing, simulation, and SAT queries, SAT sweeper simplifies logic networks by systematically merging graph vertices from input to output. To enhance the efficiency, we used STP-based exhaustive simulation, which significantly reduces the number of false equivalence class candidates, thereby improving the computational efficiency by reducing the number of SAT calls required. When compared to the SOTA SAT sweeper, our method demonstrates an average 35% runtime reduction.

翻译：近年来，电路仿真器与布尔可满足性（SAT）求解器紧密集成，以实现高效的逻辑综合与验证。电路仿真可生成高表达力的仿真模式，既能枚举也能过滤大部分综合候选方案，随后利用SAT求解器对剩余方案进行检查，从而使逻辑综合过程更加高效。本文提出了一种基于半张量积（STP）的新型k输入查找表（k-LUT）网络电路仿真器。与依赖位逻辑操作仿真k-LUT网络不同，STP仿真器利用逻辑矩阵（逻辑网络的原语）进行计算。实验结果表明，基于STP的仿真器平均运行时间减少了7.2倍。此外，我们将此仿真器集成到名为SAT sweeper的SAT-sweeping引擎中。通过结构哈希、仿真与SAT查询的组合，SAT sweeper从输入到输出系统性地合并图顶点，简化逻辑网络。为提升效率，我们采用基于STP的穷举仿真，显著减少了错误等价类候选的数量，从而通过减少所需SAT调用次数提高计算效率。与最先进的SAT sweeper相比，本方法平均运行时间减少35%。