Formal Verification of Microprocessors by Design Reduction

该项目正在探索一类称为设计简化的验证方法，该方法比传统方法具有优势。设计缩减的工作原理是逐步简化设计。在每一步，一致性检查是使用符号验证方法，使用符号模拟和自动决策程序的逻辑片段。例如，最初的设计减少建议删除流水线和类似的优化，消除缓存，简化接口，并消除陷阱和中断。一旦设计被尽可能地简化，它就可以比原始设计更容易地与用户提供的规格进行比较。该项目还在研究几种有希望的途径，以避免或简化归纳不变量的生成，这是符号验证中最耗时的方面。该项目正在寻找：新的证明方法，只需要不变量的某些状态，其中不变量是比较简单的表达;识别内部正确性条件，有助于一个不变的方法;和方法集成近似模型检查到一个更一般的框架。

This project is exploring a class of verification methods, called design reductions, which have advantages over conventional approaches. Design reduction works by simplifying a design incrementally. At each step, consistency checking is done using symbolic verification methods, which use symbolic simulation and automatic decision procedures for fragments of logic. For example, initial design reductions are proposed to remove pipelining and similar optimizations, eliminate caching, simplify interfaces, and eliminate traps and interrupts. Once a design has been simplified as much as possible, it can be compared with a user-supplied specification much more easily than can the original design. The project is also investigating several promising avenues to avoid or simplify the generation of inductive invariants, which is the most time-consuming aspect of symbolic verification. The project is searching for: new proof methods that only require invariants for certain states where the invariants are comparatively simple to express; ways of identifying internal correctness conditions that contribute to an invariant; and methods integrating approximate model checking into a more general framework.