Formal Verification

Formal verification consists in determining whether or not a circuit satisfies its specification. The specification can be some formalism that clearly and unambiguously describes the circuit behavior, whereas the circuit description usually characterizes the circuit at a lower level, e.g. a netlist of gates. Formal verification must assure that in any reachable circuit state the specification is not violated. Asynchronous circuits may have a huge number of reachable states, thus the problem of formal verification has been faced by using symbolic encoding and manipulation techniques. In addition, by using hierarchical approaches verification can be made even more efficiently.