🚀 go-pugleaf

Subject: Postdoc vacancy for protocol verification in IC-design

Recently, a postdoc vacancy is created by a proposal of
the Philips Research Lab Eindhoven (the Netherlands),
that has been accepted by the European Communities program 
called "Human Capital and Mobility".
The technical part of the proposal is appended to this letter.

The topic can be seen as a special protocol verification problem,
although the word "protocol" is not mentionned in the proposal.

We search for skilled candidates, who are non-dutch Europeans,
who have received a PhD or are about to receive a PhD 
in computer science, mathematics or electronic engineering.
The two-year postdoc starts in Januari 1993.
Interested candidates should contact the address below as 
soon as possible, preferably within 2 weeks.

A.P. Kostelijk,
Philips Research Lab Eindhoven,
P.O. Box 800000, WAY 4.47,
5600 JA Eindhoven
The Netherlands
Phone: +31-40-743897
kostelij@prl.philips.nl  



TITLE

Formal verification of multi-rate IC-designs. 

DETAILED DESCRIPTION OF THE PROJECT 

The aim of the project is to solve fundamental problems that
prevent the verification of multi-rate IC-designs.
A multi-rate IC is a digital Integrated Circuit of which 
different parts run on different clock frequencies, 
and for which no simple timing relation 
between the constituent parts exist.
Proving correctness of the communication between these parts 
is difficult. From a functional point of view, 
the communication can be multi-synchronous or even asynchronous.
A digital signal processor for example, can consist of 
different parts running with different sampling frequencies, 
again with different clock frequencies, and the communication 
can be multi-synchronous, or ``asynchronous" via 
synchronised interrupts.

Until now, formal verification methods for IC design focus
on single clock systems only. Recent advances in this area,
such as for Finite State Machine verification and Retiming
verification are a step forward in verifying single clock parts,
but they do not address multi-rate IC-designs.
There is no known method to verify non-trivial multi-rate designs
in a reasonable way. 
The verification method currently applied, based on simulation,
is insufficient to get a reasonable impression of the correctness
of the communication between the constituent parts.
Only a very limited set of interrupts  and input patterns 
can be simulated because of the long simulation times that are needed. 
Checking synchronisation and setup procedures for every possible
situation is therefore prohibitive.
The only reasonable ``verification method" remaining is to test
how the actual IC behaves after it has been processed.

The research project will focus on the fundamental question of
how the communication can be modeled, and how the implementation
can be proven correct, while assuming that the constituent
(single clock) parts of the IC design are correct.

The strategy for tackling the verification problem in 
multi-rate IC designs will be based on exploiting the knowledge 
of formal verification methods in strong combination with 
IC design expertise and know-how. In this way, it is expected 
that parts of the verification problem will be solved, 
in particular those items that are most relevant for the IC designers.


RELEVANCE OF THE PROJECT TO THE TRAINING OF YOUNG RESEARCHERS

The Philips Research IC Design Centre offers the researcher 
an ideal environment to attack this challenging problem. 
It has an outstanding reputation for
IC design research and CAD for VLSI in general,
and for IC design verification in particular.
It combines both the academic freedom to explore new ideas
and the challenge to apply the ideas on industrial designs.
In this sense we have shown several times that 
the combination of our CAD research
and IC design expertise leads to unique CAD products
that are very useful in industrial design environments.


INDUSTRIAL, ECONOMIC AND SOCIAL RELEVANCE OF THE RESEARCH

Continuous advances in IC technology 
allow the integration of functions of ever growing complexity.
The number of single chip multi-rate system designs is growing rapidly,
but its verification is at present already a major bottleneck.
Therefore, multi-rate verification has become extremely important
to guarantee first time right IC designs, and the relevance
grows even more with time. First time right IC designs are essential
to reduce the time to market of new electronic products.