Symbolic Simulation Based Verification for Data and Control Intensive Systems
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.
Symbolic simulation, is known to be effective to verify such systems. Towards this direction we are developing a tool to enable the user to symbolically simulate such systems efficiently.