Achieving timing-closure has become one of the hardest tasks in logic synthesis due to the required stringent timing constraints in very large circuit designs. In this paper, we propose a novel synthesis paradigm to achieve timing-closure called Timing-Aware CUt Enumeration (TACUE). In TACUE, optimization is conducted through three aspects: (1) a new divide-and-conquer strategy is proposed that generates multiple sub-cuts on the critical parts of the circuit; (2) two cut enumeration strategies are proposed; (3) an efficient parallel synthesis framework is offered to reduce computation time. Experiments on large and difficult industrial benchmarks show the promise of the proposed method.

Currently, BDD packages such as CUDD depend on chained hash tables. Although they are efficient in terms of memory usage, they exhibit poor cache performance due to dynamic allocation and indirections of data. Moreover, they are less appealing for concurrent environments as they need thread-safe garbage collectors. Furthermore, to take advantage of the benefits from multi-core platforms, it is best to re-engineer the underlying algorithms, such as whether traditional depth-first search (DFS) construction, breadth-first search (BFS) construction, or a hybrid BFS with DFS would be best. In this paper, we introduce a novel BDD package friendly to multicore platforms that builds on a number of heuristics. Firstly, we re-structure the Unique Table (UT) using a concurrency-friendly Hopscotch hashing to improve caching performance. Secondly, we re-engineer the BFS Queues with hopscotch hashing. Thirdly, we propose a novel technique to utilize BFS Queues to simultaneously work as a Computed Table (CT). Finally, we propose a novel incremental Mark-Sweep Garbage Collector (GC). We report results for both BFS and hybrid BFS-DFS construction methods. With these techniques, even with a single-threaded BDD, we were able to achieve a speedup of up to 8× compared to a conventional single-threaded CUDD package. When two-threads are launched, another 1.5× speedup is obtained.

The effectiveness of Satisfiability (SAT)-based Bounded Model Checking (BMC) critically relies on the deductive power of the BMC instance. Although implication relationships have been used to help SAT solver to make more deductions, too many such implications would result in a large number of clauses and potentially degrade the underlying SAT solver performance. In this paper, we have formulated clause selection as a set-cover problem. Secondly, we have proposed a novel greedy strategy for optimal selection of static logic clauses. This technique maximizes the number of literals that can be deduced by the SAT solver during the Boolean Constraint Propagation (BCP) operation. Our strategy improves BMC by 1.74x against the case where all extended implications were added to the BMC instance. Compared with the original BMC without any implications, up to 55.32x speedup can be achieved.

The effectiveness of SAT-based Bounded Model Checking (BMC) critically relies on the deductive power of the BMC instance. Although implication relationships have been used to help SAT solver to make more deductions, frequently an excessive number of implications has been used. Too many such implications can result in a large number of clauses that could potentially degrade the underlying SAT solver performance. In this paper, we first propose a framework for a parallel deduction engine to reduce implication learning time. Secondly, we propose a novel set-cover technique for optimal selection of constraint clauses. This technique depends on maximizing the number of literals that can be deduced by the SAT solver during the BCP (Boolean Constraint Propagation) operation. Our parallel deduction engine can achieve a 5.7× speedup on a 36-core machine. In addition, by selecting only those critical implications, our strategy improves BMC by another 1.74× against the case where all extended implications were added to the BMC instance. Compared with the original BMC without any implication clauses, up to 55.32× speedup can be achieved.