大量的正反器存在目前的設計會增加正規驗證和邏輯合成的複雜度。
主要的原因是隨著正反器數目的增加會使得狀態空間成指數性的成長。其中一種解決方法是找出正反器間的相依性。
如果知道正反器間的相依性，這些正反器就可以被分類成相依正反器和必要正反器這兩類，而且真正的狀態空間則由必要正反器所構成。
雖然有很多研究使用以BDD為基礎的象徵演算法去找尋這些正反器間的相依性，但是仍然無法有效的處理大型的循序電路。在這篇論文裡，我們使用SAT方法及Craig內插定理去尋找正反器間的相依性。
此外，我們所提出的方法還可以偵測出只存在可達狀態空間的循序相依性。經由循序相依性，我們可以偵測出額外的相依正反器存在於某個特定的時間框架之後，並且可以利用它們來達到額外的狀態空間減少。實驗結果顯示，這種方法可以在合理的時間內處理擁有一千五百以上個正反器的大型循序電路，並且找出它們組合及循序的相依正反器。例如，針對iscas'89測資裡的s13207，23%的正反器是組合相依正反器及額外的13%正反器是循序相依正反器。經由這些相依正反器的偵測，對s13207作可達性分析時，可以減少70.70%的BDD大小和73.32%的執行時間去達到相同的時間框架。除此之外，在600000秒的執行時間限制下，2890.76%的狀態空間也就是更多的狀態空間可以被達到。

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.

[1] F. A. Aloul, I. L. Markov, and K. A. Sakallah, “Faster SAT and Smaller BDDs
via Common Function Structure,” Technical Report, University Michigan, 12,
Dec. 2001.
[2] R. Bryant, “Graph-based Algorithms for Boolean Function Manipulation,”
IEEE Trans. Computers, vol. 35, pp. 677-691, August 1986.
[3] R. K. Brayton et al, “VIS: A System for Verification and Synthesis,” in
Proc. Computer Aided Verification Conf., pp. 423-427, 1996.
[4] D. Brand, “Verification of Large Synthesized Designs,” in
Proc. Int. Conf. Computer-Aided Design, pp. 534-537, 1993.
[5] J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, “Symbolic
Model Checking for Sequential Circuit Verification,” in IEEE Transactions
on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, no. 4,
pp. 401-424, April 1994.
[6] W. Craig, “Linear Reasoning: A New Form of the Herbrand-Gentzen Theorem,”
J. Symbolic Logic, 22(3):250-268, 1957.
[7] H. Cho, G. D. Hatchel, E. Macii, B. Plessier, and F. Somenzi, “Algorithms
for Approximate FSM Traversal Based on State Space Decomposition,” in
Proc. Design Automation Conf., pp. 25-30, 1993.
[8] N. E´en and N. S¨orensson, “An Extensible SAT-solver,” in Proc. Int. Conf. on
Theory and Applications of Satisfiability Testing, pp. 502-518, 2003.
[9] S. G. Govindaraju, D. L. Dill, A. Hu, and M. A. Horowitz, “Approximate
Reachability Analysis with BDDs Using Overlapping Projections,F in
Proc. Design Automation Conf., pp. 451-456 , 1998.
[10] A.-J. Hu and D. L. Dill, “Reducing BDD Size by Exploiting Functional Dependencies,”
in Proc. Design Automation Conf., pp. 266-271, 1993.
[11] S.-Y. Huang, K.-T. Cheng, and K.-C. Chen, “AQUILA: An Equivalence Verifier
for Large Sequential Circuits,” in Proc. Asian South Pacific Design Automation
Conf., pp. 455-460, 1997.
[12] R. Hojati, S. Krishnan, and R. K. Brayton. “Heuristic Algorithms for
Early Quantification and Partial Product Minimization,” in Technical Report
M94/11, UC Berkeley, 1994.
[13] J.-H. R. Jiang and R. K. Brayton, “Functional Dependency for Verification
Reduction,” in Proc. Computer Aided Verification Conf., pp. 268-280, 2004.
[14] J. Krajicek, “Interpolation Theorems, Lower Bounds for Proof Systems, and
Independence Results for Bounded Arithmetic,” J. Symbolic Logic, 62(2):457-
486, June 1997.
[15] C.-C. Lee, J.-H. R. Jiang, C.-Y. Huang, and A. Mishchenko. “Scalable Exploration
of Functional Dependency by Interpolation and Incremental SAT Solving,”
in Proc. Int. Conf. Computer-Aided Design, pp. 227-233, 2007.
[16] B. Lin and A. R. Newton, “Exact Redundant State Registers Removal Based on
Binary Decision Diagrams,” in Proc. Int. Conf. on Very Large Scale Integration,
pp. 277-286, 1991.
[17] M. Moskewicz, C. Madigan, L. Zhang, and S. Malik, “Chaff: Engineering an
Efficient SAT Solver,” in Proc. Design Automation Conf., pp. 530-535, 2001.
[18] K. L. McMillan, “Interpolation and SAT-based Model Checking,” in Proc. Computer
Aided Verification Conf., pp. 1-13, 2003.
[19] K. L. McMillan, “Symbolic Model Checking,” Kluwer Academic Publishers,
Norwell, MA, 1993.
[20] I.-H. Moon, J. Kukula, T. Shiple, and F. Somenzi, “Least Fixpoint Approximations
for Reachability Analysis,” in Proc. Int. Conf. Computer-Aided Design,
pp. 41-49, 1999.
[21] P. Pudlak, “Lower Bounds for Resolution and Cutting Plane Proofs and Monotone
Computations,” J. Symbolic Logic, 62(3):981-998, Sep. 1997.
[22] E. M. Sentovich, K. J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha,
H. Savoj, P. R. Stephan, R. K. Brayton, and A. Sangiovanni-Vincentelli, “SIS: A
System for Sequential Circuit Synthesis,” Technical Report UCB/ERL M92/41,
Electronics Research Lab, Univ. of California, Berkeley, CA 94720, May 1992.
[23] C. A. J. van Eijk and J. A. G. Jess, “Exploiting Functional Dependencies in
Finite State Machine Verification,” in Proc. European Design & Test Conf.,
pp. 9-14, 1996.
[24] J. Whittemore, J. Kim, and K. Sakallah, “SATIRE: A New Incremental Satisfiability
Engine,” in Proc. Design Automation Conf., pp. 542-545, 2001.