Practical safety critical systems often uses both data and control intensive systems. Existing
formal verification approaches do not handle such systems very well. Formal verification approaches
can be divided into two categories of automata theoretic approaches and theorem proving based
approaches. Automata theoretic approaches considers the circuit as finite state machine and allow
completely automated verification procedures. The efficiency of these procedures has been enhanced
such that the systems with more than 2^(100) states can now be verified. However, it is
disappointing to see that this number of states is exceeded by simple circuits of just four 32$-bit
registers. This problem is known as state space explosion. This suggests that this approaches can
not be used for the verification of data-intensive applications, where state space is very large.
Theorem proving based approaches can be applied to verify such systems but they require a great
degree of manual intervention. |