This thesis presents a novel concolic testing methodology and CORT, a test generation framework that uses it for high-level functional test generation. The test generation effort is visualized as the systematic unraveling of the control-flow response of the design over multiple (factored) explorations. We begin by transforming the Register Transfer Level (RTL) source for the design into a high-performance C++ compiled functional simulator which is instrumented for branch coverage. An exploration begins by simulating the design with concrete stimuli. Then, we perform an interleaved cycle-by-cycle symbolic evaluation over the concrete execution trace extracted from the Control Flow Graph (CFG) of the design. The purpose of this task is to dynamically discover means to divert the control flow of the system, by mutating primary-input stimulated control statements in this trace. We record the control-flow response as a Test Decision Tree (TDT), a new representation for the test generation effort. Successive explorations begin at system states heuristically selected from a global TDT, onto which each new decision tree resultant from an exploration is stitched. CORT succeeds at constructing functional tests for ITC99 and IWLS-2005 benchmarks that achieve high branch coverage using the fewest number of input vectors, faster than existing methods. Furthermore, we achieve orders of magnitude speedup compared to previous hybrid concrete and symbolic simulation based techniques. / Master of Science / In recent years, the cost of verifying digital designs has outpaced the cost of development, in terms of both resources and time. The scale and complexity of modern designs have made it increasingly impractical to manually verify the design. In the process of circuit design, designers use Hardware Descriptive Languages (HDL) to abstract the design in a manner similar to software programming languages. This thesis presents a novel methodology for the automation of testing functional level hardware description with the aim of maximizing branch coverage. Branches indicate decision points in the design, and tests with high branch coverage are able to thoroughly exercise the design in a manner that randomly generated tests cannot. In our work, the design is simulated concretely with a random test (a sequence of input or stimulus). During simulation, we analyze the flow of behavioral statements and decisions executed to construct a formulaic interpretation of the design execution in terms of syntactical elements, to uncover differentiating input that could have diverted the flow of execution to unstimulated parts of the design. This process is formally known as Concolic Execution. The techniques described in this thesis tightly interleaves concrete and symbolic simulation (concolic execution) of hardware designs to generate tests with high branch coverage, orders of magnitude faster than previous similar work.
| Identifer | oai:union.ndltd.org:VTETD/oai:vtechworks.lib.vt.edu:10919/78397 |
| Date | 21 July 2017 |
| Creators | Pinto, Sonal |
| Contributors | Electrical and Computer Engineering, Hsiao, Michael S., Schaumont, Patrick R., Zeng, Haibo |
| Publisher | Virginia Tech |
| Source Sets | Virginia Tech Theses and Dissertation |
| Detected Language | English |
| Type | Thesis |
| Format | ETD, application/pdf |
| Rights | In Copyright, http://rightsstatements.org/vocab/InC/1.0/ |
Page generated in 0.0015 seconds