NSF Young Investigator Award: Formal Methods for Hardware and Software Verification

Devadas主要研究VLSI电路设计的逻辑和行为验证，以及硬件验证技术在软件验证中的应用。主题包括：1；利用自由二进制决策图（fbdd）找到有用的电路布尔表示和有效的操作方法。正在开发用于组合和顺序、综合、测试和验证应用的算法。2. 根据非管道化规范验证管道化实现的自动方法正在被探索。这些方法确保在非流水线电路中执行任何指令时发生的每个数据传输也发生在流水线电路中。目前正在开发一种符号仿真方法，可以根据指令集规范有效地验证流水线微处理器。3. FBDD表示被用来寻找允许自动软件验证的符号遍历方法。这些也被用于通过验证程序是否满足正确性属性来调试软件程序。

Devadas Research is on logic and behavioral verification of VLSI circuit designs, and application of hardware verification techniques to software verification. Topics include: 1. Use of Free Binary Decision Diagrams (FBDDs) to find useful Boolean representations of circuits and efficient manipulation methods for them. Algorithms for combinational and sequential, synthesis, test and verification applications are being developed. 2. Automatic methods to verify pipelined implementations against unpipelined specifications are being explored. The methods ensure that each data transfer that takes place upon the execution of any instruction in the unpipelined circuit also occurs in the pipelined circuit. A symbolic simulation method is being developed that will efficiently verify pipelined micro- processors against instruction set specifications. 3. FBDD representations are being used to find symbolic traversal methods which allow for automatic software verification. These are also being used to debug software programs by verifying that the program satisfies correctness properties.