Synthesis and Verification of Combinational, Sequential and Behavioral Logic

点击翻译按钮获取中文摘要

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.