Hardware Methods Group Bibliograpy

[1]

Danko Antolovic, Bryce Himebaugh, and Steven D. Johnson. The Sk^ey^eball tracking project. 16th Florida Conference on Recent Advances in Robotics (FCRAR'2003), small tt http://www.eng.fau.edu/conf/fcrar2003/i, May 2003. 8-9 May 2003, Florida Atlantic University Seatech campus, Dania Beach, Florida. (PDF)

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.

[2]

Danko D. Antolovic, Bryce Himebaugh, and Steven D. Johnson. Skeyeball: Real-time vision system for an autonomous model airplane. In Proceedings of the 22nd Digital Avionics Systems Conference (DASC'03), October 2003. Indianapolis, Indiana. (PDF)

[3]

Steven D. Johnson. Formal methods in embedded design. Computer, 36:104-106, November 2003.

[4]

Steven D. Johnson, Yanhoung A. Liu, and Yuchen Zhang. A systematic incrementalization technique and its application to hardware design. International Journal on Software Tools for Technology Transfer, 4, 2003. (PDF)

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.

[5]

Danko Antolovic. Development of a real-time vision system for an autonomous model airplane. Technical Report 557, Indiana University Computer Science Department, Bloomington, Indiana, October 2002. Masters Thesis, small tt http://www.cs.indiana.edu/Research/techreports/TR557.shtml.

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.

[6]

Steven D. Johnson and Eric Jeschke. Modeling with streams in daisy/the schemengine project. In M. Sheeran and T. Melham, editors, Designing Correct Circuits, (DCC'02). ETAPS 2002, 2002. Presentation at the Workshop on Designing Correct Circuits, held on 6-7 April 2002 in Grenoble, France. (PDF)

[7]

Steven D. Johnson. View from the fringe of the fringe. In Tiziana Margaria and Thomas Melham, editors, 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001, Livingston, Scotland, Proceedings, volume 2144 of Lecture Notes in Computer Science, pages 1-12. Springer-Verlag, 2001. Invited paper. (PDF)

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.

[8]

Steven D. Johnson. Formal derivation of a scheme computer. Technical Report 544, Indiana University Computer Science Dept., Bloomington, Indiana, September 2000. http://www.cs.indiana.edu/ftp/techreports/.

This report describes a project involving the formal derivation and system-level verification of a computer for executing compiled Scheme.

[9]

Steven D. Johnson and Alex Tsow. Algebra of behavior tables. In C. M. Holloway, editor, Lfm2000: Fifth NASA Langley Formal Methods Workshop, pages 23-34, 2000. NASA Conference Publication NASA/CP-2000-210100. Proceedings of the 5th NASA Langley Formal Methods Workshop, Williamsburg, Virginia, 13-15 June, 2000, http://shemesh.larc.nasa.gov/fm/Lfm2000/. (PDF)

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.

[10]

Alex Tsow and Steven D. Johnson. Visualizing system factorizations with behavior tables. In Warren A. Hunt, Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, TX, USA, November 1-3, 2000, Proceedings, volume 1954 of Lecture Notes in Computer Science, pages 523-541, Heidelberg Berlin, 2000. Springer-Verlag. (PDF)

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

[11]

Steven D. Johnson. A workshop on formal methods education: an aggregation of opinions. International Journal on Software Tools for Technology Transfer, 2(3):203-207, November 1999.

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.

[12]

Steven D. Johnson, Warren P. Alexander, Shiu-Kai Chin, and Ganesh Gopalakrishnan. Report on the 21st century engineering consortium workshop. http://www.cs.indiana.edu/formal-methods-education/xxiec/report.html, March 1999. Report of the meeting held March 1998 at Melbourne, Florida.

[13]

Steven D. Johnson, Yanhong A. Liu, and Yuchen Zhang. A systematic incrementalization technique and its application to hardware design. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods (CHARME'99), volume 1703 of Lecture Notes in Computer Science, pages 334-337, Berlin, 1999. Springer. 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 1999, Proceedings. (PDF)

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.

[14]

Paul S. Miner. Hardware Verification using Coinductive Assertions. PhD thesis, Computer Science Department, Indiana University, USA, June 1998. Technical Report No. 510, 138 pages.

[15]

Ingo Cyliax, Steven D. Johnson, and Bhaskar Bose. Arriving at FPGA based hardware Unix encription using iterated co-design methods. Technical Report 496, Indiana University Computer Science Dept., Bloomington, Indiana, October 1997. small tt http://www.cs.indiana.edu/ftp/techreports/TR496.html.

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.

[16]

Steven D. Johnson. A tabular language for system design. In C. Michael Holloway and Kelly J. Hayhurst, editors, Lfm97: Fourth NASA Langley Formal Methods Workshop, September 1997. NASA Conference Publication 3356, Proceedings of the 4th NASA Langley Formal Methods Workshop, Hampton, Virginia 10-12 September, 1997, http://archive.larc.nasa.gov/shemesh/Lfm97/.

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.

[17]

Steven D. Johnson. A tabular language for system design. Technical Report 485, Indiana University Computer Science Department, June 1997. Appended version of [16].

[18]

Steven D. Johnson and Paul S. Miner. Integrated reasoning support in system design: design derivation and theorem proving. In Hon F. Li and David K. Probst, editors, Advances in Hardware Design and Verification (CHARME'97), pages 255-272. Chapman-Hall, 1997. IFIP TC10 WG 10.5 International Conference on Correct Hardware and Verification Methods, 16-18 October 1997, Montreal, Canada.

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.

[19]

Kathryn Fisler. Exploiting the potential of diagrams in guiding hardware reasoning. In Gerard Allwein and Jon Barwise, editors, Logical Reasoning with Diagrams. Oxford University Press, 1996.

[20]

Kathryn Fisler. A Unified Approach to Hardware Verification Through a Heterogenious Logic of Design Diagrams. PhD thesis, Computer Science Department, Indiana University, USA, 1996.

[21]

Steven D. Johnson, Gerard Allwein, and K. Jon Barwise. Toward the rigorous use of diagrams in reasoning about hardware. In Gerard Allwein and Jon Barwise, editors, Logical Reasoning with Diagrams. Oxford University Press, 1996.

[22]

Paul S. Miner and Steven D. Johnson. Verification of an optimized fault-tolerant clock synchronization circuit. In Mary Sheeran and Satnam Singh, editors, Designing Correct Circuits, Electronic Workshops in Computing, http://www.ewic.org.uk/ewic/workshop/view.cfm/DCC-96. Springer, September 1996. (PDF)

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.

[23]

Paul S. Miner and James F. Leathrum, Jr. Verification of IEEE compliant subtractive division algorithms. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design, FMCAD '96, volume 1166 of Lecture Notes in Computer Science, pages 64-78, Palo Alto, CA, November 1996. Springer.

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.

[24]

N. Shankar. Steps towards mechanizing program transformations using PVS. Science of Computer Programming, 26(1-3):33-57, 1996.

[25]

Kathryn Fisler. A cononical form for circuit diagrams. Technical Report 432, Indiana University Computer Science Department, May 1995.

[26]

Kathryn Fisler. Extending formal reasoning with support for hardware diagrams. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD'94), volume 901 of Lecture Notes in Computer Science, pages 298-303. Springer, 1995. Second International Conference, TPCD '94, Bad Herrenalb, Germany, September 26-28, 1994, Proceedings.

[27]

Kathryn Fisler. A logical formalization of hardware design diagrams. Technical Report 416, Indiana University Computer Science Department, September 1995.

[28]

Kathryn Fisler and Steven D. Johnson. Integrating design and verification envrionments through a logic supprting hardware diagrams. In Procedings of the 1995 IFIP International Conference on Computer Hardware Description Languages and Their Applications, pages 669-674. IEEE Cat. No. 95TH8102, September 1995.

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.

[29]

Steven D. Johnson, Paul S. Miner, and Albert Camilleri. Studies of the single pulser in various reasoning systems. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD'94), volume 901 of Lecture Notes in Computer Science, pages 209-227. Springer, 1995. Second International Conference, TPCD '94, Bad Herrenalb, Germany, September 26-28, 1994, Proceedings. (PDF)

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.

[30]

Kamlesh Rath. Sequential System Decomposition. PhD thesis, Computer Science Department, Indiana University, USA, 1995. Technical Report No. 457, 90 pages.

[31]

Kamlesh Rath, Venkatesh Choppella, and Steven D. Johnson. Decomposition of sequential behavior using interface specification and complementation. VLSI Design, 3(3-4):347-358, 1995.

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.

[32]

M. Esen Tuna, Kamlesh Rath, and Steven D. Johnson. Specification and synthesis of bounded indirection. In Proceedings of the Fifth Great Lakes Symposium on VLSI (GLSVLS I'95), pages 86-89. IEEE, March 1995.

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.

[33]

Bhaskar Bose. DDD-FM9001: Derivation of a Verified Microprocessor. PhD thesis, Computer Science Department, Indiana University, USA, 1994. Technical Report No. 456, 155 pages, //ftp.cs.indiana.edu/pub/techreports/TR456.html.

[34]

Robert G. Burger. The scheme machine. Technical Report 413, Indiana University, Computer Science Department, August 1994. 59 pages.

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.

[35]

Paul S. Miner, Shyamsundar Pullela, and Steven D. Johnson. Interaction of formal design systems in the development of a fault-tolerant clock synchronization circuit. In  13th Symposium on Reliable Distributed Systems (RDS'94), pages 128-137, 1994. (PDF)

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.

[36]

Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. Specification and synthesis of bounded indirection. Technical Report 398, Indiana University, Computer Science Department, February 1994. Published as [32].

[37]

M. Esen Tuna, Steven D. Johnson, and Bob Burger. Continuations in hardware-software codesign. In Proceedings of the 1994 IEEE International Conference on Computer Design (ICCD'94), pages 264-269. IEEE Cat. No. 94CH35712, October 1994.

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.

[38]

Zheng Zhu and Steven D. Johnson. Capturing synchronization specifications for sequential compositions. In Proceedings of the 1994 IEEE International Conference on Computer Design (ICCD'94), pages 117-121. IEEE Cat. No. 94CH35712, October 1994.

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.

[39]

Bhaskar Bose and Steven D. Johnson. DDD-FM9001: Derivation of a verified microprocessor. an exercise in integrating verification with formal derivation. In G. Milne and L. Pierre, editors, Correct Hardware Design and Verification Methods (CHARME'93), volume 683 of Lecture Notes in Computer Science, pages 191-202. Springer, 1993. IFIP WG 10.2 Advanced Research Working Conference, CHARME'93, Arles, France, May 24-26, 1993, Proceedings.

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.

[40]

Bhaskar Bose, Steven D. Johnson, and Shyam Pullela. Integrating boolean verification with formal derivation. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications (CHDL'93), volume A-32 of IFIP Transactions, pages 127-134. North-Holland, 1993. Proceedings of the 11th IFIP WG 10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL'93, sponsored by IFIP WG 10.2 and incooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993.

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.

[41]

Bhaskar Bose, M. Esen Tuna, and Steven D. Johnson. System factorization in codesign: A case study of the use of formal techniques to achieve hardware-software decomposition. In Proceedings of the International Conference on Computer Design (ICCD'93), pages 458-461. IEEE Cat. No. 93CH3335-7, October 1993.

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.

[42]

Kamlesh Rath and Steven D. Johnson. Toward a basis for protocol specification and process decomposition. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications (CHDL'93), volume A-32 of IFIP Transactions, pages 169-186. North-Holland, 1993. Proceedings of the 11th IFIP WG 10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL'93, sponsored by IFIP WG 10.2 and incooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993.

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.

[43]

Kamlesh Rath, Bhaskar Bose, and Steven D. Johnson. Derivation of a DRAM memory interface by sequential decomposition. In Proceedings of the International Conference on Computer Design (ICCD'93), pages 438-441. IEEE Cat. No. 93CH3335-7, October 1993.

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.

[44]

Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. Behavior tables: A basis for system representation and transformational system synthesis. In Proceedings of the IEEE/ACM International Conference on Computer Aided Design (ICCAD'93), pages 736-740. IEEE Cat. No. 93CH3344-9, November 1993.

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.

[45]

Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. An introduction to behavior tables. Technical Report 392, Indiana University Computer Science Department, December 1993. condensed version published in ICCAD'93.

[46]

Zheng Zhu and Steven D. Johnson. Automatic synthesis of sequential synchronizations. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications (CHDL'93), volume A-32 of IFIP Transactions, pages 285-301. North-Holland, 1993. Proceedings of the 11th IFIP WG 10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL'93, sponsored by IFIP WG 10.2 and incooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993.

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.

[47]

Zheng Zhu. Structured Hardware Design Transformations. PhD thesis, Computer Science Department, Indiana University, USA, 1992.

[48]

Bhaskar Bose. DDD - a transformation system for digital design derivation. Technical Report 331, Indiana University Computer Science Department, May 1991.

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.

[49]

Steven D. Johnson and Bhaskar Bose. A system for mechanized digital design derivation. In IFIP and ACM/SIGDA International Workshop on Formal Methods in VLSI Design, 1991. IFIP WG 10.2 conference series. Available as Indiana University Computer Science Department Technical Report No. 323 (rev. 1997).

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.

[50]

Zheng Zhu and Steven D. Johnson. An example of interactive hardware transformation. In P. A. Subramanyam, editor, IFIP and ACM/SIGDA International Workshop on Formal Methods in VLSI Design, January 1991. IFIP WG 10.2 conference series.

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.

[51]

Steven D. Johnson, R.M. Wehrmeister, and B. Bose. On the interplay of synthesis and verification: Experiments with the FM8501 processor description. In Claesen, editor, Formal VLSI Specification and Synthesis, VLSI Design Methods - I, pages 385-404. North-Holland, 1990. Proceedings of the IFIP WG 10.2/WG 10.5 International Worksho p on Applied Formal Methods for Correct VlSI Design, Sponsored by IMEC, Houtha len, Belgium, 13-16 November, 1989.

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.

[52]

K. Rath, I. Celis, and R. M. Wehrmeister. RTBA: A generic bit-sliced bus architecture for datapath synthesis. Technical Report 321, Department of Computer Science, Indiana University, December 1990.

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.

[53]

Zheng Zhu and Steven D. Johnson. An algebraic characterization of structural synthesis for hardware. In L.J.M. Claesen, editor, Formal VLSI Specification and Synthesis, VLSI Design Methods - I. North-Holland, 1990. Proceedings of the IFIP WG 10.2/WG 10.5 International Workshop on Applied Formal Methods for Correct VlSI Design, Sponsored by IMEC, Houthalen, Belgium, 13-16 November, 1989.

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.

[54]

Zheng Zhu and Steven D. Johnson. An algebraic framework for data abstraction in hardware description. In Garaint Jones and Mary Sheeran, editors, Designing Correct Circuits (DCC'90), Workshops in Computing. Springer, 1990. Workshop jointly organised by the Universities of Oxford and Glasgow, 26-28 September 1990, Oxford.

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.

[55]

C.D. Boyer and Steven D. Johnson. Using the digital design derivation system: case study of a VLSI garbage collector. In Darringer and Ramming, editors, Ninth International Symposium on Computer Hardware Description Languages (CHDL'89), Amsterdam, 1989. IFIP WG 10.2, Elsevier.

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.

[56]

Steven D. Johnson. Manipulating logical organization with system factorizations. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of Lecture Notes in Computer Science, pages 260-281. Springer, July 1989. Mathematical Sciences Institute Workshop, Cornell University, Ithaca, New York, USA, July 1989, Proceedings. (PDF)

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.

[57]

Steven D. Johnson and B. Bose. A system for digital design derivation. Technical Report 289, Indiana University, Computer Science Department, Indiana University, August 1989. Summary presented at the 1989 IEEE High Level Synthesis Workshop, Ken nebunkport, Maine.

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.

[58]

R.M. Wehrmeister. Derivation of an SECD machine: Experience with a transformational approach to synthesis. Technical Report 290, Indiana University, Computer Science Department, September 1989.

[59]

Steven D. Johnson and C.D. Boyer. Modelling transistors applicatively. In G.J. Milne, editor, The Fusion of Hardware Design and Verification, pages 397-420. North-Holland, 1988. Proceedings of the IFIP WG 10.2 Working Conference on The Fusion of Hardware Design and Vierification, Glasgow, Scotland, 4-6 July, 1988.

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.

[60]

Steven D. Johnson, B. Bose, and C.D. Boyer. A tactical framework for digital design. In Birtwistle and Subramanyam, editors, VLSI Specification, Verification and Synthesis, pages 349-383. Kluwer, Boston, 1988.

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.

[61]

Steven D. Johnson. Digital design in a functional calculus. In G. Milne and P.A. Subramanyam, editors, Formal Aspects of VLSI Design, pages 153-178. North-Holland, Amsterdam, 1986. Proceedings of tthe 1985 Edingurgh Workshop on VLSI, Edinburgh, Scotl and, U.K.

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.

[62]

Steven D. Johnson. Applicative programming and digital design. In Proc. Eleventh Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming (POPL'84), pages 218-227, 1984.

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.

[63]

Steven D. Johnson. Synthesis of Digital Designs from Recursion Equations. MIT Press, Cambridge, 1984.

[64]

Steven D. Johnson. Circuits and systems: Implementing communication with streams. IMACS Transactions on Scientific Computation, II:311-319, 1983.

[65]

Steven D. Johnson. Single pulser home page. A collection of sources and data for various studies in [29].

[66]

Steven D. Johnson. Sk^ey^eball project. Project home page, continually updated. small tt www.cs.indiana.edu/hmg/skeyeball/.