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