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.