Reachability analysis of sequential circuits

摘要

Reachability analysis is a fundamental technique in the synthesis, 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. Compared with a previous work which relies on biased random technique, our approach reaches more states with less CPU time.