الفهرس 
Symbolic Execution
Automatic Test Cases Generation on Virtual Models using Symbolic ExecutionOnly 14 pages are availabe for public view
 |  | from | 110 |  |  |
| | | from | 110 | | |
Abstract
Embedded systems, like smart phones, laptops, servers, etc. are intruding the market with high acceleration. Many studies have proven that up to 70% of the development cycle is spent in the verification. A significant stage in the development cycle of the embedded system is the validation of the hardware models. The goal of this work is to shorten the hardware validation stage time. Our approach is to get the related test cases ready before the hardware exists. It mainly depends on deploying a formal methodology on the virtual hardware model for an Automatic Test Pattern Generation. The first phase in our approach involves the creation of harness based on constraints extracted from the specification. The main goal of the harness is to tackle the challenges of deploying formal methodology to generate high functional coverage test cases. The second phase involves the replay of the test cases to provide an early evaluation of the test coverage before the RTL exists. For this purpose, we developed a semi-automated methodology to compute and report the test coverage. Therefore, when the hardware is ready, these test cases can be directly deployed for coverage verification. We have applied our approach on a QEMU Direct Memory Access controller to evaluate the test coverage for the generated test suite. Furthermore, we have applied the test suite on the corresponding Register Transfer Level model. The results demonstrate that our test suite is able to meet the coverage goal on the register transfer level using Universal Verification Methodology test environment.