Semi-formal verification of memory systems by symbolic simulation

We propose a debugging method for data-path intensive systems, in particular, memory systems. The approach is based on strengthening invariants by deriving constraints on data in the design using symbolic simulation with constrained inputs. A new heuristic is introduced for finding the appropriate input constraints for the symbolic simulation. We give up soundness in order to gain more automation and efficiency, minimizing or even eliminating the required manual effort. While it is no longer possible to prove the correctness of the design, experimental results demonstrate that the technique is quite effective in finding design errors.