Complete Functional Testing from VHDL descriptions.

Supervisors: L. Seed (EEE), M. Holcombe (DCS).

Description

Currently, RTL based VHDL is the level at which chip design is done - followed by synthesis to netlist. Whilst there has been much progress in the automaticinsertion of test structures and generation of test patterns for manufacturing test (allowing in excess of 90% fault coverage), this does not address the comprehensive functional testing which must be undertaken to ensure that the design is correct.

Generally, it is a requirement for the designer to verify the VHDL design against the specification by the generation of an adequate set of 'test vectors' at the design stage and ensure that, post layout, the design continues to function. The Department of Computer Science has recently developed a very powerful method of generating functional test sets based on descriptions written as generalised state machines. Building on this theoretical work and utilising tools developed to support this test set generation this project will seek to apply the techniques in a way that will be convenient for chip designers. The approach will be transform VHDL descriptions into this more abstract model at which level complete functional test sets may be generated. The method also identifies formal "design for test" conditions which need to be satisfied if the full fault detection capabilities of the functional tests are to be exploited. The forward path from these descriptions to VHDL is, seemingly, straigthtforward but the reverse transformation will present a number of challenging research issues although similar reverse engineering techniques have worked in other application areas.

The advantage of this work for designers is manifold:

The initial stages of the project will be concerned with identifying a set of transformational rules which will underlie the conversion of the VHDL syntax into Stream X-Machines (SXM) which preserves the semantics of the VHDL description. These rules will then be codified into an algorithm and a tool for automatically translating the VHDL descriptions into the requisite semi-diagrammatic formal notation of SXMs. The tool will probably be built in C++ (or Java) and will then interface with the existing test generation tools developed in the Department of Computer Science in collaboration with Daimler-Benz Research Labs, Berlin.

A number of case studies utilising existing VHDL descriptions of circuits will be used to evaluate the approach and the functional test sets obtained will then be applied to some of these case studies. These case studies will be selected to be representative of different design styles (e.g. control and datapath) to ensure that the techniques developed are usable across a wide range of applications - or to identify limitations.

Who Can Apply

The studentship is primarily targetted at students whose first degrees are in the area of Electronic Engineering or Computer Science although applications from any students from numerate disciplines will be considered.

For further information please contact:

Dr Luke Seed

Department of Electronic and Electrical Engineering

0114 2225844

N.Seed@sheffield.ac.uk

Professor Mike Holcombe

Department of Computer Science

0114 2221802

M.Holcombe@dcs.sheffield.ac.uk

 

Use of formal design technology to improve the treatment of constraints in hardware specification and synthesis.

Supervisors: Dr. Seed (EEE), and Dr. Fairtlough (DCS)

Description

In traditional, informal, design approaches, constraints are considered as early in the design process as possible to ensure that, at a later stage in the design, they will not cause problems. For example, timing constraints are considered during synthesis but the true situation is not known until a design is placed and routed and the real delays are known. These are then fed back to allow re-simulation and checking. If a problem is detected then it probably requires re-synthesis - or re-design. Other important constraints include limits on data size and power consumption, as well as testability and structuralconsiderations such as design partitioning and component size.

On the other hand, in formal design approaches, such relatively low-level constraints have traditionally been ignored to the detriment of utility and consequently of industrial interest and support. However, EPSRC have recently agreed to fund a 171,000 project which aims to extend Fairtlough and Mendler's general theory of abstraction and refinement to multiple abstraction levels and apply it to improve the treatment of constraints in formal hardware design (the investigators for this EPSRC project are Dr. Fairtlough and Professor Holcombe).

The first aim of the PhD project will be to identify a set of transformational rules which will underlie a semantics-preserving conversion of the VHDL syntax into Higher Order Logic (HOL). These rules will then be codified into an algorithm and a tool for automatically translating VHDL design descriptions into the requisite formal behavioural descriptions in HOL. Once in this form, formal development can begin, for example by constructing proofs that the design satisfies required or desirable properties.

The second aim of the project will be to back-annotate the formal development with constraint information generated by the tools used for synthesis, thus providing formal proofs that the synthesis has not corrupted the functional behaviour of the device, and that the implementation will not violate the required constraints. These proofs would provide a good indication that the implementation was high quality. An adjunct to the proposed process is that design information will be described more formally.

The studentship would benefit from and support the EPSRC project outlined above. The advantage to EEE is the fact that representation and refinement of the design - and the embodiment of the constraints - at a levels of abstraction above VHDL could simplify and accelerate the overall design process. The principal criterion of success would be whether the resultant implementations were comparable or better in terms of salient features (which come down to quality and cost). To this end, a number of case studies utilising existing VHDL descriptions of circuits will be used to evaluate the approach. These case studies will be selected to be representative of different design styles.

Who Can Apply

The studentship is primarily targetted at students whose first degrees are in the area of Electronic Engineering or Computer Science although applications from any students from numerate disciplines will be considered.

For further information please contact:

Dr Luke Seed

Department of Electronic and Electrical Engineering

0114 2225844

N.Seed@sheffield.ac.uk

Dr Matt Fairtlough

Department of Computer Science

0114 2221826

M.Fairtlough@dcs.sheffield.ac.uk