CISE Postdoctoral Program: Diagrammatic Reasoning in Hardware Verification

9625898 Vardi, Moshe Y Felleisen， Matthias William Marsh Rice University CISE博士后项目：硬件验证中的图解推理该奖项支持CES助理Kathryn Fisher。图表是硬件设计的基础。设计师广泛地使用它们来传达细节，表达属性，以及对设计进行非正式的推理。尽管如此，很少有人注意到在验证中支持图解推理。因此，在设计实践和验证方法之间存在着巨大的差距，这使得设计师很难执行验证。该项目旨在通过围绕公共硬件表示开发的逻辑来弥合这一差距。该逻辑有五种句法表示：三种图解和两种句子。推理规则支持使用来自多个表示的信息进行推理，从而为图解信息在实践中的使用提供形式化支持。实际目标是调查这种逻辑是否使设计人员更容易进行验证。基于逻辑的验证工具将由新手和有经验的从业者与现有方法一起实现和评估。主要的理论目标是检查图表信息如何帮助细化自动化和交互式验证方法之间的当前边界。这些方法的集成将是该工具的一个重要特性

9625898 Vardi, Moshe Y Felleisen, Matthias William Marsh Rice University CISE Postdoctoral Program: Diagrammatic Reasoning in Hardware Verification This award supports CES associate Kathryn Fisher. Diagrams are fundamental to hardware design. Designers use them extensively to convey details, to express properties, and to reason informally about designs. Despite this, little attention has been paid to supporting diagrammatic reasoning in verification. As a result, a substantial gap exists between design practice and verification methodology that makes performing verification difficult for designers. The project aims to bridge this gap through a logic developed around common hardware representations. The logic has five syntactic representations: three diagrammatic and two sentential. The inference rules support reasoning with information from multiple representations, thereby providing formal support for how diagrammatic information is used in practice. The practical objective is to investigate whether this logic makes verification easier for designers. A verification tool based on the logic will be implemented and evaluated alongside existing methodologies by both novices and experienced practitioners. The main theoretical objective is to examine how diagrammatic information can help refine the current boundaries between automated and interactive verification methodologies. The integration of these approached will be an important feature of the tool ***