The FORMAT project (#6128) successfully demonstrated a model-checking tool for the formal verification of VHDL designs.

The CheckOff range of products sold by Abstract Hardware Limited (AHL) exploits this technology. AHL`s experiences in selling CheckOff has exposed some limitations in the current generation of tools.

 

The V-FORMAT project aims to refine the CheckOff toolset so that it can address true system-level issues

 

Technical Improvements

The technical improvements sought in V-FORMAT fall into 3 major areas:

 

Timing Diagram Extensions and Improvements. This addresses theneed to produce compact representations for synchronous designs.

 

Technology scaling. AHL`s experience is that the most importantchallenge for the wider uptake of model-checking tools is performance. V-FORMAT will address this issue.

 

Industry standards. The V-FORMAT tools will build on industry-standardlanguages and toolsets.

 

The focus of VFORMAT is on enhancing the power of an existing product,the CheckOff tool, supporting formal verification of VHDL-based hardware designs. In particular

 

VFORMAT recognises the need of users of the current technology to stretchthe limits of component verification;

 

V-FORMAT extends the domain of formal verification methods by movingfrom component verification to system verification;

 

V-FORMAT considers it instrumental to not only provide bare technologicalenhancements but to develop methodological guidelines for their integration in standard industrial design flows;

 

V-FORMAT is driven from user-requirements and evaluation as well asmarket pull and thus establishes a close feed-back loop incorporating scheduled training of designers and potential customers on the technological enhancements.

 

The Partners and their Work

The VFORMAT project is to be carried out by the same team of partnerswhich successfully co-operated within the FORMAT project. The blend of partners guarantees cost-effective achievement of the goals of the project: they have excellently interacted in turning the development of the FORMAT verification tools into a success and thus have well established communication channels. At the same time, all partners have a clearly identified role, providing the minimal consortium size to achieve the project goals.

ITALTEL has gained substantial experience in the use of formal verification tools in the development of telecommunication chips. ITALTEL will not only provide feedback on the enhancements of the verification tools, but also assure, that they can be embedded in standard industrial design flows. ITALTELs similar function in the FORMAT project was instrumental to its success.

 

SIEMENS acts both as the key provider of the model-checking and equivalence-checking technology and as a highly experienced user of formal methods in IC developments for ATM- and consumer-electronic applications. The rich experience gained from numerous industrial applications of model-checking provides an excellent impetus in driving the optimisations of the kernel technology. It is fair to say, that the SIEMENS model-checking team has a leading edge over competitive groups due to its long standing record of industrial usage of the technology.

 

OFFIS is internationally recognised as a competence centre for the use of formal methods. OFFIS as the key designer of FORMATs verification environment will push the limits of the current toolset using innovative technologies, making the model-checking technology applicable to more complex components through the use of abstraction techniques, and extending the verification method to cover design hierarchies through compositional proof-methods.