Unit Verification
Unit verification is the verification level at which most efforts are currently invested, and where the highest expectations, in term of bug discovery percentage, are placed. On this front, the Unit Verification and Core Technologies (UVCT) group has four separate activities.
Cache Verification
This domain encompasses cache and memory coherency verification, and includes two activities. First, the development of a Cache Loader for initializing caches in an interesting and legal manner. Second, support and further development of the CML (Coherency Monitor Light) tool.
Floating-point unit projects
In the unit verification domain, we have developed:
- FPgen - a test generator for the datapath of the floating-point unit.
- Generic Test Plan (GTP) - a comprehensive test plan for the floating-point unit.
FPgen development is now geared towards the enablement of the GTP implementation. Together, FPgen and GTP yield a comprehensive solution to the verification of the datapath of the Floating-Point unit. They were awarded a research accomplishment in 2003.
Formal Methods for Unit Verification
Whereas the overall direction of our verification department is on the simulation-based area, a few activities are invested in Formal Methods as well. Under this umbrella, we find two separate activities. First, the OneSpec project which aims at promoting a methodology and developing enabling technology for formally defining interface protocols. Second, we are active in the Error Recovery domain, in which we study the possibility to either formally analyze a given piece of logic to check whether it is protected, or - somewhat more ambitiously - automatically generate the related error recovery logic.
Functional Coverage
As a complement to random test generation, our department has been intensively active in the domain of Functional Coverage. On the one hand, we are developing and supporting a tool, Meteor, which enables to define coverage models and analyze the related verification progress through multiple types of reports. On the other hand, we are developing a solution based on Machine Learning techniques for Coverage Directed Generation, i.e., automatically closing the loop from test generation to coverage.
Manager
Laurent Fournier,
