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 more abstract form of attribute grammars, relational attribute grammars, are further applied for the construction of a formal proof methodology, to verify the correctness of scheduling transformations in the same uniform environment. The overall hardware design methodology proposed, supports provable correct transformations and gives a novel idea for combining high-level synthesis with a mathematical framework.