摘要
可達性分析對於超大型積體電路的合成和驗證而言是一項基礎且十份重要的技術。本篇論文提出一個創新且半正規的方法來走訪有限狀態機中的狀態，而這個方法同時結合了模擬和正規方法的優點。我們使用一系列ISCAS''''89的測資來進行實驗，並且與一個以偏移亂數方式為基礎的研究方法做比較，而實驗結果指出我們的方法的確能較有效率地得到更多的狀態數。
關鍵字
可達性並列摘要
Reachability analysis is a fundamental technique in the Synthesis and verification of VLSI circuits. This paper presents a novel semi-formal approach which combines the advantages of simulation and formal methods to traverse the state space of the FSMs. We conduct the experiments on a set of ISCAS’89 benchmarks. As compared with a previous work which relies on biased random technique, our approach reaches more states with less CPU time.
並列關鍵字
reachability參考文獻
[2] J. R. Burch, E. M. Clarke, and D. E. Long“Representing circuits more efficiently in symbolic model checking,” in Proc. 28th Design Automation Conf., pp. 403-407, 1991.
[3] J. R. Burch, E. M. Clarke, and D. E. Long, “Symbolic model checking with partitioned transition relations,” in Proc. Int. Conf. Very Large Scale Integration, pp. 49-58,
[4] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential circuit verification using symbolic model checking,” in Proc. 27th Design Automation Conf.,
pp. 46-51, 1990.
[5] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, “Symbolic model checking: 10^20 states and beyond,” in Proc. Fifth Ann. IEEE Symp. Logic in Computer Sci., pp. 428-439, 1990.