Keywords design methodologies, design tools, formal proving methods, testability, technology transfer
Start Date: 01-APR-90 / Duration: 48 months
[ contact / participants ]
The project aims to provide a set of architectural-level design methodologies and prototype design support tools. These will allow a designer to prove formally the correctness of a design, evaluate its testability at a high level of abstraction, and assess its complexity in terms of its silicon implementation. These tools will operate at a very high level of abstraction, allowing a designer to make reasoned decisions about architectural choices. The new tools, rather than constituting an architecture compiler, will consist of a set of advisers that provide information on such design issues as correctness, testability, and complexity.
Moreover, such advisers can be technology-independent, permitting a final design to be implemented in various microelectronics technologies, depending upon further considerations (second sourcing, etc.) that do not strictly relate to architecture design constraints. Thus designs can be optimised at high-level prior to choosing a specific microelectronics technology for its implementation.
The project will provide:
In the second half of the project, the original research and technology transfer activities have been joined by an evaluation and application phase. Progress has been as follows:
Formal methods: There have been two major lines of work. The first focuses on algebraic representations of specifications. A theory and software has been developed for a Petri-net instance of an algebraic composition theory, integrating the synchronous composition of Petri-nets and CCS expressions. The Knuth-Bendix algorithm has been extended for equational reasoning. A state graph and data flow graph instance of a categorical theory of decomposition has also been implemented. The second line of work has been based on Abstract Hardware's LAMBDA/DIALOG verification tools, and has involved collaborative working with the industrial partners on some actual industrial problems in order to develop the tools and their interfaces. Prototype software has been developed to interface the LAMBDA output in EDIF and VHDL formats to the testability assistant tool under development in the testing area. The same interface, based on VHDL modules will also be used to create a link with standard CAD design flow.
Testing: Prototype software has been developed to perform test-pattern generation for 1- and 2-dimensional regular arrays, binary-tree architectures and some commonly-used VLSI circuit blocks (adder, decoder, shifter) from a graph description. Algorithms have been developed for testability analysis of array architectures. A means of unifying the work on arrays with "random" logic circuits has also been developed, based upon exhaustive test applied to each block of a partitioned version of the circuit-under-test. Fault-mapping rules for systolic and semi-systolic arrays of different interconnection topologies have been formalised. A representation at the functional level has been defined for sequential machines and associated faults, together with a test procedure and prototype software allowing full functional fault coverage to be obtained. The insertion of testability rules for regular structures into the selected expert system shell has been completed. A taxonomy of design for testability techniques has been completed, and a literature survey and interviews with the user partners (Italtel and GEC Avionics) undertaken to extract the rules used in their current design flow. This information will be formalised for inclusion in the testability adviser. An output format in VHDL will be developed to interface the testability assistant with the standard CAD design flow.
Complexity analysis: A method has been developed to derive alternative architectures for a given problem, and to evaluate the main characteristics of the alternative architectures. The method is based on a representation of the algorithm through Data Flow Graphs (DFGs). Control of the algorithm has been embedded in nodes so that the DFGs may describe iterative algorithms as well as general ones. Graph manipulation may be guided by technological parameters or constraints or by user-defined evaluation parameters. The loop will then consist in an iteration of the manipulation and evaluation phases. Graph manipulation with subsequent identification of macro-nodes (sub-graphs) and folding, will reduce the parallelism of the structure. Inter-node scheduling between macro nodes yields the sequencing of the respective macro operations. Intra-node scheduling schedules then the operations of the whole graph. The algorithms keep the optimum of latency and throughput. The method is being implemented in a software tool.
Evaluation and application: This activity ensures that the high-level CAD tools and methodologies are developed to industrial requirements. Both Italtel and GEC Avionics have selected complementary, highly complex designs from their different application sectors. The synthesised designs are down to layout level by applying formal transformations using the LAMBDA/DIALOG toolset. The necessary testability requirements are introduced by means of the Testability Analyser/Advisor. At each stage, the designs and the methodology are reviewed by the industrial partners and compared to the original design.
Technology transfer: This activity involves all partners in promoting the results of the project, but in particular Italtel and GEC Avionics to transfer the emerging technologies into the design and manufacturing arms of their respective companies.
Mr Robert L. Harris
ABSTRACT HARDWARE LTD
Science Park Building 2
UK - Uxbridge UB8 3PQ
tel: + 44/ 895-258-501
fax: + 44/ 895-259-437
telex: 261173 G
ABSTRACT HARDWARE LTD - UK - C
BRUNEL UNIVERSITY - UK - P
GEC AVIONICS LTD - UK - P
ITALTEL SIT - I - P
POLITECNICO DI MILANO - I - P
PATRICIA - 5020, December 1993
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook