The use of formal methods in VLSI design is currently a very active research area. This requires the specification of the behaviour of a hardware design in a formal, mathematically rigorous manner. Such specifications can subsequently be manipulated by proof systems (usually called 'proof assistants' or 'theorem provers') to prove the equivalence of hierarchical or temporal properties of hardware designs. We describe a prototype tool which integrates a theorem prover into the design environment in such a way as to ensure functional and trans formational correctness at all times. The system is driven from a hardware description language developed at Newcastle called STRICT, and it is interactive. Our aim in developing this tool is to make it easier for the designer to ensure correctness of the final implementation, without losing the benefit of his skill and experience.

This chapter describes CAD techniques capable of synthesising Fast Discrete Cosine Transform (FDCT) Blocks from behavioural, or algorithmic, specifications. We introduce SAVAGE (a Simulated Annealing based VLSI Architecture GEnerator), a software tool developed under the auspices of the Silicon Architectures Research Initiative (S ARI(Grant, 1990)) hosted at the University of Edinburgh. SAVAGE is capable of taking a data-flow description of an input algorithm, and applying a number of synthesis steps, or transformations, to produce a hardware netlist of a datapath. The netlist description is then passed to logic synthesis and layout tools to complete the route to silicon. These application specific synthesis steps are controlled by the computational technique known as simulated annealing. This chapter reviews the design process, from the initial high-level description of the FDCT, through the various synthesis transformations, and presents a set of test results illustrating the flexibility of the SAVAGE software. Finally, some extensions to the prototype SAVAGE system are described.

This chapter has described some current knowledge based systems to aid design for testability, and described research in this area taking place at Brunei University. It has also attempted to highlight specific problem areas in test strategy planning, and presented an economics based approach to the problem of test strategy evaluation. The system described here was constructed as a research tool, but the concepts and test strategy planning methods were used in a current ESPRIT project for gate array test strategy planning, which is now under industrial evaluation (Dislis et al, 1991). The basis of the test strategy planner is the cost modelling employed, which the authors believe is a reliable method for making realistic comparisons of design for test methodologies. The results of the economics based planning have so far agreed with test experts' approaches.

Techniques for the automatic generation of test patterns for digital circuits may be classified into four main areas; 1) random pattern generation... random input sequences which may be exhaustive, pseudo-exhaustive or used in conjunction with fault simulation tools to assess fault coverage. 2) heuristics ... these include checkerboard patterns and walking ones and zeros as well as functional tests; for automatic generation of such sequences there is the implication of some kind of expert system and the need for simulation to assess fault coverage. 3) path sensitisation... this encompasses the many variations on the D-algorithm and is probably the most widely used algorithmic technique. 4) algebraic techniques. It is with the last that this chapter is concerned.

The production of computer-aided design tools and environments for analogue VLSI circuit layout has proved very much more difficult than in the digital domain. The principal reason for this is that analogue circuit design involves the accommodation of many, often conflicting, practical constraints (Allen, 1986). Typical of these constraints are the optimum placement of circuit components, layout of large transistors, routing of interconnection channels noting the importance of avoiding signal cross talk, and the minimisation of parasitics which might affect circuit performance (Haskard and May, 1988, Kimble et al, 1985 and Serhan, 1985). In addition, the design of analogue circuits requires precision modelling of individual components and extensive simulation to verify the desired performance (Rijmenants, 1988). The problems associated with analogue VLSI layout techniques are reasonably well understood by experienced analogue circuit designers and it is widely accepted that these problems cannot be solved purely algorithmically. To produce a sophisticated analogue VLSI layout design tool which will enable these demanding multiple-constraint problems to be solved effectively, requires the efficient incorporation of design expertise as an integral part of the automatic analogue VLSI layout design tool. The purpose of this work is essentially to make a contribution towards meeting these demands, and to provide a greater understanding of typical expert layout design rules and how they should be incorporated within the Expert Analogue Layout System (EALS).