Verification-Aware Algorithmic Synthesis based on Canonical Data Flow Representation

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

ABSTRACT NSF Proposal 0702506 PI: Maciej Ciesielski Inst: U of Massachusetts, Amherst Verification-Aware Algorithmic Synthesis based on Canonical Data Flow Representation This work proposes a new methodology in algorithmic synthesis and verification for data intensive applications. The proposed work offers a systematic method to perform behavioral transformation of the initial description of designs specified at the algorithmic level using standard programming languages, such as C or C++. Optimization of design specification at the functional or behavioral level, rather than on the register-transfer or gate level, has been shown to have the greatest impact on the quality of synthesized hardware. The proposed method is based on a novel canonical representation of the computation, called Taylor Expansion Diagram (TED). As a canonical functional representation, TED represents a class of structural representations, from which one optimized for a particular design objective can be selected. TED will serve as a vehicle to transform initial, "un-timed" algorithmic design specification into a data flow description that will produce architecture optimized for a particular design cost, such as area, latency, power, or performance. The modified data flow graph can be synthesized by a standard high-level synthesis tool to produce an RTL net-list. An important aspect of this work is that it performs synthesis in a verification-aware fashion. This is accomplished by favoring those behavioral transformations that are ``verification-friendly'' and by maintaining a record of behavioral transformation history to be used by a formal verification engine. The proposed work will culminate in the development of a CAD system for fast architectural exploration for signal processing and algorithm-oriented designs. The prototype system will be distributed on the world-wide web.