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

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

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.