Abstract
With the growth of design complexity, verification has become one of the primary bottlenecks of the design process. Studies show that verification could take 40% to 70% of the total development effort for the design. As a result, reducing verification time directly affects the design cycle. In this dissertation, we propose three logic optimization methods to facilitate verification process. We first focus on simulation-based functional verification. A range-equivalent circuit optimization method is proposed to minimize a constraint circuit that is responsible for generating legal input patterns for a design under verification. This method could minimize a constraint circuit while preserving its range such that the pattern generation process could be accelerated and the patterns remain legal. The experimental results show that the proposed method can minimize a benchmark with an average of 37.06% reduction in terms of the number of primary inputs, and an average of 36.31% reduction in terms of the number of nodes. Additionally, each simplified benchmark can generate more output combinations than the non-simplified one for the same random simulation time. Next, we focus on satisfiability (SAT)-based equivalence checking. A node-merging method is proposed to merge two nodes (use one node replace another node) in a circuit which are functional equivalent or their functional differences are never observed at any primary output. When two nodes are merged, one of them can be removed from the circuit, and this merger may cause other redundancies in the circuit such that the resultant circuit is minimized. The experimental results show that the proposed method is 46 times faster than a previous method and has a competitive capability of circuit size reduction. Furthermore, a node addition and removal (NAR) method is proposed to enhance the node-merging method. It creates a node merger by adding a node into the circuit. When more than one node is removed due to the addition of the new node, the circuit size is reduced as well. The experimental results show that the optimization capability of the NAR method is better than that of the proposed node-merging method with a ratio of 1.27. The overall CPU time overhead is only 242.8 seconds. We further apply these two methods to facilitate bounded sequential equivalence checking. A total of approximately 27-hour verification time is saved for all the benchmarks.