Automatic test pattern generation for virtual hardware model using constrained symbolic execution

Symbolic execution is widely used for analyzing software behavior, generating test pattern, and finding bugs. However, it is not feasible for large programs. Symbolic execution attempts to explore each path of the program which result in a path explosion for large programs. This paper introduces a framework that makes the symbolic execution practical for the virtual HW models that run on QEMU platform. We describe an approach that can symbolically execute a virtual HW model to automatically generate selective test patterns. We use the constraints-based technique in order to show preferences for the generated test pattern. A native symbolic run of the program along with the constraints will generate test patterns correspond to every possible path. Our technique adds assertion statement into the program to indicate a specific operation mode for the device that the developer pay attention on. The symbolic engine generates test patterns that can derive the program through all feasible paths to reach the assertion. These test patterns can be used to verify same operation mode on the associated HW RTL model.