A Logical Formalization of Hardware Design Diagrams?

Kathi Fisler
Department of Computer Science
Lindley Hall 215
Indiana University
Bloomington, IN 47401
[email protected]

Abstract

Diagrams have been left as an informal tool in hardware reasoning, thus rendering them unacceptable representations within formal reasoning systems. We demonstrate some advantages of formally supporting diagrams in hardware verification systems via a simple example and provide a logical formalization of hardware diagrams upon which we are constructing a verification tool.

1 Introduction

The increased use of formal methods for verifying hardware specifications has generated a wealth of research into the formal models and representations of hardware that best facilitate the verification task. Most such models are based on combinations of temporal and higher-order logic which, while effective, do not necessarily reflect the models used during the design process. The hardware design process involves the use of a collection of diagrammatic forms, such as circuit diagrams and timing diagrams, which depict certain characteristics of hardware components more naturally than purely sentential representations. Given the relationship between good representations and ease and clarity of proof, it then seems natural to ask why formal verification does not support these representations.

One answer is that the lack of formalization of diagrammatic representations has precluded their use in formal proof and verification. Another is that diagrammatic representations are often seen as too specialized to support general reasoning about hardware components. However, the argument could be made that certain hardware characteristics are better represented diagrammatically, therefore reflecting limitations to sentential representations. Given this, it would seem that the development of logical systems in which sentential and diagrammatic representations could interact formally would be the best choice for hardware formal methods. Barwise and Etchemendy have demonstrated the feasibility of such heterogeneous logics via their Hyperproof system [1] [2]. Our goal in this project is to apply the logical underpinnings of Hyperproof to the domain of hardware design and verification.

The first step in developing a heterogeneous logic for the hardware domain is the formalization of the diagrammatic notations; this portion of the project is presented here. In this paper we are going

?To appear in Diagrammatic Reasoning, edited by Gerard Allwein and Jon Barwise.