Synthesis and Verification of Combinational, Sequential and Behavioral Logic

Hachtel这是一个与科罗拉多州(G.Hachtel，M.Lightner和F.Somezi)、加州大学伯克利分校(R.K.Brayton，A.R.牛顿和A.Sanyovanni-Vincentelli)和斯坦福(G.de Micheli)的联合项目。这项研究是一种系统的方法来综合和验证所有级别的逻辑，组合的，顺序的和行为的，从硬件描述语言规范。目标是：1.通过真实建模和延迟/面积折衷优化进行面向性能的综合；2.最大化可测试性；3.利用划分来解决芯片和多芯片模块设计问题。该模型是基于相互作用的、可能不确定的有限状态机(FSM)网络的时序电路，其中互连可以具有无限的延迟属性。在该模型中，组件机可以具有符号或编码的I/O，并且可以退化为仅组合逻辑或仅锁存。这使得能够统一对待不同的对象，如RAM、控制器、ALU、流水线寄存器等。研究主题是：1.支持各种应用的逻辑操作的算法和理论；2.基于理论和算法的设计、综合和形式化方法；3.嵌入式控制器的设计，包括硬件-软件协同设计；以及4.逻辑技术在机器学习、定理证明和组合学等非标准领域的应用。一套协调一致的综合工具正在制作中。这些工具在高水平或低水平上运行，取决于它们是在密克罗尼西亚联邦模式之上还是之下运行。

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.