|
|
|
GENEVIEVE
| |
GENeration ENvironment for Effective VErification
Summary
|
|
|
Genevieve is an R&D project funded by the European Union (Esprit project 25314), in which the IBM Haifa Research Laboratories serve as a key technology provider.
The objective of this project is to automate the generation of testing requirements from micro-architecture models to assist in verifying the design of embedded processors at the micro-architecture level. With this objective, the project addresses the rapidly increasing cost and complexity of verifying the design of embedded processors, due to the advances in architecture and integration, which result in increasingly complex designs.
Motivation
|
|
|
The worldwide market for embedded processors is highly competitive. The drive for higher performance and higher integration result in increasingly complex designs for modern processors. Success is dependent on finding design errors before a device is actually fabricated or already in use in potentially safety critical applications. While the transition from a high-level design to silicon can be made very reliable with modern techniques such as synthesis and silicon compilation, design errors that cause the device to behave incorrectly can only be prevented by intense scrutiny of the design. This scrutiny, known as functional verification, is currently estimated to take 30% to 50% of the total design resources; this share increases as designs become more complex.
Design verification can, in principle, be performed by either simulation or formal verification. However, presently, formal techniques such as model checking are still only applicable to limited parts of the design verification process. The functional verification of processors is thus mainly based on simulation. This cannot be exhaustive hence the selection of test cases becomes crucial to the discovery of bugs. The current state-of-the-art is model based test program generation. This automates the process of finding good test cases that verify the design against the instruction set architecture. However, the discovery of more subtle design errors is still dependent on the skill of a team of verification engineers. This process is very labor intensive and the test programs are of indeterminate quality and difficult to maintain as the design changes.
We believe that the next logical step in verification technology involves merging the current state-of-the-art techniques in model based test program generation, coverage, and formal verification to produce tools that will generate effective test programs based on a model of the top level design, called the micro-architecture.
Accordingly, this project will develop:
- A methodology for high level modeling of the micro-architecture of a microprocessor, in a way that captures the knowledge required for design verification.
- Prototype tools for identifying the required test cases. These tools will merge state-of-the-art techniques in simulation, coverage, and formal verification.
The tools and methodology developed by this project will be refined and validated by applying them to a state-of-the-art embedded processor. The techniques to be developed by this project will play an important role in controlling the escalating costs and time scales for verification that are a direct consequence of this trend. Specifically, the results of this project will be exploited directly by IBM and SGS-Thomson Microelectronics in the development of embedded processors and micro-controllers. They will also be exploited externally for verifying programmable devices such as digital signal processors and systems on a chip built around existing processor cores. To ensure this happens, the project has made provisions for a technology transfer into the European electronics design automation market through the involvement of LEDA, a specialist EDA European tools vendor.
Technology Overview
|
|
|
Genevieve will consist of a set of tools for micro-architecture modeling and the generation of test specifications driven by coverage measures. The functional components of Genevieve will include:
- A modeling language compiler: The modeling language will be a dialect of a widely used hardware description language and will facilitate the formulation of high level models. The compiler will translate this language into a format that is suitable for simulation. The language will also supply directives for test generation and requirements (constraints) that all tests must satisfy. The compiler will be able to translate the model and directives to input for a test specifications generator.
- A test specifications generator: The micro-architecture model will be used as input to the test specifications generator (traversal tool). The test specifications generator will produce a finite state machine description of the model and will perform state space traversal to generate execution paths. The execution paths generated will be driven by a coverage model also supplied as input by the user. The test specifications generator will extract a suite of execution paths (or test specifications) that cover all of the tasks described in the coverage model. The generator will supply information on the list of tasks, expected to be covered in simulation, to the feedback tool described below. The test specifications generator will also support the feedback tool in its analysis of simulation traces.
- A translation tool: The legitimate test specifications will be translated into valid test cases for some simulation environment. The translation tool will attempt to extract information from the execution paths that describe the test input required to drive the unit on this path. The translation will be naive.
- A feedback tool: As the test translation is not expected to be accurate, there will be a need to measure coverage from the actual design simulation to verify that the desired execution paths have been simulated according to the test specifications. The feedback tool will extract coverage information from the abstract tests and from the traces of design simulation and compare the two. The result of the comparison will be fed back to the traversal tool, which will try to generate further execution paths that cover the tasks not appearing in the actual simulation. A few iterations of this process will give the desired coverage with minimal manual effort.
- A graphical user interface: The effectiveness of Genevieve will be enhanced if an appropriate verification methodology is used. A graphical interface that encapsulates the recommended methodology will be provided. Each tool will be activated by a set of panels of the graphical user interface, and the interface will be designed to create a natural progression between the tools when using the prescribed methodology.
The figure below depicts the verification flow as it will be supported by these tools:
The project's intention is to develop a modeling/verification methodology to use these tools by applying this methodology to an ongoing design in SGS-Thomson.
This project meets the objectives of the Open Microprocessor Systems Initiative domain 5.5 by providing a methodology and tools for increasing the automation of testing approaches for new processor designs.
Participants
|
|
|
The GENEVIEVE consortium consists of the following partners:
Publications
|
|
|
This results of this project are documented in:
|
|
|
|
|
