Synthesis and Verification of Combinational, Sequential and Behavioral Logic

组合、顺序和行为逻辑的综合和验证

• 批准号: 9115432
• 负责人: Gary Hachtel
• 金额: $ 195.89万
• 依托单位: University of Colorado at Boulder
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1992
• 资助国家: 美国
• 起止时间: 1992-02-15 至 1996-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9115432&HistoricalAwards=false
• 关键词: Synthesis; Verification; Combinational; Sequential; Behavioral

Hachtel This a joint project with Colorado, (G. Hachtel, M. Lightner and F. Somenzi), UC, Berkeley (R.K. Brayton, A.R. Newton and A. Sangiovanni-Vincentelli), and Stanford (G. De Micheli). The research is a systematic approach to synthesis and verification of logic at all levels, combinational, sequential and behavioral, from HDL specifications. Objectives are: 1. Performance oriented synthesis through realistic modeling and delay/area tradeoff optimization; 2. Maximization of testability; and 3. Exploiting partitioning to solve both chip and multi-chip module design problems. The model is of sequential circuits based on a network of interacting, possibly non-deterministic, finite state machines (FSMs), in which interconnections can have unbounded delay attributes. In this model, the component machines may have symbolic or encoded I/O and can degenerate to just combinational logic or just latches. This enables uniform treatment of disparate objects such as RAMs, controllers, ALUs, pipeline registers, etc. Research topics are: 1. algorithms and theory for logic manipulation to support a variety of applications; 2. design, synthesis, and formal approaches based on the theory and algorithms; 3. design of embedded controllers, including hardware-software co-design; and 4. application of logic techniques to "non-standard" areas such as machine learning, theorem proving and combinatorics. A set of coordinated synthesis tools is being produced. The tools operate at both high level or low level depending on whether they operate above or below the FSM model.

哈赫特尔 这是一个与科罗拉多的联合项目。哈赫特尔，M. Lightner和F. Somenzi），UC，Berkeley（R.K. Brayton，A.R. Newton和A. Sangiovanni-Vincentelli）和斯坦福大学（G. De Micheli）。 该研究是一个系统的方法来综合和验证的逻辑在所有级别，组合，顺序和行为，从HDL规范。 目标是：1. 通过逼真的建模和延迟/面积权衡优化面向性能的综合; 2. 最大化可测试性; 3. 利用分区来解决芯片和多芯片模块设计问题。 该模型是基于交互网络的时序电路，可能是非确定性的，有限状态机（FSM），其中互连可以有无限的延迟属性。 在这个模型中，组件机器可以具有符号或编码的I/O，并且可以退化为组合逻辑或锁存器。 这使得能够统一处理不同的对象，如RAM、控制器、ALU、流水线寄存器等。 研究课题为：1. 用于逻辑操作的算法和理论，以支持各种应用; 2. 基于理论和算法的设计、综合和形式化方法; 3. 嵌入式控制器的设计，包括软硬件协同设计;以及4. 将逻辑技术应用于“非标准”领域，如机器学习，定理证明和组合学。 目前正在编制一套协调的综合工具。 这些工具在高级别或低级别上运行，这取决于它们是在FSM模型之上还是之下运行。