Visualizing System Factorizations with Behavior Tables
Behavior tables are a design formalization intended to support interactive design derivation for hardware and embedded systems. It is a reformulation of the DDD transformation system, bridging behavioral and architectural forms of expression. The tabular representations aid in visualizing design aspects that are subject to interactive refinement and optimization. These ideas are illustrated for system factorization, an import class of decompositions used in design derivation. A series of examples shows how features seen in the behavior tables determine the course of a factorization and how the rules of a core behavior table algebra compose into the more large scale transformations done at the interactive level.
KeywordsDecision Table Computer Science Department Subject Term High Level Synthesis Action Table
Unable to display preview. Download preview PDF.
- 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, ftp://ftp.cs.indiana.edu/pub/techreports/TR456.ps.Z.
- 3.Robert G. Burger. The scheme machine. Technical Report 413, Indiana University, Computer Science Department, August 1994. 59 pages.Google Scholar
- 4.Constance Heitmeyer, Alan Bull, Carolyn Gasarch, and Bruce Labaw. SCR*: a toolset for specifying and analyzing requirements. In Proceedings of the Tenth Annual Conference on Computer Assurance (COMPASS’ 95), pages 109–122, 1995.Google Scholar
- 5.D. N. Hoover, David Guaspari, and Polar Humenn. Applications of formal methods to specification and safety of avionics software. Contractor Report 4723, National Aeronautics and Space Administration Langley Research Center (NASA/LRC), Hampton VA 23681-0001, November 1994.Google Scholar
- 6.Steven D. Johnson. Manipulating logical organization with system factorizations. In Leeser and Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of LNCS, pages 260–281. Springer, July 1989.Google Scholar
- 7.Steven D. Johnson. A tabular language for system design. In C. Michael Holloway and Kelly J. Hayhurst, editors, Lfm97: Fourth NASA Langley For-mal Methods Workshop, September 1997. NASA Conference Publication 3356, http://atb-www.larc.nasa.gov/Lfm97/.
- 8.Steven D. Johnson and Bhaskar Bose. A system for mechanized digital design derivation. In IFIP and ACM/SIGDA International Workshop on Formal Meth-ods in VLSI Design, 1991. Available as Indiana University Computer Science Department Technical Report No. 323 (rev. 1997).Google Scholar
- 9.Steven D. Johnson and Alex Tsow. Algebra of behavior tables. In C. M. Holloway, editor, Lfm2000. Langley Formal Methods Group, NASA, 2000. Proceedings of the 5th NASA Langley Formal Methods Workshop, Williamsburg, Virginia, 13–15 June, 2000, http://shemesh.larc.nasa.gov/fm/Lfm2000/.
- 10.Ramayya Kumar, Christian Blumenröohr, Dirk Eisenbiegler, and Detlef Schmid. Formal synthesis in circuit design-a classification and survey. In M. Srivas and A. Camilleri, editors, Formal Methods in Computer Aided Design, pages 294–309, Berlin, 1996. Springer LNCS 1166. Proceedings of FMCAD’96.CrossRefGoogle Scholar
- 12.Sam Owre, John Rushby, and Natarajan Shankar. Analyzing tabular and state-transition specifications in PVS. Technical Report SRI-CSL-95-12, Computer Science Laboratory, SRI International, Menlo Park, CA, July 1995. Revised May 1996. Available, with specification files, from http://www.csl.sri.com/csl-95-12.html.Google Scholar
- 13.Franklin P. Prosser and David E. Winkel. The Art of Digital Design. Prentice/Hall International, second edition, 1987.Google Scholar
- 14.Kamlesh Rath. Sequential System Decomposition. PhD thesis, Computer Science Department, Indiana University, USA, 1995. Technical Report No. 457, 90 pages.Google Scholar
- 15.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.Google Scholar
- 16.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 (GLSVLSI95), pages 86–89. IEEE, March 1995.Google Scholar