Abstract
The large number of latches in current designs increase the complexity of formal verification and logic synthesis. The reason for this is that the growth of latch number leads the state space to explode exponentially. One solution to this problem is to find the functional dependencies among these latches. With the identification of functional dependencies, these latches can be identified as dependent latches or essential latches, where the state space can be constructed using only the essential latches. Although much research has been devoted to exploring the functional dependencies among latches by BDD-based symbolic algorithms, this issue is still unresolved for large sequential circuits. In this work, we attempt to find the functional dependencies among latches in a sequential circuit by using SAT solvers with the Craig interpolation theorem. In addition, our proposed approach detects sequential functional dependencies existing in the reachable state space only. The sequential functional dependencies can identify additional dependent latches after a specific timeframe in order to achieve additional reduction of the state space. Experimental results show that this approach could deal with large sequential circuits with up to 1.5K latches in a reasonable time and simultaneously identify their combinational and sequential dependent latches. For instance, with s13207 in ISCAS’89, 23% of latches are identified as combinational dependent latches and an additional 13% of latches are identified as sequential dependent latches. For the reachability analysis of s13207, with the benefits of dependent latch identification, 70.70% of BDD size and 73.32% of CPU time can be reduced when reaching to the same timeframe. Furthermore, 2890.76% more states can be reached under 600, 000 run time limit.