Interactive combat games are useful as test-beds for learning systems employing evolutionary computation. Of particular value are games that can be modified to accommodate differing levels of complexity. In this paper, the authors presented the use of Xpilot as a learning environment that can be used to evolve primitive reactive behaviors, yet can be complex enough to require combat strategies and team cooperation. In addition, this environment was used with a genetic algorithm to learn the weights for an artificial neural network controller that provides both offensive and defensive reactive control for an autonomous agent.

We report the first formal verification of a reintegration protocol for a safety-critical distributed embedded system. A reintegration protocol increases system survivability by allowing a transiently-faulty node to regain state. The protocol is verified in the Symbolic Analysis Laboratory (SAL), where bounded model-checking and decision procedures are used to verify infinite-state systems by k-induction. The protocol and its environment are modeled using a recently-developed explicit real-time model. Because k-induction has exponential complexity, we optimize this model to reduce the size of k necessary for the verification and to make $k$ invariant to the number of nodes. A corollary of the verification is that a clique avoidance property is satisfied.

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 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 will result in extensions that deal more powerfully with the factorization of sequential subsystems.>

We explore the problem of adding synchronization information to high-level system specifications. At this level of specification the components of a system may follow non-trivial, but implicitly specified sequential protocol 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.>

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 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 not yet been completely formalized but we believe our approach will provide an effective formal design path from high-level specifications to concrete realizations.>

Introduces 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.

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 while maintaining the integrity of the execution model. We illustrate how a previously- developed algebraic technique which 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 an implementation of Hunt's (1992) FM9001 microprocessor description using the DDD (digital design derivation) system. This case study demonstrates the benefits to system-level design in combinational-reasoning systems, hardware synthesis tools, and a hardware development platform in an integrated prototyping environment.>

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.>

This paper adapts applicative programming techniques to the synthesis of mynchronaua system descriptions.It presents a unifying perspective on hardware and software engineering and shows that a functional design paradigm is suitable in both realms.Established techniques for program synthesis are extended to yield hardware descriptions.This work stems from research in general programming methods for systems.Synchronous systems are a valuable special case.They are a preferred basis for hardware design: logical synchrony makes circuits easier to conceptualize, and physical synchrony makes them easier to test.Applicative notation is well suited to the description of digital circuits because it has an immediate interpretation in terms of wiring.Digital circuits are a reasonable target for synthesis because they are functional in character.The design approach is conventional: a circuit is viewed as a sequential control algorithm acting on an architecture [17].This should sound familiar to programmers who view their product as an algorithm acting on an abstract type.An engineer starts with an abstractly descriptive specification and derives a concretely descriptive realization.These notations should be suited not only to what they describe but also to each other.