CISE Postdoctoral Program: Diagrammatic Reasoning in Hardware Verification

CISE博士后项目：硬件验证中的图解推理

• 批准号: 9625898
• 负责人: Moshe Vardi
• 金额: $ 5.06万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-03-15 至 1999-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9625898&HistoricalAwards=false
• 关键词: CISE; Postdoctoral; Program; Diagrammatic; Reasoning

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

9625898 VARDI，MOSHE Y FELLEISEN，MATTHIAS WILLIAM MARSH RICE UNIVERUTITER CISE POSTOCTORAL计划：硬件验证中的示意性推理该奖项支持CES同事Kathryn Fisher。图是硬件设计的基础。 设计师广泛使用它们来传达详细信息，表达属性以及非正式地理解设计。 尽管如此，很少关注支持验证中的图解推理。 结果，设计实践和验证方法之间存在很大的差距，这使设计人员难以执行验证。 该项目旨在通过围绕共同硬件表示形式开发的逻辑来弥合这一差距。 逻辑具有五个句法表示：三个图表和两个句子。 推理规则支持推理，并提供来自多个表示的信息，从而为如何在实践中使用图形信息提供了正式的支持。 实际目标是研究这种逻辑是否使设计人员更容易验证。 基于逻辑的验证工具将由新手和经验丰富的从业者与现有方法一起实施和评估。 主要的理论目标是研究图解信息如何帮助完善自动化和交互式验证方法之间的当前边界。 这些方法的集成将是工具的重要特征***