Specification-driven Validation of Programmable Embedded Systems
by Prabhat Mishra
Validation of programmable embedded systems, consisting of processor cores, coprocessors, and memory subsystems, is one of the major bottlenecks in current System-on-Chip (SOC) design methodology. One of the most important problems in validation of such systems is the lack of a golden reference model. As a result, many existing validation techniques employ a bottom-up approach to design verification, where the functionality of an existing architecture is, in essence, reverse-engineered from its implementation.
This thesis presents a top-down validation methodology that complements the existing bottom-up approaches. It leverages the system architect’s knowledge about the behavior of the design through architecture specification. We have developed validation techniques to ensure that the static and dynamic behaviors of the specified architecture are well formed. The validated specification is used as a golden reference model.
A major challenge in top-down validation methodology is the ability to generate executable models from the specification for a wide variety of programmable architectures. We have developed a functional abstraction technique that enables specification-driven model generation for simulation, hardware generation, and property checking. The generated simulator and hardware models are used for design space exploration of programmable architectures.
We have explored two top-down validation scenarios: design validation and test generation. First, the generated hardware is used as a reference model to verify the hand-written implementation using a combination of symbolic simulation and equivalence checking. Second, we have proposed a functional coverage based test generation technique for validation of pipelined processor architectures. The experiments demonstrate the utility of the specification-driven validation methodology for programmable embedded systems.