Skip to main content

Über dieses Buch

VLSI Specification, Verification and Synthesis Proceedings of a workshop held in Calgary from 12-16 January 1987. The collection of papers in this book represents some of the discussions and presentations at a workshop on hardware verification held in Calgary, January 12-16 1987. The thrust of the workshop was to give the floor to a few leading researchers involved in the use of formal approaches to VLSI design, and provide them ample time to develop not only their latest ideas but also the evolution of these ideas. In contrast to simulation, where the objective is to assist in detecting errors in system behavior in the case of some selected inputs, the intent of hardware verification is to formally prove that a chip design meets a specification of its intended behavior (for all acceptable inputs). There are several important applications where formal verification of designs may be argued to be cost-effective. Examples include hardware components used in "safety critical" applications such as flight control, industrial plants, and medical life-support systems (such as pacemakers). The problems are of such magnitude in certain defense applications that the UK Ministry of Defense feels it cannot rely on commercial chips and has embarked on a program of producing formally verified chips to its own specification. Hospital, civil aviation, and transport boards in the UK will also use these chips. A second application domain for verification is afforded by industry where specific chips may be used in high volume or be remotely placed.



1. Implementing Safety-Critical Systems: The VIPER Microprocessor

During the last five years industry has progressively spread the use of commercial microprocessors into many areas of real-time control. This has been particularly marked in military projects and has happened in a number of civil applications, such as control of nuclear reactors and railway signalling. Some of these applications are ‘safety-critical’ in the sense that design errors could result in accidents and loss of life. Good examples of such critical applications are found in the avionics fitted in civil and military aircraft [5].
W. J. Cullyer

2. A Proof of Correctness of the Viper Microprocessor: The First Level

The Viper microprocessor designed at the Royal Signals and Radar Establishment (RSRE) is one of the first commercially produced computers to have been developed using modern formal methods. Viper is specified in a sequence of decreasingly abstract levels. In this paper a mechanical proof of the equivalence of the first two of these levels is described. The proof was generated using a version of Robin Milner’s LCF system.
Avra Cohn

3. HOL: A Proof Generating System for Higher-Order Logic

HOL is a version of Robin Milner’s LCF theorem proving system for higher-order logic. It is currently being used to investigate (1) how various levels of hardware behaviour can be rigorously modelled and (2) how the resulting behavioral representations can be the basis for verification by mechanized formal proof. This paper starts with a tutorial introduction to the meta-language ML. The version of higher-order logic implemented in the HOL system is then described. This is followed by an introduction to goal-directed proof with tactics and tacticals. Finally, there is a little example of the system in action which illustrates how HOL can be used for hardware verification.
Michael J. C. Gordon

4. Formal Verification and Implementation of a Microprocessor

Mike Gordon has described the specification and verification of a microcoded computer using the LCF_LSM hardware verification system [8]. We have subsequently redone this example in higher-order logic using the HOL system [10]. In this paper we present the specification of Gordon’s computer in higherorder logic and a brief explanation of its formal verification. A more detailed discussion of the formal verification may be found in [16]. We also describe several related examples of hardware verification based on Gordon’s computer and other microprocessor designs. Finally, we report experience in using a formal specification to implement Gordon’s computer as a 5,000 transistor CMOS microchip.
Jeffrey J. Joyce

5. Towards a framework for dealing with system timing in Very High Level Silicon Compilers

The design of a VLSI system typically involves many decisions relating to several levels of timing detail. Examples include choices relating to timing disciplines, architectural and circuit design paradigms, the number of clock phases, the number of amplification stages, the sizes of specific transistors, and the temporal behavior demanded of specific input signals (such as stability criteria they must obey). This paper discusses a framework for dealing with system timing issues in the context of very high level silicon compilers intended to aid in mapping abstract behavioral specifications into VLSI circuits. The paradigm considered allows the details of system timing to be gradually introduced as a design progresses. During the early stages of a design, no timing details need be explicit, and the only temporal constraints arise due to functionality, causality and stability criteria. As a design evolves, and decisions relating to resource allocation, computation schedules, timing and clocking disciplines are made, the temporal constraints on signals evolve correspondingly. If the external environment in which a system resides imposes any a priori temporal constraints, such constraints can be explicitly included in the initial specification, and accounted for in the synthesis process. The framework supports synchronous and asynchronous (self-timed) disciplines, multiphase-clocks, as well as techniques that bear on optimizations of performance metrics such as power and area.
P. A. Subrahmanyam

6. BIDS: A Method for Specifying and Verifying Bidirectional Hardware Devices

Previous methods of formally verifying hardware designs have been highly simplified in comparison to the physical operation of the hardware devices themselves, which is appropriate for many kinds of circuit design but not for others. In particular, the register-transfer model and the state-transition model have not been able to handle bidirectionality (allowing lines sometimes to be used for input and at other times for output). The predicate model can handle simple cases of bidirectionality, but breaks down in others, particularly when gate capacitance and/or charge sharing are involved. In this paper we describe BIDS (BIdirectional Device Specification), a more elaborate model of hardware devices for formal verification, which we believe will be adequate for most techniques that designers commonly use, including bidirectionality, gate capacitance, and charge-sharing.
David R. Musser, Paliath Narendran, William J. Premerlani

7. Hardware Verification in the Interactive VHDL Workstation

Formal Hardware Verification has gained a lot of attention recently as a viable alternative to simulation. Several notable achievements have been reported, such as Hunt [4], Birtwistle et. al. [1]. In this document we describe one aspect of an ongoing project aimed at developing an integrated environment for hardware description, simulation, and verification. We report here on the current efforts toward developing tools for formal verification of hardware and how these tools interact with other parts of the IVW workstation being developed at General Electric Research and Development Center (GE CRD). This is of necessity a preliminary document, as our work in developing an environment for highly automatic verification of hardware is at an early stage.
Paliath Narendran, Jonathan Stillman

8. Contextual Constraints for Design and Verification

A new approach to the design and verification of VLSI structures capitalizing on knowledge of the surrounding environment is proposed. This approach formalizes the use of contextual information as a means of simplifying the design and verification process and provides us with a new way of viewing the hierarchical evolution of a design. The proposed design process illustrates the different uses of contextual constraints to aid and guide the designer. In particular, constraints may be introduced to simplify verification and must in turn be satisfied by the design itself. Hence we find that design choices may be made to aid validation, an interesting reversal in the usual post-design role of simulation and formal verification.
Bruce S. Davie, George J. Milne

9. Abstraction Mechanisms for Hardware Verification

It is argued that techniques for proving the correctness of hardware designs must use abstraction mechanisms for relating formal descriptions at different levels of detail. Four such abstraction mechanisms and their formalisation in higher order logic are discussed.
Thomas F. Melham

10. Formal Validation of an Integrated Circuit Design Style

A specific design style is only ever used if it meets the required needs of the task in hand. The task in hand now is that of generating large, complex, application specific systems on silicon in a fairly short space of time with the confidence that they will perform to the required specification. In the past the development of a large circuit might have been done using a team of engineers over a period of few years, e.g. the development of the 68000 microprocessor. This method of circuit development is not acceptable in the present day due to the time and manpower spent in iterating to get the design correct. What is needed is a design technique which is easy to follow and gives very high degree of confidence in the first time correct implementation of the circuit.
I. S. Dhingra

11. A Compositional Model of MOS Circuits

This paper describes a compositional model for MOS circuits. Following Bryant in [1] it covers some effects of capacitance and resistance used frequently in designs. Bryant’s model has formed the basis of several hardware simulators. From the point of view of verification, however, it suffers the inadequacy that it is not compositional, an expression which will be explained further. This makes it hard to use the model to reason in a structured way.
Glynn Winskel

12. A Tactical Framework for Hardware Design

This work explores an algebraic approach to digital design. A collection of transformations has been implemented to derive circuits, but “hardware compilation” is not a primary goal. Paths to physical implementation are needed to explore the approach at practical levels of engineering. The potential benefits are more descriptive power and a unified foundation for design automation. However, these prospects mean little when the algebra is done manually. Hence, a basic, automated algebra is prerequisite to our experimentation with design methods.
Steven D. Johnson, Bhaskar Bose, C. David Boyer

13. Verification of Asynchronous Circuits: Behaviors, Constraints and Specifications

An algebraic methodology based on Characteristic Functions (CFs) and allowing to compare switch-level circuits with higher-level specifications is presented.
Switch-level networks, ‘user’ behaviors, input constraints and specifications are modelled as asynchronous automata which form a Boolean algebra.
Machine composition corresponds to the product of the Boolean algebra. Internal variables can be abstracted, and more generally, a component automaton can be reduced by projection under the presence of a local domain constraint. The constraints are validated by comparison with the actual user of each component
Formal verification implies comparison with a high-level specification which may either be complete or consists of a collection of properties. Verification of safety and liveness with respect to a property reduces to the validation of Boolean inequalities.
This methodology is applied to a new structure of mutual exclusion ensuring fairness.
C. Berthet, E. Cerny
Weitere Informationen