Verification-Aware Algorithmic Synthesis based on Canonical Data Flow Representation

基于规范数据流表示的验证感知算法综合

• 批准号: 0702506
• 负责人: Maciej Ciesielski
• 金额: --
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-06-01 至 2011-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0702506&HistoricalAwards=false
• 关键词: Verification; Aware; Algorithmic; Synthesis; based

ABSTRACTNSF Proposal 0702506PI: Maciej CiesielskiInst: U of Massachusetts, AmherstVerification-Aware Algorithmic Synthesis based on Canonical Data Flow RepresentationThis 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.

摘要/ abstract摘要：nsf提案0702506PI: Maciej ciesielski institute: U of Massachusetts， amherst基于规范数据流表示的验证感知算法合成这项工作为数据密集型应用的算法合成和验证提出了一种新的方法。建议的工作提供了一种系统的方法来执行在算法级别使用标准编程语言（如C或c++）指定的设计的初始描述的行为转换。在功能或行为层面优化设计规范，而不是在寄存器-传输或门级，已被证明对合成硬件的质量有最大的影响。所提出的方法是基于计算的一种新的规范表示，称为泰勒展开图（TED）。作为规范的功能表示，TED表示了一类结构表示，可以从中选择针对特定设计目标进行优化的结构表示。TED将作为一种工具，将初始的“非定时”算法设计规范转化为数据流描述，从而产生针对特定设计成本（如面积、延迟、功耗或性能）进行优化的架构。修改后的数据流图可以通过标准的高级合成工具进行合成，以生成RTL网络列表。这项工作的一个重要方面是，它以验证感知的方式执行合成。这是通过支持那些“验证友好”的行为转换，并通过维护行为转换历史记录以供正式的验证引擎使用来实现的。建议的工作将最终发展一个CAD系统，用于信号处理和面向算法的设计的快速建筑探索。原型系统将在全球网络上发布。