This article describes a robotic vision system for a semi-autonomous aircraft. Skeyeball is an RC model aircraft developed to host research and educational projects in autonomous aviation. The vision system described here is designed to be integrated into the aircraft's robotic navigation system, with the objective of steering the plane relative to a selected feature on the ground. The vision system utilizes a combination of FPGA and microprocessor hardware. The algorithm is a sequence of digitizing, thresholding, edge detection and segmentation into connected components; this sequence is implemented as both ASICs and code. The system is radio-controlled, battery powered, and capable of tracking speed compatible with the flight of the model aircraft.
A systematic transformation method based on incrementalization and value caching generalizes a broad family of program optimizations. It yields significant performance improvements in many program classes, including iterative schemes that characterize hardware specifications. CACHET is an interactive incrementalization tool. Although incrementalization is highly structured and automatable, better results are obtained through interaction, where the main task is to guide term rewriting based on data specific identities. Incrementalization specialized to iteration corresponds to strength reduction, a familiar program refinement technique. This correspondence is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm, which has also served as an example of theorem prover based implementation verification. One goal of this study is to explore how ingenious design insights are discovered and applied in contrasting formal systems, as reflected in their supporting tools.
This thesis describes a real-time embedded vision system capable of tracking two-dimensional objects in a relatively simple (uncluttered) scene, in live video. This vision system is intended as a component of a robotic flight system, used to keep a model airplane in a holding pattern above an object on the ground. The system used a two-pronged approach to object tracking, taking into account the motion of the scene and the graphic ``signature'' of the object. The vision system consists of these main components: a motion-detection and filtering ASIC, implemented on FPGAs, a scene-analysis program running on a Motorola ColdFire processor, a dual-port RAM holding the image data, and a digital camera on a motorized gimbal.
Abstract. Formal analysis remains outside the mainstream of system design practice. Theorem proving is regarded by many to be on the margin of exploratory and applied research activity in this formalized system design. Although it may seem relatively academic, it is vital that this avenue continue to be as vigorously explored as approaches favoring highly automated reasoning. Design derivation, a term for design formalisms based on transformations and equivalence, represents just a small twig on the theorem-proving branch of formal system analysis. A perspective on current trends in is presented from this remote outpost, including a review of the author's work since the early 1980s.
This report describes a project involving the formal derivation and system-level verification of a computer for executing compiled Scheme.
A design formalism based on behavior tables was presented at Lfm97. This paper describes ongoing work on a supporting tool, now in development. The goal is to make design derivation, the interactive construction of correct implementations, more natural and visually palatable while preserving the benefits of formal manipulation. We review the syntax and semantics of behavior tables, introducing some new syntactic elements. We present a core algebra for architectural refinment, including new notational conventions for expressing such rules.
Behavior tables are a design formalization intended to make a derivational style of hardware design more efficient by illuminating transformation opportunities. Previously we developed a transformational algebra for direct equivalence of tables rather than some intermediate representation. A design tool is illustrated for system factorization; its core implements the fore-mentioned table manipulations
The 21st Century Engineering Consortium Workshop was devoted to educational issues in the area of formal methods. This article summarizes opinions and perspectives which emerged at the workshop and sketches a context for their assessment. There was broad agreement that advances in education are crucial to expanding formal methods practice. However, specific recommendations vary among interest groups and individuals. In this multi-faceted area, it is important to establish a framework for debating issues and presenting them to the broader community. Nowhere is this need greater than in discussions of education.
A systematic transformation method based on incrementalization and value caching, generalizes a broad family of program improvement techniques. The technique and an interactive tool supporting it are presented. Though highly structured and automatable, better results are obtained through interaction with an external intelligence, whose main task is to provide insight and proofs involving term equality. This process yields significant performance improvements in many representative program classes, including iterative schemes that characterize Today's hardware specifications. This is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm.
SRAM based FPGAs are well suited for using iterative hardware/software codesign techniques to derive hardware implementations from software algorithms. In this paper we present a case study of the Unix password encryption algorithm implemented in a FPGA using this technique. We have found that: 1. FPGAs are cost effective for accelerating custom algorithms such as Unix crypt, 2. SRAM based FPGA are suitable for secure implementations of hardware, and 3. software algorithms can be implemented swiftly in FPGAs using iterative codesign techniques.
A tabular language for describing synchronous behaviors is developed as a visual representation for formalized design derivation. A sketch of behavior table syntax and semantics is given. An example illustrates the kinds of formal manipulations investigated by the research. Evidence is accumulating that tables are perspicuous for specification, design, and verification, but graphical support is essential to their effective use.
Practical applications of formal methods research require the integrated use of distinct tools for reasoning and design. Many approaches to this problem involve embedding specialized verification procedures in a theorem prover or logical framework. In fact, some theorem provers are promoted as frameworks of just this kind. We discuss some of the problems inherent to such monolithic treatments, illustrating with studies we have done in ad hoc heterogeneous reasoning. For both technical and pragmatic reasons we conclude that shallow embedding, that is, integration through superficial syntax translation, is a reasonable and even necessary approach.
In previous work, we have explored the interaction between different formal hardware development techniques in the implementation of a fault-tolerant clock synchronization circuit. We present a clever optimization of this earlier design and illustrate how we have extended our framework to support its incremental design refinement. The primary design tool represents circuits as systems of stream equations, where each stream corresponds to a signal within the circuit. These signals are annotated with invariants which can be established using proof by coinduction. This study lays the groundwork for a more formal integration of disparite reasoning tools.
A parameterized definition of subtractive floating point algorithms is presented and verified using PVS. The general algorithm is proven to satisfy a formal definition of an IEEE standard for floating point arithmetic. The utility of the general specification is illustrated using a number of different instances of the general algorithm.
Formal methods and verification tools are difficult for designers to use. Research has been concentrated on handling large proofs; meanwhile, insufficient attention has been paid to the reasoning process. We argue that a heterogeneous logic supporting hardware diagrams and sentential logic provides a natural framework for reasoning and for the formal integration of design and verification environments. We present such a logic and demonstrate its flexibility on fragments of a traffic light controller design and verification problem.
The single-pulser is a clocked sequential device which generates a unit-time pulse on its output for every pulse on its input. This paper explores how a single-pulser implementation is verified by various formal reasoning tools, including [at present] the PVS higher-order theorem prover, a CTL model checker, the DDD design derivation system, and, in addition, the Octtools design environment. By fixing a single, simple example, the study attempts to compare how the underlying formalisms influence one's perspective on design and verification.
Decomposition of system behavior along functional boundaries into interacting sequential components is a key step in top-down system design. In this paper, we present sequential decomposition, a method for factoring sequential components from a system specification based on interface specifications of the components. The resulting components can be independently synthesized, or realized using off-the-shelf components. We introduce Interface specification language (ISL), based on finite-state machine semantics, to specify the input/output behavior of synchronous sub-systems. A component is factored from a system by embedding an implementation of the complement of its interface into the system description. The composition of a machine with its complement is shown to be isomorphic to the machine, and the composition of a machine with an implementation of its component is shown to be a safe interaction. We apply sequential decomposition to a non-trivial example, a special-purpose computer with Scheme programming language primitives as its instructions.
Bounded indirection is a restricted form of pointers for system specification. It provides a mechanism for compact descriptions of many complex control structures, such as interrupts, continuations, and dynamic connections between machines. We describe three kinds of indirection--control state, value and net indirection--for use in different aspects of system description. Transformations on indirection representations and methods for synthesizing bounded indirection within the framework of behavior tables are presented.
This paper describes the design and implementation of the Scheme Machine, a symbolic computer derived from an abstract Scheme interpreter. The derivation is performed in several transformation passes. First, the interpreter is factored into a compiler and an abstract CPU. Next, the CPU specification is refined so that it can be used with the Digital Design Derivation system. Finally, the DDD system assists in the transformation into hardware. The resulting CPU, implemented in field programmable gate arrays and PALs, is interfaced to a garbage-collecting heap to form a complete Scheme system.
We propose a design strategy that exploits the strengths of different formal approaches to establish a reliable path from a mechanically verified high-level description to a concrete gate-level realization. We demonstrate the use of this approach in the realization of a fault-tolerant clock synchronization circuit. We used the Digital Design Derivation system (DDD) to derive a major portion of the design leaving relatively small portions to be verified either by the use of a mechanical theorem prover (PVS) or by demonstrating boolean equivalence using Ordered Binary Decision Diagrams. The interface between the different formal systems has yet to be completely formalized but be believe our approach will provide an effective formal design path from high-level specifications to concrete realizations.
This paper presents a case study for using high-level programming techniques to support the migration of software into hardware. The example is a derived implementation of a symbolic processing machine. The design environment employs codesign to maintain consistency between an executable software model of the system and the individual hardware components that are extracted from it. The presentation focuses on the use of continuations to move from a procedural view of memory allocation to a process view. Our previous work has used functional models as a source for correct hardware derivation using a transformational algebra. The work reported here will result in extensions that deal more powerfully with the factorization of sequential subsystems.
We explore the problem of adding sychronization information to high-level system specifications. At this level of specification the components of a system may follow non-trivial but implicitly specified sequential protocols in order to perform their operations. We illustrate a method of extracting protocols for closely coupled systems of such components. A language is defined for specifying external timing and behavior. Although limited in its expressiveness, this language allows us to derive partial synchronization conditions in the form of timing inequalities. The solution to a system of timing inequalities is itself a timing expression from which a controlling state-machine can be synthesized.
The DDD-FM9001 is a 32-bit general purpose microprocessor formally derived directly from Hunt's mechanically verified Nqthm FM9001 microprocessor specification. The exercise was part of a project to construct an implementation of the FM9001 by applying DDD (Digital Design Derivation System), a transformation system which implements a basic design algebra of equivalence preserving transformations for circuit derivation, to the Nqthm FM9001 specification. The main thesis of this work maintains that derivation and verification represent interdependent facets of design and must be integrated if formal methods are to support the natural analytical and generative reasoning that takes place in engineering practice. In this paper we describe the continuation of previous work in which the DDD system was applied to Hunt's FM8501 specification. This paper describes the derivation of the DDD-FM9001 and compares the derived architecture and hardware realization with that of the FM9001 in an effort to better understand the interplay between derivation and verification.
With the growing complexity in VLSI technology, the need for powerful design tools has become essential to the future of computer design. Formal methods in VLSI are playing a fundamental role in design automation as techniques for derivation and verification provide a rigorous framework for reasoning about complex designs and guaranteeing integrity in the design process. However, derivation and verification have emerged as opposing approaches to design. This paper describes results in integrating formal derivational reasoning with low level verification systems. The work in progress is part of a project to construct an implementation of the FM9001 Microprocessor description by applying the DDD System, a transformation system which implements a basic design algebra of correctness preserving transformations for circuit derivation, in conjunction with verification systems. The purpose is to study the interaction between derivation and verification in hardware design. The result of this work is a derived FM9001 implemented in FPGAs defined by a rigorous path to hardware which integrates both derivation and verification.
A major element of codesign is the task of decomposing a design in order to target some of its components to hardware and some to software. We illustrate how a previously developed algebraic technique we call system factorization adapts to this notion of decomposition. As an example, we describe how the mechanization of system factorization was used in the formal derivation of a hybrid implementation of Hunt's FM9001 microprocessor using the DDD design derivation system. This case study also demonstrates the benefits to system-level design in combining an executable modeling language, its associated formal-reasoning systems, hardware synthesis tools, and a hardware development platform in an integrated prototyping environment.
In a formalism of top-down design, we consider the decomposition of behavioral specifications into interacting sequential components. The higher level of description specifies the operations to be performed in a major computation step. The goal is to incorporate a given interface specification in a lower-level specification that accounts for interactions with and among sequential components. This construction generalizes the earlier formalism of system factorization to include interface protocols. It expands on the objectives of high-level synthesis by considering control-synchronization loops in scheduling. This paper presents a specification language for sequential process interaction and develops an interpretation based on finite-state-machines. Operations of minimization, composition and complementation are defined; the last of these being the key to top-down decomposition. This is a formal model that has not yet been automated. A small example is used to illustrate the ideas.
Design and synthesis of DRAM based memory systems has been a difficult task in high-level system synthesis because of the relatively complex protocols involved. In this paper, we illustrate a method for top-down design of a DRAM memory interface using a transformational approach. Sequential decomposition of the DRAM memory interface entails extraction of a DRAM memory object from a system description that incorporates the read/write protocol and accounts for refresh cycles. We apply sequential decomposition to a non-trivial example, a formally derived realization of the Nqthm FM9001 microprocessor specification, called DDD-FM9001.
In this paper, we introduce behavior tables, an extension of register transfer tables, as a unified basis for reasoning about control, datapath, protocol, and data expansion facets of system synthesis. Behavior tables can model indirection in system specification, by allowing names of registers and states to be treated as values. Behavior tables are based on a finite state machine model and provide a framework for transformational design to derive a formally correct implementation from a specification. To illustrate our approach, we sketch some transformations on a behavior table description of the FM9001 processor.
To compose sequential systems, designers usually have to devise a synchronization mechanism which coordinates consituents of the composition in order to achieve certain goals of computation. In this paper, we present a simple language for specifying sequential behaviors. An advantage of the language is that a specification of synchronization, when composition is required, can be easily obtained form the specifications of subsystems. We also briefly describe an algorithm which converts a specification of synchronization to a description of synchronization in our language. Our approach illustrates that, with proper sequential descriptions of sybsystems, necessary synchronization can be obtained automatically. This frees designers from control design, thus leaving more time and energy to consider architectural improvement and timing efficiency.
DDD is a transformation system that implements a design algebra for synthesizing digital circuit descriptions from high-level functional specifications. The system reflects a formal approach to hardware synthesis based on algebraic manipulation of purely functional forms. The system is intended to provide a well founded, mechanized, algebraic tool set for design synthesis. DDD is implemented in the Lisp dialect Scheme as a collection of transformations that operate on s-expressions. Transformations are applied manually by the designer, either interactively or by creating a script, at various stages of the design process in order to derive hardware implementations. The hardware descriptions that are manipulated by DDD are written in Scheme and may be executed as Scheme programs. DDD derives a technology independent set of digital circuit descriptions which are projected to binary representations. Boolean equations are then generated from these descriptions and are integrated with existing logic synthesis tools, such as boolean equation minimizers, PLD assemblers, and VLSI layout generators.
A research group at Indiana University is investigating a formalization of digital system design that is based on functional algebra. The algebra is used to characterize of digital design techniques. We have developed a transformation system called DDD to facilitate this study. DDD stands for digital design derivation; the system is used interactively to translate higher level specifications into hierarchical boolean systems, to which logic synthesis tools are then applied. In this paper, we take a detailed look at how the system is used. In two small examples, we examine the sequence of intermediate expressions produced as an implementation is derived. We discuss how these expressions are used at strategic levels of thinking. We illustrate how the choice of target technology influences the tactical course of derivation. Throughout, we try to give a sense of how functional abstractions are manipulated in the engineering process. DDD is classified as a primitive synthesis system because it performs very little automatic optimization. Its primary purpose is to secure a core of algebraic laws from which its transformations are composed, thereby allowing us to explore the formalization of design at scale. However, there are several advantages to basing synthesis on algebraic manipulation. Since all intermediate representations are expressions, the engineer can examine and interact at any point in the synthesis path. Design animation--symbolic modeling of the design, using Scheme in this case--can be done almost directly.
This presentation demonstrates and example of correct circuit design through transformation. The example itself is simple. However, it exposes som important aspects of digital design transformation. The presentation focuses on the issue of finding suitable hardware architecture for the specified system and the correctness of the architecture. The paper discusses the transformations which carry out the design.
Verification and synthesis are interdependent aspects of engineering which reflect alternative ways of reasoning between specifications and implementations. They must be integrated if either is to reach its potential in practice. The experimentation reported here explores the interplay between design derivation, or synthesis by algebraic refinement, and verification by direct proof. A transformation system for digital design derivation (DDD), which is based on functional algebra, is applied to Hunt's FM8501 processor description, which is verified in the functional Boyer-Moore logic. A comparison of synthesized and verified architectures isolates those qualities of the implementation that require a proof of correctness. DDD is also used to reduce the FM8501 implementation to a gate level hardware description. The mechanized algebra sustains correctness as physical organization is imposed on the implementation. Thus, integrated synthesis obviates tedious proofs of behavioral equivalence at lower levels of description. The key requirement for integrating verification and synthesis is a unified treatment of abstraction. Since they were composed for the purpose of conducting a proof, the FM8501 descriptions present a good test for a synthesis system.
Register transfer equations are used to specify the register and ALU datapaths of machine architectures. RTBA (Register Transfer Bus Architecture) is a model for automatic bit-sliced VLSI implementation of register transfer equations. This article presents the steps followed in derivation of layout from a system of register transfer equations using RTBA. As an example, and implementation of the complete datapath of the min-max benchmark is derived through a series of behavior preserving transformations.
We present an algebraic method to specify hardware architectures. This method regards hardware architectures as extended abstract data types. Architectural constraints of hardware are expressed as operators of abstract data types; thus, they are part of architectural specifications. The serialization problem is formalized and discussed in the proposed framework.
The aim of this work is to extend the standard treatment of data types to a foundation for hardware synthesis. Hardware synthesis exposes several problems not typically consiered in software oriented theory. These include architectural constraints on the use of type instances, parallelism in the use of multiple instances, and consolidation of distinct types in a common process. Since we are concerned with the question of incorporating (more) concrete implementations of (more) abstract types found in higher levels of specification, our foundation must address these aspects of description. The paper begins with a condensed example of a stack based processor operating on a standard memory. The specification is compared to a target description in which both the stack and the memory are implemented by a single memory process. The remainder of the paper formalizes issues raised in the example.
The DDD transformation system, under development at Indiana University, reflects an approach to digital design synthesis based on a purely functional algebra. The system has been used to derive several working designs realized in PLD (programmable logic device) technologies. This paper reports on the reimplementation of one of these designs, a garbage collector, in VLSI. The design example provides a context for discussing the method of synthesis and its mechanization. A generic system of control transformations was developed to aid in meetin the architectural constraints of the VLSI target. The exercise also illustrates the role of the algebra in managing the translation from conceptual architecture to physical organization.
Logical organization refers to a system's decomposition into functional units, processes, and so on; it is sometimes called the `structural' aspect of system description. In an approach to digital synthesis based on functional algebra, logical organization is developed using a class of transformations called system factorizations. These transformations isolate subsystems and encapsulate them as applicative combinators. Factorizations have a variety of uses, ranging from the refinement of actual architecture to the synthesis of certain kinds of verification conditions. This paper outlines the foundations for this algebra and presents several examples.
The Digital Design Derivation system (DDD) is a facility for synthesizing digital implementations of higher level algorithmic specifications. It is being developed to explore an approach to design based on the algebraic manipulation of functional expressions. This summary reviews the motives for DDD's development, outlines the synthesis process, and reviews experience with the system.
An applicative modeling language is used to explore logical transistor behavior. An applicative source language is good at describing functional qualities, but relational qualities require a careful treatment. With this issue in mind, we examine ways to represent bidirectional information flow in combinational systems. Formal approaches to hardware verification and synthesis enjoy the support of flexible symbolic processing systems, which readily represent disparate aspects of design. What we mean here by ``modeling'' is the ad hoc manipulation of such representations. Our main purpose is to explore and illustrate techniques for this kind of activity. In particular, we show how the interrelated qualities of lazy semantics and recursive data definition contribute to the natural description of hardware structures and behaviors.
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. The transformation system discussed in this paper supports a basic design algebra. At this early stage of its development, the system is essentially an editor for deriving digital system descriptions from certain applicative specifications and for interactively manipulating them. It is integrated with existing assemblers for programmable hardware packages, such as the PAL components used to implement the examples presented in Sections 3 and 5.
A technique is presented for deriving synchronous-system descriptions from recursive function definitions, using correctness-preserving transformations. The use of functional abstraction to address control and communication is illustrated in a small example. The relationship of this technique to conventional digital design methodology is discussed.
An approch to deriving digital system descriptions from first-order recursion equations is described. The central constructions relates iterative systems of function definitions so systems of sequence (or stream) definitions. The example presented extends Wand's refinement of the min-max tree search to an alpha-beta search algorithm.