Refinement and property checking in high-level synthesis using attribute grammars

Abstract

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.