A formal method for hardware design using attribute grammars

Recent advances in fabrication technology have pushed the digital designers´ perspective towards higher levels of abstraction. While a lot of research work has been reported to support this demand, the development of automated high-level synthesis environments is still an experimental field. 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, scheduling heuristics. Their main advantages being modularity and declarative notation. In this paper, a methodology to prove the correctness of all previously presented transformations is given. The overall hardware design methodology proposed, supports provable correct transformations and combines a mathematical framework with the problem of high-level synthesis for the first time