Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars

  • George Economakos
  • George Papakonstantinou
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)


Recent advances in fabrication technology have pushed the digital designers’ perspective towards higher levels of abstraction. Previous work has shown that attribute grammars, used in traditional compiler construction, can also be effectively adopted to describe in a formal and uniform way high-level hardware compilation heuristics, their main advantages being modularity and declarative notation. In this paper, a more abstract form of attribute grammars, relational attribute grammars, are further applied as a framework over which formal hardware verification is performed along with synthesis. The overall hardware design methodology proposed is a novel idea that supports provable correct designs.


Parse Tree Semantic Condition Behavioral Description Attribute Grammar Nonterminal Symbol 
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.


  1. 1.
    P. Deransart and J. Maluszynski. A Grammatical View of Logic Programming. MIT Press, 1993.Google Scholar
  2. 2.
    G. Economakos and G. Papakonstantinou. Exploiting the use of VHDL specifications in the AGENDA high-level synthesis environment. In 24th EUROMICRO Conference, Workshop on Digital System Design, pages 91–98. EUROMICRO, 1998.Google Scholar
  3. 3.
    G. Economakos, G. Papakonstantinou, K. Pekmestzi, and P. Tsanakas. Hardware compilation using attribute grammars. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pages 273–290. IFIP WG 10.5, 1997.Google Scholar
  4. 4.
    G. Economakos, G. Papakonstantinou, and P. Tsanakas. An attribute grammar approach to high-level automated hardware synthesis. Information and Software Technology, 37(9):493–502, 1995.CrossRefGoogle Scholar
  5. 5.
    G. Economakos, G. Papakonstantinou, and P. Tsanakas. AGENDA: An attribute grammar driven environment for the design automation of digital systems. In Design Automation and Test in Europe Conference and Exhibition, pages 933–934. ACM/IEEE, 1998.Google Scholar
  6. 6.
    G. Economakos, G. Papakonstantinou, and P. Tsanakas. Incorporating multi-pass attribute grammars for the high-level synthesis of ASICs. In Symposium on Applied Computing, pages 45–49. ACM, 1998.Google Scholar
  7. 7.
    D. Gajski, N. Dutt, A. Wu, and S. Lin. High-Level Synthesis. Kluwer Academic Publishers, 1992.Google Scholar
  8. 8.
    D. E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2(2):127–145, 1968.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Y-L. Lin. Recent development in high level synthesis. ACM Transactions on Design Automation of Electronic Systems, 2(1):2–21, 1997.CrossRefGoogle Scholar
  10. 10.
    M. C. McFarland, A. C. Parker, and R. Camposano. The high-level synthesis of digital systems. Proceedings of the IEEE, 78(2):301–318, 1990.CrossRefGoogle Scholar
  11. 11.
    K. L. McMillan. Fitting formal methods into the design cycle. In 31st Design Automation Conference, pages 314–319. ACM/IEEE, 1994.Google Scholar
  12. 12.
    J. Paaki. Attribute grammar paradigms-a high-level methodology in language implementation. ACM Computing Surveys, 27(2):196–255, 1995.CrossRefGoogle Scholar
  13. 13.
    R. A. Walker and S. Chaudhuri. High-level synthesis: Introduction to the scheduling problem. IEEE Design ℰ Test of Computers, 12(2):60–69, 1995.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • George Economakos
    • 1
  • George Papakonstantinou
    • 1
  1. 1.Dept. of Electrical and Computer EngineeringNational Technical University of AthensGreece

Personalised recommendations