Boolean matching, a fundamental problem in circuit design, determines whether two Boolean circuits are equivalent under input/output permutations and negations. While most works focus on finding a single match or proving its absence, the problem of enumerating all matches remains largely unexplored, with BooM being a notable exception. Motivated by timing challenges in Intel’s library mapping flow, we introduce EBat - an open-source tool for enumerating all matches between single-output circuits. Built from scratch, EBat reuses BooM’s SAT encoding and introduces novel high-level algorithms and performance-critical subroutines to efficiently identify and block multiple mismatches and matches simultaneously. Experiments demonstrate that EBat substantially outperforms BooM’s baseline algorithm, solving 3 to 4 times more benchmarks within a given time limit. EBat has been productized as part of Intel’s library mapping flow, effectively addressing the timing challenges.

Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.

Motivated by the need to improve the scalability of Intel’s in-house Static Timing Analysis (STA) tool, we consider the problem of enumerating all the solutions of a single-output combinational Boolean circuit, called AllSAT-CT. While AllSAT-CT is immediately reducible to enumerating the solutions of a Boolean formula in Conjunctive Normal Form (AllSAT-CNF), our experiments had shown that such a reduction, followed by applying state-of-the-art AllSAT-CNF tools, does not scale well on neither our industrial AllSAT-CT instances nor generic circuits, both when the user requires the solutions to be disjoint or when they can be non-disjoint. We focused on understanding the reasons for this phenomenon for the well-known iterative blocking family of AllSAT-CNF algorithms. We realized that existing blocking AllSAT-CNF algorithms fail to generalize efficiently for AllSAT-CT, since they are restricted to Boolean logic. Consequently, we introduce three dedicated AllSAT-CT algorithms that are ternary-logic-aware: a ternary simulation-based algorithm TALE, a dual-rail&MaxSAT-based algorithm MARS, and their combination. Specifically, we introduce in MARS two novel blocking clause generation approaches for the disjoint and non-disjoint cases. We implemented our algorithms in our new tool HALL. We show that HALL scales substantially better than any reduction to existing AllSAT-CNF tools on our industrial STA instances as well as on publicly available families of combinational circuits for both the disjoint and the non-disjoint cases.