Formal Methods in Hardware Verification


FORMAT - 6128

Keywords design methodologies, design tools, formal proving methods, testability, technology transfer


Start Date: 01-JUN-92 / Duration: 42 months

[ contact / participants ]


Objectives

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.


CONTACT POINT

Dr J. Goicolea Ruigomez
Tecnologica Grupo INI
Electronica
Plaza del Marques de Salamanca, 3-4
E - 28006 Madrid
tel: + 34 / 1-396-4923
fax: + 34 / 1-396-4841

Participants

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
TELEFONICA INVESTIGACION
Y DESARROLLO - E - A


TCS synopses home page TCS acronym index TCS number index
All synopses home page all acronyms index all numbers index

FORMAT - 6128, December 1993


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook