SAT-based complete logic implication with application to logic optimization

Logic implication that finds necessary assignments for a given set of value assignments in a Boolean circuit has a wide set of applications in the computer-aided design field, such as logic optimization, design verification, and test pattern generation. Due to the high computational complexity, earlier methods either cannot or do not find all necessary assignments, limiting their qualities in the applications. With the dramatic advance of Boolean satisfiability (SAT) solving techniques, applying the efficient SAT solving techniques to logic implication seems promising. Thus, the paper presents a SAT-based method for complete logic implication. Given a set of value assignments, it first simulates a large number of random patterns and collects a set of candidate necessary assignments based on the simulation results. Then, instead of validating each candidate one by one, it iteratively calls a SAT solver to identify the invalid candidates and remove them. At each SAT solving iteration, at least one invalid candidate can be removed. Finally, only the valid candidates are left and they are exactly all the necessary assignments. Furthermore, we extend the method to compute all mandatory assignments for a stuck-at fault test and apply the extended method to enhance a logic optimization algorithm whose quality largely depends on the completeness of the mandatory assignment computation. The experimental results show that the enhanced method achieves an average of 1.3× improvement in circuit size reduction with acceptable CPU time overhead.