CISE Postdoctoral Program: Diagrammatic Reasoning in Hardware Verification

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

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 ***