Abstract
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.