Efficient (Non-)Reachability Analysis of Counterexamples.
Rolf Drechsler, Wolfgang Günther, Burkhard Stubert · 2004
Formal verification of complete ASICs with up to several million gates can only be carried out, if the sequential problem is transformed to a combinational one. The circuits that have to be compared are modeled as Finite State Machines (FSMs). But the state encoding has to be (nearly) identical such that a matching of the states can be performed. Then combinational equivalence checking is carried out on the resulting design. If the designs are not equivalent, a counterexample consisting of values for some inputs and registers is returned. The remaining problem is to decide whether this counterexample is (sequentially) reachable, i.e. whether the state s specified in the counterexample is valid.