Advertisement

An approach to formalization of data flow graphs

  • Per Bojsen
Conference paper
  • 227 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

This paper describes the data flow graph (DFG) simulator formalized by the author in the logic of the Boyer-Moore theorem prover, nqthm, which is intended to serve as the basis for formal verification of DFGs. DFGs are central to the field of architectural synthesis. Formalizing DFGs by defining an interpreter is one possible approach to formal verification of DFGs. The type of DFGs being formalized is described, followed by an overview of the dfg simulator including a discussion of the representation of DFGs chosen. Due to the theorem prover's lack of a sufficiently strong type system, it is necessary to define predicates stating consistency of the objects purportedly representing DFGs. These issues are discussed and the predicates solving them are presented.

Keywords

Token List Node Input Node Type Formal Verification Correctness Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    R. S. Boyer and J. S. Moore. A mechanical proof of the turing completeness of pure lisp. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 133–167. 1984.Google Scholar
  2. 2.
    R. S. Boyer and J. S. Moore. A mechanical proof of the unsolvability of the halting problem. Journal of the ACM, 31(3):441–458, March 1984.Google Scholar
  3. 3.
    Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, Inc., 1979.Google Scholar
  4. 4.
    Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, Inc., 1988.Google Scholar
  5. 5.
    Jens P.Brage. The semantics of a set of DFG nodes for high-level synthesis. Technical Report DAG91-TR01, Design Automation Group, Department of Computer Science, Technical University of Denmark, July 1991.Google Scholar
  6. 6.
    Gjalt G. de Jong. Verification of data flow graphs using temporal logic. In Applied Formal Methods For Correct VLSI Design, pages 301–310, November 1989.Google Scholar
  7. 7.
    Jack B. Dennis. First version of a data flow procedure language. In Lecture Notes in Computer Science 19, Programming Symposium, pages 362–376. Springer-Verlag, 1974.Google Scholar
  8. 8.
    Jack B.Dennis. Models of data flow computation. In Control Flow and Data Flow, Concepts of Distributed Programming, pages 346–353. Springer-Verlag, 1986.Google Scholar
  9. 9.
    Krishna M. Kavi, Bill P. Buckles, and U. Narayan Bhat. A formal definition of data flow graph models. IEEE Transactions on Computers, C-35(l l):940–948, November 1986.Google Scholar
  10. 10.
    Jan Madsen and Jens P. Brage. Flow graph modelling using VHDL bus resolution functions. In EuroVHDL'90, First European Conference on VHDL Methods, Marseille, France, page 11, September 1990.Google Scholar
  11. 11.
    Wolfgang Reisig. Petri Nets, An Introduction. Springer-Verlag, 1985.Google Scholar
  12. 12.
    J. T. J. van Eijndhoven, G. G. de Jong, and L. Stok. The ASCIS data flow graph semantics and textual format. Technical Report 91-E-251, Faculty of Electrical Engineering, Eindhoven University of Technology, April 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Per Bojsen
    • 1
  1. 1.Design Automation Group, Center for Integrated ElectronicsTechnical University of DenmarkLyngbyDenmark

Personalised recommendations