Digital Design Derivation

This ongoing research project in formal methods develops an algebraic approach to system design. We explore techniques and tools for implementing digital systems using constructions, transformations, and refinements. Other terms used for this general approach to design are transformational, generative, and constructive.

Our purposes in formalizing these processes are twofold. First, formalization enables us to create tools to secure design processes in practice. However, the tools we develop are more closely related to theorem provers than hardware synthesizers, which ``automatically explore the design space.'' Our research is concerned with computer-assisted reasoning, through which a formal system supports rational but computationally intractable design processes. Thus, it is targeted for that level of design just beyond the reach of synthesis tools, which themselves are continually advancing.

Second, formalizing helps consolidate our understanding of design processes so that we can teach them more effectively to future generations of engineers. This research project began around 1980 as an adaptation of applicative programming methodology to the specification and construction of digital systems. It continues to interact with contemporary research in software oriented methods. We would like to abolish all distinctions of hardware and software, and instead characterize each target technology as a combination of aspects principally including architecture, behavior, coordination, and data.

NSF support for this line of research began in 1987 with the grant Digital Design Derivation (MIP87-07067, 1987-89) and has continued under grants entitled Algebra for Digital Design Derivation (MIP89-21842, 1990-1992) and Decomposing digital-system specifications into interacting sequential processes (MIP92-08745, 1993-1996 A full list of resulting publications can be accessed through the World Wide Web at URL http://www.cs.indiana.edu/hmg/hmg.html.

Research Topics

Theoretical contributions include representations of behavioral and structural specification in functional algebra [5], adaptation of algebraic techniques to architectural refinement [26, 27, 25, 28], design decomposition based on interface specification [19, 17, 18, 16], and formalization of stream semantics [13]. We have done elementary studies comparing how different formal systems address the same design [12].

We implemented our formalism in a tool called DDD [1, 2], which is used interactively to transform higher descriptions of behavior to synthesizable hardware descriptions. We did several case studies to demonstrate the approach and illustrate the thesis that heterogeneous reasoning is is more effective than a comprehensive logic in design-critical applications [2, 13, 23, 14, 6, 5, 4, 3]. This component of our research reflects our ongoing commitment to exploring applications in real design settings, and to integrate the software we develop with existing CAD systems.

Behavior tables emerged as a useful language representation for interactive design derivation. We began using these tables informally to describe DDD [11] and later for the presentation of case studies. This has prompted us to consider them more seriously as an HDL, we are exploring features that are appropriate in higher levels of system specification [24, 22, 21, 20, 15]. The work with behavior tables also germinated an interest in the fundamental role of diagrams in formal mathematics [8, 10, 9].

The DDD system is now under commercial development, with SBIR funding through NASA, by Derivation Systems, Inc., Carlsbad California [7] (dvsi.com).. DSI is a start-up company established by graduates of this research group.

Our case studies have resulted in several design artifacts. A formally derived version of Hunt's FM9001 microprocessor is realized in FPGA technology [2]. A language-specific computer for compiled Scheme, containing a derived CPU, garbage collector, and allocator [6], is an ongoing case study relating to contemporary programming methods research. A custom VLSI realization of a fault-tolerant clock synchronization circuit has been verified and tested [13, 14]. Miner has also constructed a PVS theory of streams, to be published as part of his doctoral thesis in early 1997.

References

1

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

2

Bhaskar Bose. DDD-FM9001: Derivation of a Verified Microprocessor. PhD thesis, Computer Science Department, Indiana University, USA, 1994. Technical Report No. 456, 155 pages.

3

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, Proceedings of IFIP Conference on Correct Hardware Design and Verification Methods, pages 191-202. Springer, LNCS 683, 1993. also published as Technical Report 380, Computer Science Department, Indiana University.

4

Bhaskar Bose, Steven D. Johnson, and Shyam Pullela. Integrating boolean verification with formal derivation. In D. Agnew, L. Claesen, and R. Camposano, editors, Proceedings of IFIP Conference on Hardware Description Languages and their Applications, pages 127-134. Elsevier, April 1993. Also published as Technical Report No. 372, Dept. of Computer Science, Indiana University.

5

Bhaskar Bose, M. Esen Tuna, and Steven D. Johnson. System factorization in codesign: A case study of the use of formal gechniques to achieve hardware-software decomposition. In Proceedings of the International Conference on Computer Design, pages 458-461. IEEE, October 1993. Also published as Tech Report # 386, Computer Science Department, Indiana University.

6

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

7

Derivation Systems, Inc., Carlsbad, California. DRS: Derivational Reasoning System, 1.2.1 edition, December 1995. Contact drs@derivation.com.

8

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

9

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. CHDL proceedings pp. 493-696 of the ``ACV'95'' held August 29 to September 1, 1995, Chiba, Japan.

10

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

11

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. Participants' proceedings, workshop held in Miami, Florida, January 1991. Available as Indiana University Computer Science Department Technical Report No. 323 (December 1990).

12

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, pages 209-227. Springer, 1995. LNCS vol. 901, proceedings of the Second International Conference, TPCD'94.

13

Paul S. Miner and Steven D. Johnson. Verification of an optimized fault-tolerant clock synchronization circuit: A case study exploring the boundary between formal reasoning systems. In Satnam Singh, Mary Sheeran, and Geraint Jones, editors, Third Workshop on Designing Correct Circuits. Springer Electronic Workshops in Computing, 1996. http://www.springer.co.uk/ewic/workshops/DCC96.

14

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, pages 128-137, 1994. Proceedings of SRDS 94 held at Dana Point, California, October 1994.

15

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.

16

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

17

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), pages 438-441. IEEE, October 1993. Also published as Tech Report No. 385, Computer Science Department, Indiana University.

18

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

19

Kamlesh Rath and Steven D. Johnson. Toward a basis for protocol specification and process decomposition. In D. Agnew, L. Claesen, and R. Camposano, editors, Proceedings of IFIP Conference on Hardware Description Languages and their Applications, pages 157-174. Elsevier, April 1993. Also published as Technical Report No. 375, Dept. of Computer Science, Indiana University.

20

Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. Behavior tables: A basis for system representation and transformational system synthesis. In Proceedings of the International Conference on Computer Aided Design (ICCAD), pages 736-740. IEEE, November 1993. Also published as Technical Report 89, Computer Science Department, Indiana University.

21

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

22

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.

23

M. Esen Tuna, Steven D. Johnson, and Bob Burger. Continuations in hardware-software codesign. In Proceedings of the International Conference on Computer Design (ICCD), pages 264-269. IEEE, October 1994. Also published as Tech Report # 409, Computer Science Department, Indiana University.

24

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, pages 86-89. IEEE, March 1995.

25

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

26

Zheng Zhu and Steven D. Johnson. An algebraic framework for data abstraction in hardware description. In Jones and Sheeran, editors, Proceedings of The Oxford Workshop on Designing Correct Circuits. Springer, 1990.

27

Zheng Zhu and Steven D. Johnson. An example of interactive hardware transformation. In Subramanyam, editor, Proceedings of ACM International Workshop on Formal Methods in VLSI Design, January 1991. available as Techical Report 383, Computer Science Department, Indiana University.

28

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, October 1994.

About this document ...