Keywords design methodologies, design tools, formal proving methods, testability, technology transfer
Start Date: 01-JUN-92 / Duration: 42 months
[ contact / participants ]
The objective of FORMAT is to reduce the design time for complex hardware modules by providing a set of system-level methods and design tools supporting an enhanced version of VHDL. Emphasis will be placed on formal verification and synthesis methods, whose introduction is expected to lead not only to designs of greater reliability but also to earlier recognition of errors in the design cycle. A transformation approach will also be explored.
FORMAT will specify and develop a graphical front-end and a specification language (VHDL-S) for use by designers. The graphical interface will use timing diagrams augmented to describe hierarchy and structure. Internally, specifications are automatically translated to either temporal logic or LOTOS, depending on the application domain and the approach envisaged.
The verification approach will use temporal logic as an intermediate language to capture, refine and process the specifications. VHDL descriptions will be internally translated into petri-net models from which transition systems will be generated, which will be checked against the specifications. Structural properties will be analysed directly in the PN model and interpreted in the VHDL description.
The transformation approach will use LOTOS to refine the specification through the use of formal methodology. This approach will specifically target the synthesis of communication controllers. The tools developed will be integrated with the LAMBDA system, the most advanced general theorem-prover framework.
Industrial demonstrators are planned in the fields of communications, advanced general-purpose processors and embedded control systems.
Dr J. Goicolea Ruigomez
Tecnologica Grupo INI
Plaza del Marques de Salamanca, 3-4
E - 28006 Madrid
tel: + 34 / 1-396-4923
fax: + 34 / 1-396-4841
TECNOLOGIA GRUPO INI SA - E - C
ABSTRACT HARDWARE LTD - UK - P
ITALTEL SIT - I - P
SIEMENS AG - D - P
KURATORIUM OFFIS EV - D - A
UNIVERSITÄT PASSAU - D - A
UNIVERSIDAD POLITECNICA DE MADRID - E - A
Y DESARROLLO - E - A
FORMAT - 6128, December 1993
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook