形式化验证，Gap-free Processor Verifification by S2QED and Property Generation（一）

news2024/11/15 15:23:56

一、Article:文献出处（方便再次搜索）

（1）作者

（2）文献题目

（3）文献时间

（4）引用

二、Data:文献数据（总结归纳，方便理解）

（1）背景介绍

（2）目的

（3）结论

（4）主要实现手段

（5）实验结果

（6）问题记录

三、Comments对文献的想法（强迫自己思考，结合自己的学科）

四、Why:为什么看这篇文献（方便再次搜索）

五、Summary:文献方向归纳（方便分类管理）

一、Article:文献出处（方便再次搜索）

Keerthikumara Devarajegowda, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz (Technische University at Kaiserslautern, 德国凯泽斯劳滕大学)
Keerthikumara Devarajegowda, Wolfgang Ecker(Infifineon Technologies AG,英飞凌技术公司)
Eshan Singh, Clark Barrett, Subhasish Mitra (Stanford University, 美国斯坦福大学)
Wolfgang Ecker(Technische Universität München, 慕尼黑工业大学)

K. Devarajegowda et al., "Gap-free Processor Verification by S2QED and Property Generation," 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE), Grenoble, France, 2020, pp. 526-531, doi: 10.23919/DATE48585.2020.9116515.

随着基于RISC-V指令集架构计算市场的不断增长（比如：物联网），迫切需要一种新的高效的处理器验证技术；

在处理器设计过程中，形式化验证的主要障碍之一是需要过多的人工干预和专业知识，开发一组完全覆盖所有指令集行为的property是laborious和challenging的；

现有的完整的形式验证技术，除了需要很多的人工干，还很难在许多工业验证流程中集成。

开发一种自动化的（省时省力）、能够同时检测出单指令bug和多指令bug的、方便和工业流程结合的形式化验证方法。

对处理器的RTL级别的微架构描述进行全面的验证，以确定该微架构描述是否正确地实现了该处理器的ISA级别规范。总的来说，开发一组高度自动化的（人工干预少得多）、完备的处理器验证方法；

拓展了S2QED方法，同时覆盖了single and multiple instruction bugs，并且确保设计能根据一个定义良好的criterion得到完整验证；
鲁棒性强，通过少量的人工干预，从ISA模型中自动生成property；
不同于传统的model checking，验证工程师无需明确指定处理器的具体（特定）行为场景，比如：stalling、exception、speculation等，计算模型可以进行隐式处理。

行文模糊，多处指代不明，如后文提到的S2QED property并不等同于改进前的S2QED property，但作者常混用一个称呼；
类似地，在公式推导部分，主要是Case Split Test部分，字母、下标和公式介绍不清晰，造成阅读障碍；
在技术实现上面，就目前而言，如作者所说，其验证实现局限于顺序执行CPU，但工业中，大多数处理器都是乱序执行的，还可以拓展到无核设备，比如：内存控制器、外围设备等。