An Interactive Verification and Debugging Environment by Concrete/Symbolic Simulations for System-Level Designs

This paper proposes a new approach for state space exploration on model checking of system-level designs, named "user-driven Breadth-First Search,\´\´ and an interactive verification and debugging environment for its realization. Our approach aims to overcome the limited width of the traditional concrete simulation (Depth-First Search) and the limited depth of symbolic simulation (Breadth-First Search), by combining both of them with the users\´ guidance. Our case study demonstrates that our approach can detect one of the bugs, which were difficult to be found due to too wide input space for concrete simulation, and due to too deep iteration cycles for symbolic simulation.