A Canonical Form for Circuit Diagrams

Kathi Fisler?

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

May 1, 1995

Abstract

A canonical form for circuit diagrams with a designated start state is presented. The form is based upon finite automata minimization and Shannon's canonical form for boolean expressions.

1 Introduction

This paper presents a canonical form for circuit diagrams with a designated start state. It builds upon our previous work in the logic of hardware diagrams [Fis94]. This canonical form will be used to prove a set of inference rules on circuit diagrams logically complete in a companion paper. We present a general discussion of our canonical form in section 2, a background of circuit diagram logic in section 3 and the canonical form algorithm in section 4.

2 Canonical Forms and Circuit Diagrams

In section 3, we define an equivalence relation on circuit diagrams such that all diagrams in the same equivalence class are behaviorally equivalent. Intuitively, two circuits are behaviorally equivalent if and only if they have the same observable external behavior when operated on the same sets of inputs. We would like to be able to determine whether two circuits are behaviorally equivalent without the need for exhaustive simulation. One way to do this would be to select a unique representative from each equivalence class and to define a function that maps any circuit diagram to the representative of its class. Two circuit diagrams could then be compared for behavioral equivalence by applying the function to each diagram and seeing if the same representative circuit was returned. Assuming we can define both the function and the representatives, we refer to the function as a canonicalizer and say that those circuit diagrams in the range of the function are in canonical form.

A circuit diagram canonicalizer could take many forms. For example, given the correlation between circuit diagrams and state machines, we could design a canonicalizer that converted a circuit diagram into a Mealy/Moore machine, minimized the state machine, then used a fixed implementation technique to convert the state machine back into a circuit diagram. The only drawback to

?Research supported by AT&T Bell Laboratories through the PhD Fellowship Program.