Formal verification of heavily optimized multipliers is a critical yet challenging problem in both industry and academia. Current approaches suffer from fundamental limitations: Symbolic Computer Algebra (SCA) techniques struggle with heavily optimized multipliers, Satisfiability (SAT)-based approaches require structurally similar reference designs, and hybrid methods fail to handle Booth multipliers. On the other hand, industrial design flows possess extensive libraries of verified multipliers for optimization workflows, creating an underutilized opportunity for library-based verification. Yet optimal reference selection becomes challenging due to large-scale libraries and optimization-obscured architectural relationships. To address these challenges, we propose LibSCAT, a verification framework that leverages large-scale reference libraries in a scalable manner. First, we propose a reference library-based methodology that adaptively combines SCA and SAT techniques through intelligent reference selection and predictive method choice. Second, we propose a Siamese Graph Neural Network model that captures multiplier structural relationships in latent space from reverse-engineered graphs, generating robust embeddings for efficient reference selection. Third, we propose a Random Forest-based predictor that leverages learned embeddings for accurate selection of verification strategies. Experimental results show our method achieves 88.2% success on heavily optimized simple partial product multipliers and 94.0% success on heavily optimized Booth multipliers, significantly outperforming state-of-the-art methods.

Equality graphs (E-graphs) offer a compact representation for vast sets of equivalent implementations, proving invaluable in hardware synthesis and program optimization. Nevertheless, extracting the optimal implementation from an e-graph constitutes an NP-hard challenge. Current extraction methods face critical limitations: heuristic-based approaches fail to produce high-quality solutions, GPU-accelerated techniques lack determinism and demand excessive memory, exact ILP methods struggle with scalability, and specialized solvers only function for particular e-graph types. To address this, we present ESACO, a novel deterministic framework that rapidly and consistently converges to high-quality solutions across diverse benchmarks by effectively combining Simulated Annealing (SA) for local refinement with Ant Colony Optimization (ACO) for global search. First, we develop a synergistic hybrid-heuristic framework that orchestrates complementary search paradigms, harmonizing ACO’s global exploration capabilities with SA’s targeted local exploitation mechanisms. Second, we introduce an SA-based local search method that employs novel rip-up and repair moves for efficiently refining promising solutions. Third, we propose an ACO-based global search algorithm incorporating strategic restart mechanisms to effectively explore the complex solution space while escaping local optima. Experimental results demonstrate that ESACO achieves up to 42× speedup using a single thread compared to state-of-the-art GPU-accelerated methods while maintaining or improving solution quality.

Formally verifying logic-optimized integer multipliers remains a crucial yet insufficiently addressed problem in both industry and academia, presenting significant verification challenges, particularly when verifying the large-scale logic-optimized multipliers with diverse architectures. Satisfiability (SAT)-based methods require structurally similar and known correct reference multipliers, which may not always be readily accessible. Symbolic computer algebra (SCA) techniques can verify multipliers without references but encounter difficulties with optimized multipliers due to unclear adder boundaries. To enable effective formal verification of the optimized multipliers, we propose the RefSCAT framework, which contains a reference multiplier generator that produces references structurally similar to the optimized multiplier with clear adder boundaries, enabling a synergistic SCA-SAT verification flow. First, we propose a reverse engineering algorithm that extracts the essential adder tree from the optimized multiplier, ensuring similarity. Second, since only a partial netlist is extractable after optimization, we propose a constraint satisfaction algorithm to complete the generation using only adders while following the extracted netlist, ensuring both similarity and clear adder boundaries. Third, leveraging the generated reference, we propose a synergized SCA-SAT verification flow that verifies the generated reference using SCA and then uses it as a correct reference for the SAT-based verification. The experiments demonstrate that RefSCAT can successfully verify logic-optimized multipliers with diverse partial-product-based architectures up to 128 bits, outperforming the state-of-the-art methods by verifying at least 29% more benchmarks.

Formal verification of large-scale optimized integer multipliers remains a critical yet insufficiently addressed challenge in industry and academia. Current methods employ reference multiplier generators to automatically construct structurally similar reference multipliers, which are then used by Satisfiability (SAT)-based techniques to verify equivalence with optimized multipliers. However, these approaches face limitations when generating references for large-scale optimized multipliers within acceptable timeframes. To address these limitations, we introduce the RefSCAT-2.0 framework, designed to rapidly produce high-quality large-scale reference multipliers. Firstly, we generate the macro-architecture to determine the number of adders required for constructing the reference multiplier. We propose a novel Integer Linear Programming (ILP)-based macro-architecture generation algorithm that minimizes the number of allocated adders, thereby reducing the overall problem complexity. Secondly, we organize the allocated adders into groups to simplify the subsequent generation process. We present a multi-level scheduler that automatically decomposes adders into groups with minimized interdependencies, ensuring both the quality of generation and a reduction in overall generation complexity. Thirdly, we generate the micro-architecture for each scheduled group, wherein we finalize the connections between adders. We present a graph-based design space representation coupled with a quantum-inspired ant colony optimization (QACO)-based generation algorithm that can efficiently explores the micro-architectures of each scheduled group. Experimental results show that RefSCAT-2.0 successfully verifies all 124 cases in a 256-bit optimized multiplier benchmark suite, outperforming SCA-based tcad22revsca and hybrid RefSCATTCAD24 methods which solve only 24 cases each.

Logic rewriting is an effective but time-consuming technique to optimize the multilevel logic network by rewriting subnetworks of the input network with other logic equivalent structures. However, contemporary multithread rewriting algorithms either fail to parallelize the subprocedures of rewriting for individual nodes (intranode parallelism) or require locks to ensure the mutual exclusive among the scheduled nodes that are rewritten concurrently (internode parallelism), hence inevitably decreasing the degrees of parallelism and the scalability. This article proposes a novel GPU-based logic rewriting acceleration framework to address the mentioned issues in two phases. First, to exploit the intranode parallelism, we propose recursion-free algorithms that parallelize subprocedures of rewriting, which was hard to achieve due to the highly recursive nature of original rewriting algorithms. Second, to exploit the internode parallelism, we propose a work scheduler that can schedule mutually exclusive nodes and a GPU-friendly data structure that can support efficient concurrent operations. The new work scheduler and data structure allow simultaneously processing plenty of nodes without using locks. Experimental results show that our method can achieve on average$3.81\times $speedup, compared to the state-of-the-art GPU-parallel method with the same quality of results.

Memory scrubbing is a resource-efficient technique to ensure the high reliability of SRAM-based FPGAs by refreshing the configuration memory just before its execution. To maximize reliability, a scrubbing scheduling algorithm is expected to scrub as many tasks as possible. Unfortunately, contemporary scheduling algorithms either suboptimally handle scrubbing conflicts under bursty requests from multiple user tasks or discriminate against low-criticality tasks by giving them very low scrubbing opportunities. Besides, exploring the architectural support for scrubbing problems may bring considerable potential for reliability improvements. However, this direction of scheduling-architecture co-optimization has not been well studied so far. In this article, we propose a negotiation-based dynamic scrubbing framework, which addresses the above-mentioned issues in three phases: 1) we propose a negotiation-driven scrubbing scheduling algorithm, which temporarily allows and iteratively reduces the conflicts of scrubbing tasks in order to accommodate more scrubbing tasks to be scheduled; 2) we develop a logistic probability model to prevent scheduling starvation of a set of mix-criticality tasks by dynamically legalizing conflicting ones, considering both the criticality and schedulability of each task; and 3) we develop a dynamic voltage/frequency scaling-based multi-ICAPs allocation algorithm to co-optimize with FPGA architectural features for reliability maximization. Compared to the state-of-the-art, experimental results show that our work achieves up to 31.46% improvement in terms of reliability for contemporary SRAM-based FPGAs.